src/HOL/Import/HOL/HOL4Base.thy
author wenzelm
Wed, 21 Sep 2005 18:04:49 +0200
changeset 17566 484ff733f29c
parent 17188 a26a4fc323ed
child 17644 bd59bfd4bf37
permissions -rw-r--r--
new header syntax;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15647
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
     1
(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
     2
17566
484ff733f29c new header syntax;
wenzelm
parents: 17188
diff changeset
     3
theory HOL4Base imports "../HOL4Compat" "../HOL4Syntax" begin
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     4
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     5
;setup_theory bool
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     6
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     7
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     8
  ARB :: "'a" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     9
  "ARB == SOME x. True"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    10
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    11
lemma ARB_DEF: "ARB = (SOME x. True)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    12
  by (import bool ARB_DEF)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    13
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    14
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    15
  IN :: "'a => ('a => bool) => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    16
  "IN == %x f. f x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    17
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    18
lemma IN_DEF: "IN = (%x f. f x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    19
  by (import bool IN_DEF)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    20
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    21
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    22
  RES_FORALL :: "('a => bool) => ('a => bool) => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    23
  "RES_FORALL == %p m. ALL x. IN x p --> m x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    24
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    25
lemma RES_FORALL_DEF: "RES_FORALL = (%p m. ALL x. IN x p --> m x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    26
  by (import bool RES_FORALL_DEF)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    27
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    28
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    29
  RES_EXISTS :: "('a => bool) => ('a => bool) => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    30
  "RES_EXISTS == %p m. EX x. IN x p & m x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    31
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    32
lemma RES_EXISTS_DEF: "RES_EXISTS = (%p m. EX x. IN x p & m x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    33
  by (import bool RES_EXISTS_DEF)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    34
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    35
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    36
  RES_EXISTS_UNIQUE :: "('a => bool) => ('a => bool) => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    37
  "RES_EXISTS_UNIQUE ==
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    38
%p m. RES_EXISTS p m &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    39
      RES_FORALL p (%x. RES_FORALL p (%y. m x & m y --> x = y))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    40
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    41
lemma RES_EXISTS_UNIQUE_DEF: "RES_EXISTS_UNIQUE =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    42
(%p m. RES_EXISTS p m &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    43
       RES_FORALL p (%x. RES_FORALL p (%y. m x & m y --> x = y)))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    44
  by (import bool RES_EXISTS_UNIQUE_DEF)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    45
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    46
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    47
  RES_SELECT :: "('a => bool) => ('a => bool) => 'a" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    48
  "RES_SELECT == %p m. SOME x. IN x p & m x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    49
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    50
lemma RES_SELECT_DEF: "RES_SELECT = (%p m. SOME x. IN x p & m x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    51
  by (import bool RES_SELECT_DEF)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    52
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    53
lemma EXCLUDED_MIDDLE: "ALL t. t | ~ t"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    54
  by (import bool EXCLUDED_MIDDLE)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    55
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    56
lemma FORALL_THM: "All f = All f"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    57
  by (import bool FORALL_THM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    58
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    59
lemma EXISTS_THM: "Ex f = Ex f"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    60
  by (import bool EXISTS_THM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    61
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    62
lemma F_IMP: "ALL t. ~ t --> t --> False"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    63
  by (import bool F_IMP)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    64
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    65
lemma NOT_AND: "~ (t & ~ t)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    66
  by (import bool NOT_AND)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    67
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    68
lemma AND_CLAUSES: "ALL t.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    69
   (True & t) = t &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    70
   (t & True) = t & (False & t) = False & (t & False) = False & (t & t) = t"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    71
  by (import bool AND_CLAUSES)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    72
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    73
lemma OR_CLAUSES: "ALL t.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    74
   (True | t) = True &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    75
   (t | True) = True & (False | t) = t & (t | False) = t & (t | t) = t"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    76
  by (import bool OR_CLAUSES)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    77
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    78
lemma IMP_CLAUSES: "ALL t.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    79
   (True --> t) = t &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    80
   (t --> True) = True &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    81
   (False --> t) = True & (t --> t) = True & (t --> False) = (~ t)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    82
  by (import bool IMP_CLAUSES)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    83
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    84
lemma NOT_CLAUSES: "(ALL t. (~ ~ t) = t) & (~ True) = False & (~ False) = True"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    85
  by (import bool NOT_CLAUSES)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    86
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    87
lemma BOOL_EQ_DISTINCT: "True ~= False & False ~= True"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    88
  by (import bool BOOL_EQ_DISTINCT)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    89
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    90
lemma EQ_CLAUSES: "ALL t.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    91
   (True = t) = t &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    92
   (t = True) = t & (False = t) = (~ t) & (t = False) = (~ t)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    93
  by (import bool EQ_CLAUSES)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    94
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    95
lemma COND_CLAUSES: "ALL t1 t2. (if True then t1 else t2) = t1 & (if False then t1 else t2) = t2"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    96
  by (import bool COND_CLAUSES)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    97
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    98
lemma SELECT_UNIQUE: "ALL P x. (ALL y. P y = (y = x)) --> Eps P = x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    99
  by (import bool SELECT_UNIQUE)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   100
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   101
lemma BOTH_EXISTS_AND_THM: "ALL (P::bool) Q::bool. (EX x::'a. P & Q) = ((EX x::'a. P) & (EX x::'a. Q))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   102
  by (import bool BOTH_EXISTS_AND_THM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   103
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   104
lemma BOTH_FORALL_OR_THM: "ALL (P::bool) Q::bool.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   105
   (ALL x::'a. P | Q) = ((ALL x::'a. P) | (ALL x::'a. Q))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   106
  by (import bool BOTH_FORALL_OR_THM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   107
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   108
lemma BOTH_FORALL_IMP_THM: "ALL (P::bool) Q::bool.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   109
   (ALL x::'a. P --> Q) = ((EX x::'a. P) --> (ALL x::'a. Q))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   110
  by (import bool BOTH_FORALL_IMP_THM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   111
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   112
lemma BOTH_EXISTS_IMP_THM: "ALL (P::bool) Q::bool.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   113
   (EX x::'a. P --> Q) = ((ALL x::'a. P) --> (EX x::'a. Q))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   114
  by (import bool BOTH_EXISTS_IMP_THM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   115
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   116
lemma OR_IMP_THM: "ALL A B. (A = (B | A)) = (B --> A)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   117
  by (import bool OR_IMP_THM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   118
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   119
lemma DE_MORGAN_THM: "ALL A B. (~ (A & B)) = (~ A | ~ B) & (~ (A | B)) = (~ A & ~ B)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   120
  by (import bool DE_MORGAN_THM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   121
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   122
lemma IMP_F_EQ_F: "ALL t. (t --> False) = (t = False)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   123
  by (import bool IMP_F_EQ_F)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   124
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   125
lemma EQ_EXPAND: "ALL t1 t2. (t1 = t2) = (t1 & t2 | ~ t1 & ~ t2)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   126
  by (import bool EQ_EXPAND)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   127
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   128
lemma COND_RATOR: "ALL b f g x. (if b then f else g) x = (if b then f x else g x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   129
  by (import bool COND_RATOR)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   130
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   131
lemma COND_ABS: "ALL b f g. (%x. if b then f x else g x) = (if b then f else g)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   132
  by (import bool COND_ABS)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   133
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   134
lemma COND_EXPAND: "ALL b t1 t2. (if b then t1 else t2) = ((~ b | t1) & (b | t2))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   135
  by (import bool COND_EXPAND)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   136
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   137
lemma ONE_ONE_THM: "ALL f. inj f = (ALL x1 x2. f x1 = f x2 --> x1 = x2)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   138
  by (import bool ONE_ONE_THM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   139
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   140
lemma ABS_REP_THM: "(All::(('a => bool) => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   141
 (%P::'a => bool.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   142
     (op -->::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   143
      ((Ex::(('b => 'a) => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   144
        ((TYPE_DEFINITION::('a => bool) => ('b => 'a) => bool) P))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   145
      ((Ex::(('b => 'a) => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   146
        (%x::'b => 'a.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   147
            (Ex::(('a => 'b) => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   148
             (%abs::'a => 'b.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   149
                 (op &::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   150
                  ((All::('b => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   151
                    (%a::'b. (op =::'b => 'b => bool) (abs (x a)) a))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   152
                  ((All::('a => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   153
                    (%r::'a.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   154
                        (op =::bool => bool => bool) (P r)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   155
                         ((op =::'a => 'a => bool) (x (abs r)) r)))))))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   156
  by (import bool ABS_REP_THM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   157
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   158
lemma LET_RAND: "(P::'b => bool) (Let (M::'a) (N::'a => 'b)) = (let x::'a = M in P (N x))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   159
  by (import bool LET_RAND)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   160
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   161
lemma LET_RATOR: "Let (M::'a) (N::'a => 'b => 'c) (b::'b) = (let x::'a = M in N x b)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   162
  by (import bool LET_RATOR)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   163
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   164
lemma SWAP_FORALL_THM: "ALL P. (ALL x. All (P x)) = (ALL y x. P x y)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   165
  by (import bool SWAP_FORALL_THM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   166
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   167
lemma SWAP_EXISTS_THM: "ALL P. (EX x. Ex (P x)) = (EX y x. P x y)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   168
  by (import bool SWAP_EXISTS_THM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   169
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   170
lemma AND_CONG: "ALL P P' Q Q'. (Q --> P = P') & (P' --> Q = Q') --> (P & Q) = (P' & Q')"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   171
  by (import bool AND_CONG)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   172
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   173
lemma OR_CONG: "ALL P P' Q Q'. (~ Q --> P = P') & (~ P' --> Q = Q') --> (P | Q) = (P' | Q')"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   174
  by (import bool OR_CONG)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   175
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   176
lemma COND_CONG: "ALL P Q x x' y y'.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   177
   P = Q & (Q --> x = x') & (~ Q --> y = y') -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   178
   (if P then x else y) = (if Q then x' else y')"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   179
  by (import bool COND_CONG)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   180
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   181
lemma MONO_COND: "(x --> y) --> (z --> w) --> (if b then x else z) --> (if b then y else w)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   182
  by (import bool MONO_COND)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   183
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   184
lemma SKOLEM_THM: "ALL P. (ALL x. Ex (P x)) = (EX f. ALL x. P x (f x))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   185
  by (import bool SKOLEM_THM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   186
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   187
lemma bool_case_thm: "(ALL (e0::'a) e1::'a. (case True of True => e0 | False => e1) = e0) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   188
(ALL (e0::'a) e1::'a. (case False of True => e0 | False => e1) = e1)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   189
  by (import bool bool_case_thm)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   190
14847
44d92c12b255 updated;
wenzelm
parents: 14684
diff changeset
   191
lemma bool_case_ID: "ALL x b. (case b of True => x | _ => x) = x"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   192
  by (import bool bool_case_ID)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   193
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   194
lemma boolAxiom: "ALL e0 e1. EX x. x True = e0 & x False = e1"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   195
  by (import bool boolAxiom)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   196
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   197
lemma UEXISTS_OR_THM: "ALL P Q. (EX! x. P x | Q x) --> Ex1 P | Ex1 Q"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   198
  by (import bool UEXISTS_OR_THM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   199
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   200
lemma UEXISTS_SIMP: "(EX! x::'a. (t::bool)) = (t & (ALL x::'a. All (op = x)))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   201
  by (import bool UEXISTS_SIMP)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   202
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   203
consts
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   204
  RES_ABSTRACT :: "('a => bool) => ('a => 'b) => 'a => 'b" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   205
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   206
specification (RES_ABSTRACT) RES_ABSTRACT_DEF: "(ALL (p::'a => bool) (m::'a => 'b) x::'a.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   207
    IN x p --> RES_ABSTRACT p m x = m x) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   208
(ALL (p::'a => bool) (m1::'a => 'b) m2::'a => 'b.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   209
    (ALL x::'a. IN x p --> m1 x = m2 x) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   210
    RES_ABSTRACT p m1 = RES_ABSTRACT p m2)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   211
  by (import bool RES_ABSTRACT_DEF)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   212
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   213
lemma BOOL_FUN_CASES_THM: "ALL f. f = (%b. True) | f = (%b. False) | f = (%b. b) | f = Not"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   214
  by (import bool BOOL_FUN_CASES_THM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   215
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   216
lemma BOOL_FUN_INDUCT: "ALL P. P (%b. True) & P (%b. False) & P (%b. b) & P Not --> All P"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   217
  by (import bool BOOL_FUN_INDUCT)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   218
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   219
;end_setup
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   220
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   221
;setup_theory combin
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   222
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   223
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   224
  K :: "'a => 'b => 'a" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   225
  "K == %x y. x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   226
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   227
lemma K_DEF: "K = (%x y. x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   228
  by (import combin K_DEF)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   229
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   230
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   231
  S :: "('a => 'b => 'c) => ('a => 'b) => 'a => 'c" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   232
  "S == %f g x. f x (g x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   233
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   234
lemma S_DEF: "S = (%f g x. f x (g x))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   235
  by (import combin S_DEF)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   236
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   237
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   238
  I :: "'a => 'a" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   239
  "(op ==::('a => 'a) => ('a => 'a) => prop) (I::'a => 'a)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   240
 ((S::('a => ('a => 'a) => 'a) => ('a => 'a => 'a) => 'a => 'a)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   241
   (K::'a => ('a => 'a) => 'a) (K::'a => 'a => 'a))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   242
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   243
lemma I_DEF: "(op =::('a => 'a) => ('a => 'a) => bool) (I::'a => 'a)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   244
 ((S::('a => ('a => 'a) => 'a) => ('a => 'a => 'a) => 'a => 'a)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   245
   (K::'a => ('a => 'a) => 'a) (K::'a => 'a => 'a))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   246
  by (import combin I_DEF)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   247
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   248
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   249
  C :: "('a => 'b => 'c) => 'b => 'a => 'c" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   250
  "C == %f x y. f y x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   251
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   252
lemma C_DEF: "C = (%f x y. f y x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   253
  by (import combin C_DEF)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   254
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   255
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   256
  W :: "('a => 'a => 'b) => 'a => 'b" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   257
  "W == %f x. f x x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   258
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   259
lemma W_DEF: "W = (%f x. f x x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   260
  by (import combin W_DEF)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   261
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   262
lemma I_THM: "ALL x. I x = x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   263
  by (import combin I_THM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   264
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   265
lemma I_o_ID: "ALL f. I o f = f & f o I = f"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   266
  by (import combin I_o_ID)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   267
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   268
;end_setup
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   269
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   270
;setup_theory sum
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   271
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   272
lemma ISL_OR_ISR: "ALL x. ISL x | ISR x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   273
  by (import sum ISL_OR_ISR)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   274
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   275
lemma INL: "ALL x. ISL x --> Inl (OUTL x) = x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   276
  by (import sum INL)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   277
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   278
lemma INR: "ALL x. ISR x --> Inr (OUTR x) = x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   279
  by (import sum INR)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   280
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   281
lemma sum_case_cong: "ALL (M::'b + 'c) (M'::'b + 'c) (f::'b => 'a) g::'c => 'a.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   282
   M = M' &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   283
   (ALL x::'b. M' = Inl x --> f x = (f'::'b => 'a) x) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   284
   (ALL y::'c. M' = Inr y --> g y = (g'::'c => 'a) y) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   285
   sum_case f g M = sum_case f' g' M'"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   286
  by (import sum sum_case_cong)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   287
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   288
;end_setup
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   289
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   290
;setup_theory one
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   291
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   292
;end_setup
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   293
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   294
;setup_theory option
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   295
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   296
lemma option_CLAUSES: "(op &::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   297
 ((All::('a => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   298
   (%x::'a.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   299
       (All::('a => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   300
        (%y::'a.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   301
            (op =::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   302
             ((op =::'a option => 'a option => bool) ((Some::'a ~=> 'a) x)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   303
               ((Some::'a ~=> 'a) y))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   304
             ((op =::'a => 'a => bool) x y))))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   305
 ((op &::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   306
   ((All::('a => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   307
     (%x::'a.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   308
         (op =::'a => 'a => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   309
          ((the::'a option => 'a) ((Some::'a ~=> 'a) x)) x))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   310
   ((op &::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   311
     ((All::('a => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   312
       (%x::'a.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   313
           (Not::bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   314
            ((op =::'a option => 'a option => bool) (None::'a option)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   315
              ((Some::'a ~=> 'a) x))))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   316
     ((op &::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   317
       ((All::('a => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   318
         (%x::'a.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   319
             (Not::bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   320
              ((op =::'a option => 'a option => bool) ((Some::'a ~=> 'a) x)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   321
                (None::'a option))))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   322
       ((op &::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   323
         ((All::('a => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   324
           (%x::'a.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   325
               (op =::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   326
                ((IS_SOME::'a option => bool) ((Some::'a ~=> 'a) x))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   327
                (True::bool)))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   328
         ((op &::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   329
           ((op =::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   330
             ((IS_SOME::'a option => bool) (None::'a option)) (False::bool))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   331
           ((op &::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   332
             ((All::('a option => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   333
               (%x::'a option.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   334
                   (op =::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   335
                    ((IS_NONE::'a option => bool) x)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   336
                    ((op =::'a option => 'a option => bool) x
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   337
                      (None::'a option))))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   338
             ((op &::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   339
               ((All::('a option => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   340
                 (%x::'a option.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   341
                     (op =::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   342
                      ((Not::bool => bool) ((IS_SOME::'a option => bool) x))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   343
                      ((op =::'a option => 'a option => bool) x
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   344
                        (None::'a option))))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   345
               ((op &::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   346
                 ((All::('a option => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   347
                   (%x::'a option.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   348
                       (op -->::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   349
                        ((IS_SOME::'a option => bool) x)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   350
                        ((op =::'a option => 'a option => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   351
                          ((Some::'a ~=> 'a) ((the::'a option => 'a) x))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   352
                          x)))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   353
                 ((op &::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   354
                   ((All::('a option => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   355
                     (%x::'a option.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   356
                         (op =::'a option => 'a option => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   357
                          ((option_case::'a option
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   358
   => ('a ~=> 'a) => 'a option ~=> 'a)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   359
                            (None::'a option) (Some::'a ~=> 'a) x)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   360
                          x))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   361
                   ((op &::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   362
                     ((All::('a option => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   363
                       (%x::'a option.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   364
                           (op =::'a option => 'a option => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   365
                            ((option_case::'a option
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   366
     => ('a ~=> 'a) => 'a option ~=> 'a)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   367
                              x (Some::'a ~=> 'a) x)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   368
                            x))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   369
                     ((op &::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   370
                       ((All::('a option => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   371
                         (%x::'a option.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   372
                             (op -->::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   373
                              ((IS_NONE::'a option => bool) x)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   374
                              ((op =::'b => 'b => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   375
                                ((option_case::'b
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   376
         => ('a => 'b) => 'a option => 'b)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   377
                                  (e::'b) (f::'a => 'b) x)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   378
                                e)))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   379
                       ((op &::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   380
                         ((All::('a option => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   381
                           (%x::'a option.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   382
                               (op -->::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   383
                                ((IS_SOME::'a option => bool) x)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   384
                                ((op =::'b => 'b => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   385
                                  ((option_case::'b
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   386
           => ('a => 'b) => 'a option => 'b)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   387
                                    e f x)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   388
                                  (f ((the::'a option => 'a) x)))))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   389
                         ((op &::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   390
                           ((All::('a option => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   391
                             (%x::'a option.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   392
                                 (op -->::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   393
                                  ((IS_SOME::'a option => bool) x)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   394
                                  ((op =::'a option => 'a option => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   395
                                    ((option_case::'a option
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   396
             => ('a ~=> 'a) => 'a option ~=> 'a)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   397
(ea::'a option) (Some::'a ~=> 'a) x)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   398
                                    x)))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   399
                           ((op &::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   400
                             ((All::('b => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   401
                               (%u::'b.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   402
                                   (All::(('a => 'b) => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   403
                                    (%f::'a => 'b.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   404
  (op =::'b => 'b => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   405
   ((option_case::'b => ('a => 'b) => 'a option => 'b) u f
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   406
     (None::'a option))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   407
   u)))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   408
                             ((op &::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   409
                               ((All::('b => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   410
                                 (%u::'b.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   411
                                     (All::(('a => 'b) => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   412
(%f::'a => 'b.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   413
    (All::('a => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   414
     (%x::'a.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   415
         (op =::'b => 'b => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   416
          ((option_case::'b => ('a => 'b) => 'a option => 'b) u f
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   417
            ((Some::'a ~=> 'a) x))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   418
          (f x)))))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   419
                               ((op &::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   420
                                 ((All::(('a => 'b) => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   421
                                   (%f::'a => 'b.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   422
 (All::('a => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   423
  (%x::'a.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   424
      (op =::'b option => 'b option => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   425
       ((option_map::('a => 'b) => 'a option ~=> 'b) f
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   426
         ((Some::'a ~=> 'a) x))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   427
       ((Some::'b ~=> 'b) (f x)))))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   428
                                 ((op &::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   429
                                   ((All::(('a => 'b) => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   430
                                     (%f::'a => 'b.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   431
   (op =::'b option => 'b option => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   432
    ((option_map::('a => 'b) => 'a option ~=> 'b) f (None::'a option))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   433
    (None::'b option)))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   434
                                   ((op &::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   435
                                     ((op =::'a option => 'a option => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   436
 ((OPTION_JOIN::'a option option ~=> 'a) (None::'a option option))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   437
 (None::'a option))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   438
                                     ((All::('a option => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   439
 (%x::'a option.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   440
     (op =::'a option => 'a option => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   441
      ((OPTION_JOIN::'a option option ~=> 'a)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   442
        ((Some::'a option ~=> 'a option) x))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   443
      x))))))))))))))))))))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   444
  by (import option option_CLAUSES)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   445
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   446
lemma option_case_compute: "option_case (e::'b) (f::'a => 'b) (x::'a option) =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   447
(if IS_SOME x then f (the x) else e)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   448
  by (import option option_case_compute)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   449
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   450
lemma OPTION_MAP_EQ_SOME: "ALL f x y. (option_map f x = Some y) = (EX z. x = Some z & y = f z)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   451
  by (import option OPTION_MAP_EQ_SOME)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   452
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   453
lemma OPTION_JOIN_EQ_SOME: "ALL x xa. (OPTION_JOIN x = Some xa) = (x = Some (Some xa))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   454
  by (import option OPTION_JOIN_EQ_SOME)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   455
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   456
lemma option_case_cong: "ALL M M' u f.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   457
   M = M' & (M' = None --> u = u') & (ALL x. M' = Some x --> f x = f' x) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   458
   option_case u f M = option_case u' f' M'"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   459
  by (import option option_case_cong)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   460
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   461
;end_setup
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   462
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   463
;setup_theory marker
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   464
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   465
consts
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   466
  stmarker :: "'a => 'a" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   467
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   468
defs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   469
  stmarker_primdef: "stmarker == %x. x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   470
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   471
lemma stmarker_def: "ALL x. stmarker x = x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   472
  by (import marker stmarker_def)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   473
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   474
lemma move_left_conj: "ALL x xa xb.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   475
   (x & stmarker xb) = (stmarker xb & x) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   476
   ((stmarker xb & x) & xa) = (stmarker xb & x & xa) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   477
   (x & stmarker xb & xa) = (stmarker xb & x & xa)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   478
  by (import marker move_left_conj)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   479
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   480
lemma move_right_conj: "ALL x xa xb.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   481
   (stmarker xb & x) = (x & stmarker xb) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   482
   (x & xa & stmarker xb) = ((x & xa) & stmarker xb) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   483
   ((x & stmarker xb) & xa) = ((x & xa) & stmarker xb)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   484
  by (import marker move_right_conj)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   485
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   486
lemma move_left_disj: "ALL x xa xb.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   487
   (x | stmarker xb) = (stmarker xb | x) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   488
   ((stmarker xb | x) | xa) = (stmarker xb | x | xa) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   489
   (x | stmarker xb | xa) = (stmarker xb | x | xa)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   490
  by (import marker move_left_disj)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   491
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   492
lemma move_right_disj: "ALL x xa xb.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   493
   (stmarker xb | x) = (x | stmarker xb) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   494
   (x | xa | stmarker xb) = ((x | xa) | stmarker xb) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   495
   ((x | stmarker xb) | xa) = ((x | xa) | stmarker xb)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   496
  by (import marker move_right_disj)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   497
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   498
;end_setup
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   499
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   500
;setup_theory relation
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   501
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   502
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   503
  TC :: "('a => 'a => bool) => 'a => 'a => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   504
  "TC ==
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   505
%R a b.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   506
   ALL P.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   507
      (ALL x y. R x y --> P x y) & (ALL x y z. P x y & P y z --> P x z) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   508
      P a b"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   509
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   510
lemma TC_DEF: "ALL R a b.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   511
   TC R a b =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   512
   (ALL P.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   513
       (ALL x y. R x y --> P x y) & (ALL x y z. P x y & P y z --> P x z) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   514
       P a b)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   515
  by (import relation TC_DEF)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   517
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   518
  RTC :: "('a => 'a => bool) => 'a => 'a => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   519
  "RTC ==
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   520
%R a b.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   521
   ALL P. (ALL x. P x x) & (ALL x y z. R x y & P y z --> P x z) --> P a b"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   522
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   523
lemma RTC_DEF: "ALL R a b.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   524
   RTC R a b =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   525
   (ALL P. (ALL x. P x x) & (ALL x y z. R x y & P y z --> P x z) --> P a b)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   526
  by (import relation RTC_DEF)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   527
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   528
consts
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   529
  RC :: "('a => 'a => bool) => 'a => 'a => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   530
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   531
defs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   532
  RC_primdef: "RC == %R x y. x = y | R x y"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   533
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   534
lemma RC_def: "ALL R x y. RC R x y = (x = y | R x y)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   535
  by (import relation RC_def)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   536
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   537
consts
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   538
  transitive :: "('a => 'a => bool) => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   539
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   540
defs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   541
  transitive_primdef: "transitive == %R. ALL x y z. R x y & R y z --> R x z"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   542
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   543
lemma transitive_def: "ALL R. transitive R = (ALL x y z. R x y & R y z --> R x z)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   544
  by (import relation transitive_def)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   545
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   546
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   547
  pred_reflexive :: "('a => 'a => bool) => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   548
  "pred_reflexive == %R. ALL x. R x x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   549
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   550
lemma reflexive_def: "ALL R. pred_reflexive R = (ALL x. R x x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   551
  by (import relation reflexive_def)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   552
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   553
lemma TC_TRANSITIVE: "ALL x. transitive (TC x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   554
  by (import relation TC_TRANSITIVE)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   555
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   556
lemma RTC_INDUCT: "ALL x xa.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   557
   (ALL x. xa x x) & (ALL xb y z. x xb y & xa y z --> xa xb z) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   558
   (ALL xb xc. RTC x xb xc --> xa xb xc)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   559
  by (import relation RTC_INDUCT)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   560
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   561
lemma TC_RULES: "ALL x.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   562
   (ALL xa xb. x xa xb --> TC x xa xb) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   563
   (ALL xa xb xc. TC x xa xb & TC x xb xc --> TC x xa xc)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   564
  by (import relation TC_RULES)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   565
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   566
lemma RTC_RULES: "ALL x.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   567
   (ALL xa. RTC x xa xa) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   568
   (ALL xa xb xc. x xa xb & RTC x xb xc --> RTC x xa xc)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   569
  by (import relation RTC_RULES)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   570
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   571
lemma RTC_STRONG_INDUCT: "ALL R P.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   572
   (ALL x. P x x) & (ALL x y z. R x y & RTC R y z & P y z --> P x z) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   573
   (ALL x y. RTC R x y --> P x y)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   574
  by (import relation RTC_STRONG_INDUCT)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   575
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   576
lemma RTC_RTC: "ALL R x y. RTC R x y --> (ALL z. RTC R y z --> RTC R x z)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   577
  by (import relation RTC_RTC)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   578
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   579
lemma RTC_TRANSITIVE: "ALL x. transitive (RTC x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   580
  by (import relation RTC_TRANSITIVE)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   581
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   582
lemma RTC_REFLEXIVE: "ALL R. pred_reflexive (RTC R)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   583
  by (import relation RTC_REFLEXIVE)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   584
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   585
lemma RC_REFLEXIVE: "ALL R. pred_reflexive (RC R)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   586
  by (import relation RC_REFLEXIVE)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   587
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   588
lemma TC_SUBSET: "ALL x xa xb. x xa xb --> TC x xa xb"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   589
  by (import relation TC_SUBSET)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   590
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   591
lemma RTC_SUBSET: "ALL R x y. R x y --> RTC R x y"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   592
  by (import relation RTC_SUBSET)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   593
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   594
lemma RC_SUBSET: "ALL R x y. R x y --> RC R x y"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   595
  by (import relation RC_SUBSET)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   596
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   597
lemma RC_RTC: "ALL R x y. RC R x y --> RTC R x y"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   598
  by (import relation RC_RTC)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   599
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   600
lemma TC_INDUCT: "ALL x xa.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   601
   (ALL xb y. x xb y --> xa xb y) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   602
   (ALL x y z. xa x y & xa y z --> xa x z) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   603
   (ALL xb xc. TC x xb xc --> xa xb xc)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   604
  by (import relation TC_INDUCT)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   605
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   606
lemma TC_INDUCT_LEFT1: "ALL x xa.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   607
   (ALL xb y. x xb y --> xa xb y) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   608
   (ALL xb y z. x xb y & xa y z --> xa xb z) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   609
   (ALL xb xc. TC x xb xc --> xa xb xc)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   610
  by (import relation TC_INDUCT_LEFT1)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   611
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   612
lemma TC_STRONG_INDUCT: "ALL R P.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   613
   (ALL x y. R x y --> P x y) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   614
   (ALL x y z. P x y & P y z & TC R x y & TC R y z --> P x z) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   615
   (ALL u v. TC R u v --> P u v)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   616
  by (import relation TC_STRONG_INDUCT)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   617
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   618
lemma TC_STRONG_INDUCT_LEFT1: "ALL R P.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   619
   (ALL x y. R x y --> P x y) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   620
   (ALL x y z. R x y & P y z & TC R y z --> P x z) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   621
   (ALL u v. TC R u v --> P u v)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   622
  by (import relation TC_STRONG_INDUCT_LEFT1)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   623
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   624
lemma TC_RTC: "ALL R x y. TC R x y --> RTC R x y"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   625
  by (import relation TC_RTC)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   626
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   627
lemma RTC_TC_RC: "ALL R x y. RTC R x y --> RC R x y | TC R x y"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   628
  by (import relation RTC_TC_RC)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   629
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   630
lemma TC_RC_EQNS: "ALL R. RC (TC R) = RTC R & TC (RC R) = RTC R"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   631
  by (import relation TC_RC_EQNS)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   632
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   633
lemma RC_IDEM: "ALL R. RC (RC R) = RC R"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   634
  by (import relation RC_IDEM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   635
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   636
lemma TC_IDEM: "ALL R. TC (TC R) = TC R"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   637
  by (import relation TC_IDEM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   638
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   639
lemma RTC_IDEM: "ALL R. RTC (RTC R) = RTC R"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   640
  by (import relation RTC_IDEM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   641
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   642
lemma RTC_CASES1: "ALL x xa xb. RTC x xa xb = (xa = xb | (EX u. x xa u & RTC x u xb))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   643
  by (import relation RTC_CASES1)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   644
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   645
lemma RTC_CASES2: "ALL x xa xb. RTC x xa xb = (xa = xb | (EX u. RTC x xa u & x u xb))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   646
  by (import relation RTC_CASES2)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   647
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   648
lemma RTC_CASES_RTC_TWICE: "ALL x xa xb. RTC x xa xb = (EX u. RTC x xa u & RTC x u xb)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   649
  by (import relation RTC_CASES_RTC_TWICE)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   650
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   651
lemma TC_CASES1: "ALL R x z. TC R x z --> R x z | (EX y. R x y & TC R y z)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   652
  by (import relation TC_CASES1)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   653
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   654
lemma TC_CASES2: "ALL R x z. TC R x z --> R x z | (EX y. TC R x y & R y z)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   655
  by (import relation TC_CASES2)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   656
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   657
lemma TC_MONOTONE: "ALL R Q. (ALL x y. R x y --> Q x y) --> (ALL x y. TC R x y --> TC Q x y)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   658
  by (import relation TC_MONOTONE)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   659
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   660
lemma RTC_MONOTONE: "ALL R Q. (ALL x y. R x y --> Q x y) --> (ALL x y. RTC R x y --> RTC Q x y)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   661
  by (import relation RTC_MONOTONE)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   662
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   663
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   664
  WF :: "('a => 'a => bool) => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   665
  "WF == %R. ALL B. Ex B --> (EX min. B min & (ALL b. R b min --> ~ B b))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   666
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   667
lemma WF_DEF: "ALL R. WF R = (ALL B. Ex B --> (EX min. B min & (ALL b. R b min --> ~ B b)))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   668
  by (import relation WF_DEF)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   669
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   670
lemma WF_INDUCTION_THM: "ALL R. WF R --> (ALL P. (ALL x. (ALL y. R y x --> P y) --> P x) --> All P)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   671
  by (import relation WF_INDUCTION_THM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   672
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   673
lemma WF_NOT_REFL: "ALL x xa xb. WF x --> x xa xb --> xa ~= xb"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   674
  by (import relation WF_NOT_REFL)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   675
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   676
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   677
  EMPTY_REL :: "'a => 'a => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   678
  "EMPTY_REL == %x y. False"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   679
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   680
lemma EMPTY_REL_DEF: "ALL x y. EMPTY_REL x y = False"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   681
  by (import relation EMPTY_REL_DEF)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   682
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   683
lemma WF_EMPTY_REL: "WF EMPTY_REL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   684
  by (import relation WF_EMPTY_REL)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   685
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   686
lemma WF_SUBSET: "ALL x xa. WF x & (ALL xb y. xa xb y --> x xb y) --> WF xa"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   687
  by (import relation WF_SUBSET)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   688
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   689
lemma WF_TC: "ALL R. WF R --> WF (TC R)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   690
  by (import relation WF_TC)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   691
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   692
consts
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   693
  inv_image :: "('b => 'b => bool) => ('a => 'b) => 'a => 'a => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   694
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   695
defs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   696
  inv_image_primdef: "relation.inv_image ==
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   697
%(R::'b => 'b => bool) (f::'a => 'b) (x::'a) y::'a. R (f x) (f y)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   698
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   699
lemma inv_image_def: "ALL (R::'b => 'b => bool) f::'a => 'b.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   700
   relation.inv_image R f = (%(x::'a) y::'a. R (f x) (f y))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   701
  by (import relation inv_image_def)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   702
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   703
lemma WF_inv_image: "ALL (R::'b => 'b => bool) f::'a => 'b. WF R --> WF (relation.inv_image R f)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   704
  by (import relation WF_inv_image)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   705
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   706
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   707
  RESTRICT :: "('a => 'b) => ('a => 'a => bool) => 'a => 'a => 'b" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   708
  "RESTRICT == %f R x y. if R y x then f y else ARB"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   709
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   710
lemma RESTRICT_DEF: "ALL f R x. RESTRICT f R x = (%y. if R y x then f y else ARB)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   711
  by (import relation RESTRICT_DEF)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   712
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   713
lemma RESTRICT_LEMMA: "ALL x xa xb xc. xa xb xc --> RESTRICT x xa xc xb = x xb"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   714
  by (import relation RESTRICT_LEMMA)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   715
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   716
consts
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   717
  approx :: "('a => 'a => bool) => (('a => 'b) => 'a => 'b) => 'a => ('a => 'b) => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   718
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   719
defs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   720
  approx_primdef: "approx == %R M x f. f = RESTRICT (%y. M (RESTRICT f R y) y) R x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   721
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   722
lemma approx_def: "ALL R M x f. approx R M x f = (f = RESTRICT (%y. M (RESTRICT f R y) y) R x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   723
  by (import relation approx_def)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   724
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   725
consts
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   726
  the_fun :: "('a => 'a => bool) => (('a => 'b) => 'a => 'b) => 'a => 'a => 'b" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   727
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   728
defs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   729
  the_fun_primdef: "the_fun == %R M x. Eps (approx R M x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   730
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   731
lemma the_fun_def: "ALL R M x. the_fun R M x = Eps (approx R M x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   732
  by (import relation the_fun_def)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   733
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   734
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   735
  WFREC :: "('a => 'a => bool) => (('a => 'b) => 'a => 'b) => 'a => 'b" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   736
  "WFREC ==
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   737
%R M x. M (RESTRICT (the_fun (TC R) (%f v. M (RESTRICT f R v) v) x) R x) x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   738
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   739
lemma WFREC_DEF: "ALL R M.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   740
   WFREC R M =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   741
   (%x. M (RESTRICT (the_fun (TC R) (%f v. M (RESTRICT f R v) v) x) R x) x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   742
  by (import relation WFREC_DEF)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   743
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   744
lemma WFREC_THM: "ALL R M. WF R --> (ALL x. WFREC R M x = M (RESTRICT (WFREC R M) R x) x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   745
  by (import relation WFREC_THM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   746
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   747
lemma WFREC_COROLLARY: "ALL M R f. f = WFREC R M --> WF R --> (ALL x. f x = M (RESTRICT f R x) x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   748
  by (import relation WFREC_COROLLARY)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   749
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   750
lemma WF_RECURSION_THM: "ALL R. WF R --> (ALL M. EX! f. ALL x. f x = M (RESTRICT f R x) x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   751
  by (import relation WF_RECURSION_THM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   752
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   753
;end_setup
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   754
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   755
;setup_theory pair
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   756
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   757
lemma CURRY_ONE_ONE_THM: "(curry f = curry g) = (f = g)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   758
  by (import pair CURRY_ONE_ONE_THM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   759
15647
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
   760
lemma UNCURRY_ONE_ONE_THM: "(op =::bool => bool => bool)
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
   761
 ((op =::('a * 'b => 'c) => ('a * 'b => 'c) => bool)
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
   762
   ((split::('a => 'b => 'c) => 'a * 'b => 'c) (f::'a => 'b => 'c))
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
   763
   ((split::('a => 'b => 'c) => 'a * 'b => 'c) (g::'a => 'b => 'c)))
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
   764
 ((op =::('a => 'b => 'c) => ('a => 'b => 'c) => bool) f g)"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   765
  by (import pair UNCURRY_ONE_ONE_THM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   766
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   767
lemma pair_Axiom: "ALL f. EX x. ALL xa y. x (xa, y) = f xa y"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   768
  by (import pair pair_Axiom)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   769
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   770
lemma UNCURRY_CONG: "ALL M M' f.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   771
   M = M' & (ALL x y. M' = (x, y) --> f x y = f' x y) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   772
   split f M = split f' M'"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   773
  by (import pair UNCURRY_CONG)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   774
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   775
lemma ELIM_PEXISTS: "(EX p. P (fst p) (snd p)) = (EX p1. Ex (P p1))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   776
  by (import pair ELIM_PEXISTS)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   777
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   778
lemma ELIM_PFORALL: "(ALL p. P (fst p) (snd p)) = (ALL p1. All (P p1))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   779
  by (import pair ELIM_PFORALL)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   780
15647
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
   781
lemma PFORALL_THM: "(All::(('a => 'b => bool) => bool) => bool)
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
   782
 (%x::'a => 'b => bool.
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
   783
     (op =::bool => bool => bool)
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
   784
      ((All::('a => bool) => bool)
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
   785
        (%xa::'a. (All::('b => bool) => bool) (x xa)))
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
   786
      ((All::('a * 'b => bool) => bool)
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
   787
        ((split::('a => 'b => bool) => 'a * 'b => bool) x)))"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   788
  by (import pair PFORALL_THM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   789
15647
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
   790
lemma PEXISTS_THM: "(All::(('a => 'b => bool) => bool) => bool)
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
   791
 (%x::'a => 'b => bool.
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
   792
     (op =::bool => bool => bool)
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
   793
      ((Ex::('a => bool) => bool)
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
   794
        (%xa::'a. (Ex::('b => bool) => bool) (x xa)))
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
   795
      ((Ex::('a * 'b => bool) => bool)
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
   796
        ((split::('a => 'b => bool) => 'a * 'b => bool) x)))"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   797
  by (import pair PEXISTS_THM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   798
15647
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
   799
lemma LET2_RAND: "(All::(('c => 'd) => bool) => bool)
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
   800
 (%x::'c => 'd.
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
   801
     (All::('a * 'b => bool) => bool)
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
   802
      (%xa::'a * 'b.
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
   803
          (All::(('a => 'b => 'c) => bool) => bool)
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
   804
           (%xb::'a => 'b => 'c.
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
   805
               (op =::'d => 'd => bool)
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
   806
                (x ((Let::'a * 'b => ('a * 'b => 'c) => 'c) xa
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
   807
                     ((split::('a => 'b => 'c) => 'a * 'b => 'c) xb)))
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
   808
                ((Let::'a * 'b => ('a * 'b => 'd) => 'd) xa
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
   809
                  ((split::('a => 'b => 'd) => 'a * 'b => 'd)
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
   810
                    (%(xa::'a) y::'b. x (xb xa y)))))))"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   811
  by (import pair LET2_RAND)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   812
15647
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
   813
lemma LET2_RATOR: "(All::('a1 * 'a2 => bool) => bool)
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
   814
 (%x::'a1 * 'a2.
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
   815
     (All::(('a1 => 'a2 => 'b => 'c) => bool) => bool)
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
   816
      (%xa::'a1 => 'a2 => 'b => 'c.
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
   817
          (All::('b => bool) => bool)
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
   818
           (%xb::'b.
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
   819
               (op =::'c => 'c => bool)
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
   820
                ((Let::'a1 * 'a2 => ('a1 * 'a2 => 'b => 'c) => 'b => 'c) x
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
   821
                  ((split::('a1 => 'a2 => 'b => 'c)
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
   822
                           => 'a1 * 'a2 => 'b => 'c)
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
   823
                    xa)
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
   824
                  xb)
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
   825
                ((Let::'a1 * 'a2 => ('a1 * 'a2 => 'c) => 'c) x
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
   826
                  ((split::('a1 => 'a2 => 'c) => 'a1 * 'a2 => 'c)
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
   827
                    (%(x::'a1) y::'a2. xa x y xb))))))"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   828
  by (import pair LET2_RATOR)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   829
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   830
lemma pair_case_cong: "ALL x xa xb.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   831
   x = xa & (ALL x y. xa = (x, y) --> xb x y = f' x y) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   832
   split xb x = split f' xa"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   833
  by (import pair pair_case_cong)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   834
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   835
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   836
  LEX :: "('a => 'a => bool) => ('b => 'b => bool) => 'a * 'b => 'a * 'b => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   837
  "LEX == %R1 R2 (s, t) (u, v). R1 s u | s = u & R2 t v"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   838
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   839
lemma LEX_DEF: "ALL R1 R2. LEX R1 R2 = (%(s, t) (u, v). R1 s u | s = u & R2 t v)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   840
  by (import pair LEX_DEF)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   841
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   842
lemma WF_LEX: "ALL x xa. WF x & WF xa --> WF (LEX x xa)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   843
  by (import pair WF_LEX)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   844
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   845
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   846
  RPROD :: "('a => 'a => bool) => ('b => 'b => bool) => 'a * 'b => 'a * 'b => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   847
  "RPROD == %R1 R2 (s, t) (u, v). R1 s u & R2 t v"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   848
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   849
lemma RPROD_DEF: "ALL R1 R2. RPROD R1 R2 = (%(s, t) (u, v). R1 s u & R2 t v)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   850
  by (import pair RPROD_DEF)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   851
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   852
lemma WF_RPROD: "ALL R Q. WF R & WF Q --> WF (RPROD R Q)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   853
  by (import pair WF_RPROD)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   854
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   855
;end_setup
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   856
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   857
;setup_theory num
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   858
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   859
;end_setup
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   860
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   861
;setup_theory prim_rec
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   862
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   863
lemma LESS_0_0: "0 < Suc 0"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   864
  by (import prim_rec LESS_0_0)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   865
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   866
lemma LESS_LEMMA1: "ALL x xa. x < Suc xa --> x = xa | x < xa"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   867
  by (import prim_rec LESS_LEMMA1)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   868
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   869
lemma LESS_LEMMA2: "ALL m n. m = n | m < n --> m < Suc n"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   870
  by (import prim_rec LESS_LEMMA2)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   871
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   872
lemma LESS_THM: "ALL m n. (m < Suc n) = (m = n | m < n)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   873
  by (import prim_rec LESS_THM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   874
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   875
lemma LESS_SUC_IMP: "ALL x xa. x < Suc xa --> x ~= xa --> x < xa"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   876
  by (import prim_rec LESS_SUC_IMP)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   877
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   878
lemma EQ_LESS: "ALL n. Suc m = n --> m < n"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   879
  by (import prim_rec EQ_LESS)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   880
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   881
lemma NOT_LESS_EQ: "ALL (m::nat) n::nat. m = n --> ~ m < n"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   882
  by (import prim_rec NOT_LESS_EQ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   883
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   884
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   885
  SIMP_REC_REL :: "(nat => 'a) => 'a => ('a => 'a) => nat => bool" 
14847
44d92c12b255 updated;
wenzelm
parents: 14684
diff changeset
   886
  "(op ==::((nat => 'a) => 'a => ('a => 'a) => nat => bool)
44d92c12b255 updated;
wenzelm
parents: 14684
diff changeset
   887
        => ((nat => 'a) => 'a => ('a => 'a) => nat => bool) => prop)
44d92c12b255 updated;
wenzelm
parents: 14684
diff changeset
   888
 (SIMP_REC_REL::(nat => 'a) => 'a => ('a => 'a) => nat => bool)
44d92c12b255 updated;
wenzelm
parents: 14684
diff changeset
   889
 (%(fun::nat => 'a) (x::'a) (f::'a => 'a) n::nat.
44d92c12b255 updated;
wenzelm
parents: 14684
diff changeset
   890
     (op &::bool => bool => bool)
44d92c12b255 updated;
wenzelm
parents: 14684
diff changeset
   891
      ((op =::'a => 'a => bool) (fun (0::nat)) x)
44d92c12b255 updated;
wenzelm
parents: 14684
diff changeset
   892
      ((All::(nat => bool) => bool)
44d92c12b255 updated;
wenzelm
parents: 14684
diff changeset
   893
        (%m::nat.
44d92c12b255 updated;
wenzelm
parents: 14684
diff changeset
   894
            (op -->::bool => bool => bool) ((op <::nat => nat => bool) m n)
44d92c12b255 updated;
wenzelm
parents: 14684
diff changeset
   895
             ((op =::'a => 'a => bool) (fun ((Suc::nat => nat) m))
44d92c12b255 updated;
wenzelm
parents: 14684
diff changeset
   896
               (f (fun m))))))"
44d92c12b255 updated;
wenzelm
parents: 14684
diff changeset
   897
44d92c12b255 updated;
wenzelm
parents: 14684
diff changeset
   898
lemma SIMP_REC_REL: "(All::((nat => 'a) => bool) => bool)
44d92c12b255 updated;
wenzelm
parents: 14684
diff changeset
   899
 (%fun::nat => 'a.
44d92c12b255 updated;
wenzelm
parents: 14684
diff changeset
   900
     (All::('a => bool) => bool)
44d92c12b255 updated;
wenzelm
parents: 14684
diff changeset
   901
      (%x::'a.
44d92c12b255 updated;
wenzelm
parents: 14684
diff changeset
   902
          (All::(('a => 'a) => bool) => bool)
44d92c12b255 updated;
wenzelm
parents: 14684
diff changeset
   903
           (%f::'a => 'a.
44d92c12b255 updated;
wenzelm
parents: 14684
diff changeset
   904
               (All::(nat => bool) => bool)
44d92c12b255 updated;
wenzelm
parents: 14684
diff changeset
   905
                (%n::nat.
44d92c12b255 updated;
wenzelm
parents: 14684
diff changeset
   906
                    (op =::bool => bool => bool)
44d92c12b255 updated;
wenzelm
parents: 14684
diff changeset
   907
                     ((SIMP_REC_REL::(nat => 'a)
44d92c12b255 updated;
wenzelm
parents: 14684
diff changeset
   908
                                     => 'a => ('a => 'a) => nat => bool)
44d92c12b255 updated;
wenzelm
parents: 14684
diff changeset
   909
                       fun x f n)
44d92c12b255 updated;
wenzelm
parents: 14684
diff changeset
   910
                     ((op &::bool => bool => bool)
44d92c12b255 updated;
wenzelm
parents: 14684
diff changeset
   911
                       ((op =::'a => 'a => bool) (fun (0::nat)) x)
44d92c12b255 updated;
wenzelm
parents: 14684
diff changeset
   912
                       ((All::(nat => bool) => bool)
44d92c12b255 updated;
wenzelm
parents: 14684
diff changeset
   913
                         (%m::nat.
44d92c12b255 updated;
wenzelm
parents: 14684
diff changeset
   914
                             (op -->::bool => bool => bool)
44d92c12b255 updated;
wenzelm
parents: 14684
diff changeset
   915
                              ((op <::nat => nat => bool) m n)
44d92c12b255 updated;
wenzelm
parents: 14684
diff changeset
   916
                              ((op =::'a => 'a => bool)
44d92c12b255 updated;
wenzelm
parents: 14684
diff changeset
   917
                                (fun ((Suc::nat => nat) m))
44d92c12b255 updated;
wenzelm
parents: 14684
diff changeset
   918
                                (f (fun m))))))))))"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   919
  by (import prim_rec SIMP_REC_REL)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   920
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   921
lemma SIMP_REC_EXISTS: "ALL x f n. EX fun. SIMP_REC_REL fun x f n"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   922
  by (import prim_rec SIMP_REC_EXISTS)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   923
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   924
lemma SIMP_REC_REL_UNIQUE: "ALL x xa xb xc xd xe.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   925
   SIMP_REC_REL xb x xa xd & SIMP_REC_REL xc x xa xe -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   926
   (ALL n. n < xd & n < xe --> xb n = xc n)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   927
  by (import prim_rec SIMP_REC_REL_UNIQUE)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   928
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   929
lemma SIMP_REC_REL_UNIQUE_RESULT: "ALL x f n. EX! y. EX g. SIMP_REC_REL g x f (Suc n) & y = g n"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   930
  by (import prim_rec SIMP_REC_REL_UNIQUE_RESULT)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   931
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   932
consts
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   933
  SIMP_REC :: "'a => ('a => 'a) => nat => 'a" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   934
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   935
specification (SIMP_REC) SIMP_REC: "ALL x f' n. EX g. SIMP_REC_REL g x f' (Suc n) & SIMP_REC x f' n = g n"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   936
  by (import prim_rec SIMP_REC)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   937
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   938
lemma LESS_SUC_SUC: "ALL m. m < Suc m & m < Suc (Suc m)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   939
  by (import prim_rec LESS_SUC_SUC)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   940
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   941
lemma SIMP_REC_THM: "ALL x f.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   942
   SIMP_REC x f 0 = x & (ALL m. SIMP_REC x f (Suc m) = f (SIMP_REC x f m))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   943
  by (import prim_rec SIMP_REC_THM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   944
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   945
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   946
  PRE :: "nat => nat" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   947
  "PRE == %m. if m = 0 then 0 else SOME n. m = Suc n"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   948
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   949
lemma PRE_DEF: "ALL m. PRE m = (if m = 0 then 0 else SOME n. m = Suc n)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   950
  by (import prim_rec PRE_DEF)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   951
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   952
lemma PRE: "PRE 0 = 0 & (ALL m. PRE (Suc m) = m)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   953
  by (import prim_rec PRE)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   954
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   955
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   956
  PRIM_REC_FUN :: "'a => ('a => nat => 'a) => nat => nat => 'a" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   957
  "PRIM_REC_FUN == %x f. SIMP_REC (%n. x) (%fun n. f (fun (PRE n)) n)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   958
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   959
lemma PRIM_REC_FUN: "ALL x f. PRIM_REC_FUN x f = SIMP_REC (%n. x) (%fun n. f (fun (PRE n)) n)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   960
  by (import prim_rec PRIM_REC_FUN)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   961
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   962
lemma PRIM_REC_EQN: "ALL x f.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   963
   (ALL n. PRIM_REC_FUN x f 0 n = x) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   964
   (ALL m n. PRIM_REC_FUN x f (Suc m) n = f (PRIM_REC_FUN x f m (PRE n)) n)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   965
  by (import prim_rec PRIM_REC_EQN)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   966
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   967
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   968
  PRIM_REC :: "'a => ('a => nat => 'a) => nat => 'a" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   969
  "PRIM_REC == %x f m. PRIM_REC_FUN x f m (PRE m)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   970
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   971
lemma PRIM_REC: "ALL x f m. PRIM_REC x f m = PRIM_REC_FUN x f m (PRE m)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   972
  by (import prim_rec PRIM_REC)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   973
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   974
lemma PRIM_REC_THM: "ALL x f.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   975
   PRIM_REC x f 0 = x & (ALL m. PRIM_REC x f (Suc m) = f (PRIM_REC x f m) m)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   976
  by (import prim_rec PRIM_REC_THM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   977
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   978
lemma DC: "ALL P R a.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   979
   P a & (ALL x. P x --> (EX y. P y & R x y)) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   980
   (EX x. x 0 = a & (ALL n. P (x n) & R (x n) (x (Suc n))))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   981
  by (import prim_rec DC)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   982
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   983
lemma num_Axiom_old: "ALL e f. EX! fn1. fn1 0 = e & (ALL n. fn1 (Suc n) = f (fn1 n) n)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   984
  by (import prim_rec num_Axiom_old)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   985
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   986
lemma num_Axiom: "ALL e f. EX x. x 0 = e & (ALL n. x (Suc n) = f n (x n))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   987
  by (import prim_rec num_Axiom)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   988
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   989
consts
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   990
  wellfounded :: "('a => 'a => bool) => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   991
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   992
defs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   993
  wellfounded_primdef: "wellfounded == %R. ~ (EX f. ALL n. R (f (Suc n)) (f n))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   994
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   995
lemma wellfounded_def: "ALL R. wellfounded R = (~ (EX f. ALL n. R (f (Suc n)) (f n)))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   996
  by (import prim_rec wellfounded_def)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   997
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   998
lemma WF_IFF_WELLFOUNDED: "ALL R. WF R = wellfounded R"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   999
  by (import prim_rec WF_IFF_WELLFOUNDED)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1000
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1001
lemma WF_PRED: "WF (%x y. y = Suc x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1002
  by (import prim_rec WF_PRED)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1003
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1004
lemma WF_LESS: "(WF::(nat => nat => bool) => bool) (op <::nat => nat => bool)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1005
  by (import prim_rec WF_LESS)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1006
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1007
consts
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1008
  measure :: "('a => nat) => 'a => 'a => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1009
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1010
defs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1011
  measure_primdef: "prim_rec.measure == relation.inv_image op <"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1012
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1013
lemma measure_def: "prim_rec.measure = relation.inv_image op <"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1014
  by (import prim_rec measure_def)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1015
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1016
lemma WF_measure: "ALL x. WF (prim_rec.measure x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1017
  by (import prim_rec WF_measure)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1018
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1019
lemma measure_thm: "ALL x xa xb. prim_rec.measure x xa xb = (x xa < x xb)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1020
  by (import prim_rec measure_thm)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1021
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1022
;end_setup
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1023
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1024
;setup_theory arithmetic
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1025
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1026
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1027
  nat_elim__magic :: "nat => nat" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1028
  "nat_elim__magic == %n. n"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1029
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1030
lemma nat_elim__magic: "ALL n. nat_elim__magic n = n"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1031
  by (import arithmetic nat_elim__magic)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1032
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1033
consts
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1034
  EVEN :: "nat => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1035
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1036
specification (EVEN) EVEN: "EVEN 0 = True & (ALL n. EVEN (Suc n) = (~ EVEN n))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1037
  by (import arithmetic EVEN)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1038
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1039
consts
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1040
  ODD :: "nat => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1041
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1042
specification (ODD) ODD: "ODD 0 = False & (ALL n. ODD (Suc n) = (~ ODD n))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1043
  by (import arithmetic ODD)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1044
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1045
lemma TWO: "2 = Suc 1"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1046
  by (import arithmetic TWO)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1047
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1048
lemma NORM_0: "(0::nat) = (0::nat)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1049
  by (import arithmetic NORM_0)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1050
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1051
lemma num_case_compute: "ALL n. nat_case f g n = (if n = 0 then f else g (PRE n))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1052
  by (import arithmetic num_case_compute)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1053
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1054
lemma ADD_CLAUSES: "0 + m = m & m + 0 = m & Suc m + n = Suc (m + n) & m + Suc n = Suc (m + n)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1055
  by (import arithmetic ADD_CLAUSES)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1056
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1057
lemma LESS_ADD: "ALL (m::nat) n::nat. n < m --> (EX p::nat. p + n = m)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1058
  by (import arithmetic LESS_ADD)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1059
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1060
lemma LESS_ANTISYM: "ALL (m::nat) n::nat. ~ (m < n & n < m)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1061
  by (import arithmetic LESS_ANTISYM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1062
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1063
lemma LESS_LESS_SUC: "ALL x xa. ~ (x < xa & xa < Suc x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1064
  by (import arithmetic LESS_LESS_SUC)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1065
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1066
lemma FUN_EQ_LEMMA: "ALL f x1 x2. f x1 & ~ f x2 --> x1 ~= x2"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1067
  by (import arithmetic FUN_EQ_LEMMA)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1068
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1069
lemma LESS_NOT_SUC: "ALL m n. m < n & n ~= Suc m --> Suc m < n"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1070
  by (import arithmetic LESS_NOT_SUC)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1071
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1072
lemma LESS_0_CASES: "ALL m::nat. (0::nat) = m | (0::nat) < m"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1073
  by (import arithmetic LESS_0_CASES)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1074
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1075
lemma LESS_CASES_IMP: "ALL (m::nat) n::nat. ~ m < n & m ~= n --> n < m"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1076
  by (import arithmetic LESS_CASES_IMP)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1077
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1078
lemma LESS_CASES: "ALL (m::nat) n::nat. m < n | n <= m"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1079
  by (import arithmetic LESS_CASES)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1080
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1081
lemma LESS_EQ_SUC_REFL: "ALL m. m <= Suc m"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1082
  by (import arithmetic LESS_EQ_SUC_REFL)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1083
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1084
lemma LESS_ADD_NONZERO: "ALL (m::nat) n::nat. n ~= (0::nat) --> m < m + n"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1085
  by (import arithmetic LESS_ADD_NONZERO)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1086
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1087
lemma LESS_EQ_ANTISYM: "ALL (x::nat) xa::nat. ~ (x < xa & xa <= x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1088
  by (import arithmetic LESS_EQ_ANTISYM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1089
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1090
lemma SUB_0: "ALL m::nat. (0::nat) - m = (0::nat) & m - (0::nat) = m"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1091
  by (import arithmetic SUB_0)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1092
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1093
lemma SUC_SUB1: "ALL m. Suc m - 1 = m"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1094
  by (import arithmetic SUC_SUB1)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1095
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1096
lemma PRE_SUB1: "ALL m. PRE m = m - 1"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1097
  by (import arithmetic PRE_SUB1)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1098
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1099
lemma MULT_CLAUSES: "ALL x xa.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1100
   0 * x = 0 &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1101
   x * 0 = 0 &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1102
   1 * x = x &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1103
   x * 1 = x & Suc x * xa = x * xa + xa & x * Suc xa = x + x * xa"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1104
  by (import arithmetic MULT_CLAUSES)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1105
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1106
lemma PRE_SUB: "ALL m n. PRE (m - n) = PRE m - n"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1107
  by (import arithmetic PRE_SUB)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1108
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1109
lemma ADD_EQ_1: "ALL (m::nat) n::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1110
   (m + n = (1::nat)) =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1111
   (m = (1::nat) & n = (0::nat) | m = (0::nat) & n = (1::nat))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1112
  by (import arithmetic ADD_EQ_1)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1113
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1114
lemma ADD_INV_0_EQ: "ALL (m::nat) n::nat. (m + n = m) = (n = (0::nat))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1115
  by (import arithmetic ADD_INV_0_EQ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1116
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1117
lemma PRE_SUC_EQ: "ALL m n. 0 < n --> (m = PRE n) = (Suc m = n)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1118
  by (import arithmetic PRE_SUC_EQ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1119
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1120
lemma INV_PRE_EQ: "ALL m n. 0 < m & 0 < n --> (PRE m = PRE n) = (m = n)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1121
  by (import arithmetic INV_PRE_EQ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1122
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1123
lemma LESS_SUC_NOT: "ALL m n. m < n --> ~ n < Suc m"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1124
  by (import arithmetic LESS_SUC_NOT)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1125
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1126
lemma ADD_EQ_SUB: "ALL (m::nat) (n::nat) p::nat. n <= p --> (m + n = p) = (m = p - n)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1127
  by (import arithmetic ADD_EQ_SUB)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1128
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1129
lemma LESS_ADD_1: "ALL (x::nat) xa::nat. xa < x --> (EX xb::nat. x = xa + (xb + (1::nat)))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1130
  by (import arithmetic LESS_ADD_1)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1131
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1132
lemma NOT_ODD_EQ_EVEN: "ALL n m. Suc (n + n) ~= m + m"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1133
  by (import arithmetic NOT_ODD_EQ_EVEN)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1134
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1135
lemma MULT_SUC_EQ: "ALL p m n. (n * Suc p = m * Suc p) = (n = m)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1136
  by (import arithmetic MULT_SUC_EQ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1137
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1138
lemma MULT_EXP_MONO: "ALL p q n m. (n * Suc q ^ p = m * Suc q ^ p) = (n = m)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1139
  by (import arithmetic MULT_EXP_MONO)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1140
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1141
lemma LESS_ADD_SUC: "ALL m n. m < m + Suc n"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1142
  by (import arithmetic LESS_ADD_SUC)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1143
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1144
lemma LESS_OR_EQ_ADD: "ALL (n::nat) m::nat. n < m | (EX p::nat. n = p + m)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1145
  by (import arithmetic LESS_OR_EQ_ADD)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1146
14847
44d92c12b255 updated;
wenzelm
parents: 14684
diff changeset
  1147
lemma WOP: "(All::((nat => bool) => bool) => bool)
44d92c12b255 updated;
wenzelm
parents: 14684
diff changeset
  1148
 (%P::nat => bool.
44d92c12b255 updated;
wenzelm
parents: 14684
diff changeset
  1149
     (op -->::bool => bool => bool) ((Ex::(nat => bool) => bool) P)
44d92c12b255 updated;
wenzelm
parents: 14684
diff changeset
  1150
      ((Ex::(nat => bool) => bool)
44d92c12b255 updated;
wenzelm
parents: 14684
diff changeset
  1151
        (%n::nat.
44d92c12b255 updated;
wenzelm
parents: 14684
diff changeset
  1152
            (op &::bool => bool => bool) (P n)
44d92c12b255 updated;
wenzelm
parents: 14684
diff changeset
  1153
             ((All::(nat => bool) => bool)
44d92c12b255 updated;
wenzelm
parents: 14684
diff changeset
  1154
               (%m::nat.
44d92c12b255 updated;
wenzelm
parents: 14684
diff changeset
  1155
                   (op -->::bool => bool => bool)
44d92c12b255 updated;
wenzelm
parents: 14684
diff changeset
  1156
                    ((op <::nat => nat => bool) m n)
44d92c12b255 updated;
wenzelm
parents: 14684
diff changeset
  1157
                    ((Not::bool => bool) (P m)))))))"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1158
  by (import arithmetic WOP)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1159
15647
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
  1160
lemma INV_PRE_LESS: "ALL m>0. ALL n. (PRE m < PRE n) = (m < n)"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1161
  by (import arithmetic INV_PRE_LESS)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1162
15647
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
  1163
lemma INV_PRE_LESS_EQ: "ALL n>0. ALL m. (PRE m <= PRE n) = (m <= n)"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1164
  by (import arithmetic INV_PRE_LESS_EQ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1165
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1166
lemma SUB_EQ_EQ_0: "ALL (m::nat) n::nat. (m - n = m) = (m = (0::nat) | n = (0::nat))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1167
  by (import arithmetic SUB_EQ_EQ_0)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1168
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1169
lemma SUB_LESS_OR: "ALL (m::nat) n::nat. n < m --> n <= m - (1::nat)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1170
  by (import arithmetic SUB_LESS_OR)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1171
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1172
lemma LESS_SUB_ADD_LESS: "ALL (n::nat) (m::nat) i::nat. i < n - m --> i + m < n"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1173
  by (import arithmetic LESS_SUB_ADD_LESS)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1174
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1175
lemma LESS_EQ_SUB_LESS: "ALL (x::nat) xa::nat. xa <= x --> (ALL c::nat. (x - xa < c) = (x < xa + c))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1176
  by (import arithmetic LESS_EQ_SUB_LESS)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1177
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1178
lemma NOT_SUC_LESS_EQ: "ALL x xa. (~ Suc x <= xa) = (xa <= x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1179
  by (import arithmetic NOT_SUC_LESS_EQ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1180
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1181
lemma SUB_LESS_EQ_ADD: "ALL (m::nat) p::nat. m <= p --> (ALL n::nat. (p - m <= n) = (p <= m + n))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1182
  by (import arithmetic SUB_LESS_EQ_ADD)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1183
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1184
lemma SUB_CANCEL: "ALL (x::nat) (xa::nat) xb::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1185
   xa <= x & xb <= x --> (x - xa = x - xb) = (xa = xb)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1186
  by (import arithmetic SUB_CANCEL)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1187
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1188
lemma NOT_EXP_0: "ALL m n. Suc n ^ m ~= 0"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1189
  by (import arithmetic NOT_EXP_0)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1190
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1191
lemma ZERO_LESS_EXP: "ALL m n. 0 < Suc n ^ m"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1192
  by (import arithmetic ZERO_LESS_EXP)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1193
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1194
lemma ODD_OR_EVEN: "ALL x. EX xa. x = Suc (Suc 0) * xa | x = Suc (Suc 0) * xa + 1"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1195
  by (import arithmetic ODD_OR_EVEN)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1196
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1197
lemma LESS_EXP_SUC_MONO: "ALL n m. Suc (Suc m) ^ n < Suc (Suc m) ^ Suc n"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1198
  by (import arithmetic LESS_EXP_SUC_MONO)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1199
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1200
lemma LESS_LESS_CASES: "ALL (m::nat) n::nat. m = n | m < n | n < m"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1201
  by (import arithmetic LESS_LESS_CASES)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1202
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1203
lemma LESS_EQUAL_ADD: "ALL (m::nat) n::nat. m <= n --> (EX p::nat. n = m + p)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1204
  by (import arithmetic LESS_EQUAL_ADD)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1205
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1206
lemma LESS_EQ_EXISTS: "ALL (m::nat) n::nat. (m <= n) = (EX p::nat. n = m + p)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1207
  by (import arithmetic LESS_EQ_EXISTS)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1208
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1209
lemma MULT_EQ_1: "ALL (x::nat) y::nat. (x * y = (1::nat)) = (x = (1::nat) & y = (1::nat))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1210
  by (import arithmetic MULT_EQ_1)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1211
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1212
consts
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1213
  FACT :: "nat => nat" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1214
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1215
specification (FACT) FACT: "FACT 0 = 1 & (ALL n. FACT (Suc n) = Suc n * FACT n)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1216
  by (import arithmetic FACT)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1217
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1218
lemma FACT_LESS: "ALL n. 0 < FACT n"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1219
  by (import arithmetic FACT_LESS)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1220
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1221
lemma EVEN_ODD: "ALL n. EVEN n = (~ ODD n)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1222
  by (import arithmetic EVEN_ODD)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1223
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1224
lemma ODD_EVEN: "ALL x. ODD x = (~ EVEN x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1225
  by (import arithmetic ODD_EVEN)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1226
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1227
lemma EVEN_OR_ODD: "ALL x. EVEN x | ODD x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1228
  by (import arithmetic EVEN_OR_ODD)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1229
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1230
lemma EVEN_AND_ODD: "ALL x. ~ (EVEN x & ODD x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1231
  by (import arithmetic EVEN_AND_ODD)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1232
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1233
lemma EVEN_ADD: "ALL m n. EVEN (m + n) = (EVEN m = EVEN n)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1234
  by (import arithmetic EVEN_ADD)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1235
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1236
lemma EVEN_MULT: "ALL m n. EVEN (m * n) = (EVEN m | EVEN n)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1237
  by (import arithmetic EVEN_MULT)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1238
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1239
lemma ODD_ADD: "ALL m n. ODD (m + n) = (ODD m ~= ODD n)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1240
  by (import arithmetic ODD_ADD)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1241
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1242
lemma ODD_MULT: "ALL m n. ODD (m * n) = (ODD m & ODD n)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1243
  by (import arithmetic ODD_MULT)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1244
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1245
lemma EVEN_DOUBLE: "ALL n. EVEN (2 * n)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1246
  by (import arithmetic EVEN_DOUBLE)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1247
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1248
lemma ODD_DOUBLE: "ALL x. ODD (Suc (2 * x))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1249
  by (import arithmetic ODD_DOUBLE)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1250
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1251
lemma EVEN_ODD_EXISTS: "ALL x. (EVEN x --> (EX m. x = 2 * m)) & (ODD x --> (EX m. x = Suc (2 * m)))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1252
  by (import arithmetic EVEN_ODD_EXISTS)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1253
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1254
lemma EVEN_EXISTS: "ALL n. EVEN n = (EX m. n = 2 * m)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1255
  by (import arithmetic EVEN_EXISTS)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1256
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1257
lemma ODD_EXISTS: "ALL n. ODD n = (EX m. n = Suc (2 * m))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1258
  by (import arithmetic ODD_EXISTS)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1259
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1260
lemma NOT_SUC_LESS_EQ_0: "ALL x. ~ Suc x <= 0"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1261
  by (import arithmetic NOT_SUC_LESS_EQ_0)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1262
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1263
lemma NOT_LEQ: "ALL x xa. (~ x <= xa) = (Suc xa <= x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1264
  by (import arithmetic NOT_LEQ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1265
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1266
lemma NOT_NUM_EQ: "ALL x xa. (x ~= xa) = (Suc x <= xa | Suc xa <= x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1267
  by (import arithmetic NOT_NUM_EQ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1268
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1269
lemma NOT_GREATER_EQ: "ALL x xa. (~ xa <= x) = (Suc x <= xa)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1270
  by (import arithmetic NOT_GREATER_EQ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1271
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1272
lemma SUC_ADD_SYM: "ALL m n. Suc (m + n) = Suc n + m"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1273
  by (import arithmetic SUC_ADD_SYM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1274
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1275
lemma NOT_SUC_ADD_LESS_EQ: "ALL m n. ~ Suc (m + n) <= m"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1276
  by (import arithmetic NOT_SUC_ADD_LESS_EQ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1277
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1278
lemma SUB_LEFT_ADD: "ALL (m::nat) (n::nat) p::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1279
   m + (n - p) = (if n <= p then m else m + n - p)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1280
  by (import arithmetic SUB_LEFT_ADD)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1281
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1282
lemma SUB_RIGHT_ADD: "ALL (m::nat) (n::nat) p::nat. m - n + p = (if m <= n then p else m + p - n)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1283
  by (import arithmetic SUB_RIGHT_ADD)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1284
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1285
lemma SUB_LEFT_SUB: "ALL (m::nat) (n::nat) p::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1286
   m - (n - p) = (if n <= p then m else m + p - n)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1287
  by (import arithmetic SUB_LEFT_SUB)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1288
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1289
lemma SUB_LEFT_SUC: "ALL m n. Suc (m - n) = (if m <= n then Suc 0 else Suc m - n)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1290
  by (import arithmetic SUB_LEFT_SUC)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1291
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1292
lemma SUB_LEFT_LESS_EQ: "ALL (m::nat) (n::nat) p::nat. (m <= n - p) = (m + p <= n | m <= (0::nat))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1293
  by (import arithmetic SUB_LEFT_LESS_EQ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1294
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1295
lemma SUB_RIGHT_LESS_EQ: "ALL (m::nat) (n::nat) p::nat. (m - n <= p) = (m <= n + p)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1296
  by (import arithmetic SUB_RIGHT_LESS_EQ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1297
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1298
lemma SUB_RIGHT_LESS: "ALL (m::nat) (n::nat) p::nat. (m - n < p) = (m < n + p & (0::nat) < p)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1299
  by (import arithmetic SUB_RIGHT_LESS)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1300
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1301
lemma SUB_RIGHT_GREATER_EQ: "ALL (m::nat) (n::nat) p::nat. (p <= m - n) = (n + p <= m | p <= (0::nat))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1302
  by (import arithmetic SUB_RIGHT_GREATER_EQ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1303
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1304
lemma SUB_LEFT_GREATER: "ALL (m::nat) (n::nat) p::nat. (n - p < m) = (n < m + p & (0::nat) < m)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1305
  by (import arithmetic SUB_LEFT_GREATER)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1306
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1307
lemma SUB_RIGHT_GREATER: "ALL (m::nat) (n::nat) p::nat. (p < m - n) = (n + p < m)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1308
  by (import arithmetic SUB_RIGHT_GREATER)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1309
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1310
lemma SUB_LEFT_EQ: "ALL (m::nat) (n::nat) p::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1311
   (m = n - p) = (m + p = n | m <= (0::nat) & n <= p)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1312
  by (import arithmetic SUB_LEFT_EQ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1313
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1314
lemma SUB_RIGHT_EQ: "ALL (m::nat) (n::nat) p::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1315
   (m - n = p) = (m = n + p | m <= n & p <= (0::nat))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1316
  by (import arithmetic SUB_RIGHT_EQ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1317
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1318
lemma LE: "(ALL n::nat. (n <= (0::nat)) = (n = (0::nat))) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1319
(ALL (m::nat) n::nat. (m <= Suc n) = (m = Suc n | m <= n))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1320
  by (import arithmetic LE)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1321
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1322
lemma DA: "ALL (k::nat) n::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1323
   (0::nat) < n --> (EX (x::nat) q::nat. k = q * n + x & x < n)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1324
  by (import arithmetic DA)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1325
15647
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
  1326
lemma DIV_LESS_EQ: "ALL n>0::nat. ALL k::nat. k div n <= k"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1327
  by (import arithmetic DIV_LESS_EQ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1328
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1329
lemma DIV_UNIQUE: "ALL (n::nat) (k::nat) q::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1330
   (EX r::nat. k = q * n + r & r < n) --> k div n = q"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1331
  by (import arithmetic DIV_UNIQUE)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1332
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1333
lemma MOD_UNIQUE: "ALL (n::nat) (k::nat) r::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1334
   (EX q::nat. k = q * n + r & r < n) --> k mod n = r"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1335
  by (import arithmetic MOD_UNIQUE)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1336
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1337
lemma DIV_MULT: "ALL (n::nat) r::nat. r < n --> (ALL q::nat. (q * n + r) div n = q)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1338
  by (import arithmetic DIV_MULT)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1339
15647
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
  1340
lemma MOD_EQ_0: "ALL n>0::nat. ALL k::nat. k * n mod n = (0::nat)"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1341
  by (import arithmetic MOD_EQ_0)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1342
15647
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
  1343
lemma ZERO_MOD: "ALL n>0::nat. (0::nat) mod n = (0::nat)"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1344
  by (import arithmetic ZERO_MOD)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1345
15647
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
  1346
lemma ZERO_DIV: "ALL n>0::nat. (0::nat) div n = (0::nat)"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1347
  by (import arithmetic ZERO_DIV)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1348
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1349
lemma MOD_MULT: "ALL (n::nat) r::nat. r < n --> (ALL q::nat. (q * n + r) mod n = r)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1350
  by (import arithmetic MOD_MULT)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1351
15647
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
  1352
lemma MOD_TIMES: "ALL n>0::nat. ALL (q::nat) r::nat. (q * n + r) mod n = r mod n"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1353
  by (import arithmetic MOD_TIMES)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1354
15647
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
  1355
lemma MOD_PLUS: "ALL n>0::nat. ALL (j::nat) k::nat. (j mod n + k mod n) mod n = (j + k) mod n"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1356
  by (import arithmetic MOD_PLUS)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1357
15647
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
  1358
lemma MOD_MOD: "ALL n>0::nat. ALL k::nat. k mod n mod n = k mod n"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1359
  by (import arithmetic MOD_MOD)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1360
15647
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
  1361
lemma ADD_DIV_ADD_DIV: "ALL x>0::nat. ALL (xa::nat) r::nat. (xa * x + r) div x = xa + r div x"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1362
  by (import arithmetic ADD_DIV_ADD_DIV)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1363
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1364
lemma MOD_MULT_MOD: "ALL (m::nat) n::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1365
   (0::nat) < n & (0::nat) < m -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1366
   (ALL x::nat. x mod (n * m) mod n = x mod n)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1367
  by (import arithmetic MOD_MULT_MOD)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1368
15647
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
  1369
lemma DIVMOD_ID: "ALL n>0::nat. n div n = (1::nat) & n mod n = (0::nat)"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1370
  by (import arithmetic DIVMOD_ID)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1371
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1372
lemma DIV_DIV_DIV_MULT: "ALL (x::nat) xa::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1373
   (0::nat) < x & (0::nat) < xa -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1374
   (ALL xb::nat. xb div x div xa = xb div (x * xa))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1375
  by (import arithmetic DIV_DIV_DIV_MULT)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1376
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1377
lemma DIV_P: "ALL (P::nat => bool) (p::nat) q::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1378
   (0::nat) < q -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1379
   P (p div q) = (EX (k::nat) r::nat. p = k * q + r & r < q & P k)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1380
  by (import arithmetic DIV_P)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1381
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1382
lemma MOD_P: "ALL (P::nat => bool) (p::nat) q::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1383
   (0::nat) < q -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1384
   P (p mod q) = (EX (k::nat) r::nat. p = k * q + r & r < q & P r)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1385
  by (import arithmetic MOD_P)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1386
15647
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
  1387
lemma MOD_TIMES2: "ALL n>0::nat. ALL (j::nat) k::nat. j mod n * (k mod n) mod n = j * k mod n"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1388
  by (import arithmetic MOD_TIMES2)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1389
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1390
lemma MOD_COMMON_FACTOR: "ALL (n::nat) (p::nat) q::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1391
   (0::nat) < n & (0::nat) < q --> n * (p mod q) = n * p mod (n * q)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1392
  by (import arithmetic MOD_COMMON_FACTOR)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1393
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1394
lemma num_case_cong: "ALL M M' b f.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1395
   M = M' & (M' = 0 --> b = b') & (ALL n. M' = Suc n --> f n = f' n) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1396
   nat_case b f M = nat_case b' f' M'"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1397
  by (import arithmetic num_case_cong)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1398
15647
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
  1399
lemma SUC_ELIM_THM: "ALL P. (ALL n. P (Suc n) n) = (ALL n>0. P n (n - 1))"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1400
  by (import arithmetic SUC_ELIM_THM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1401
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1402
lemma SUB_ELIM_THM: "(P::nat => bool) ((a::nat) - (b::nat)) =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1403
(ALL x::nat. (b = a + x --> P (0::nat)) & (a = b + x --> P x))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1404
  by (import arithmetic SUB_ELIM_THM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1405
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1406
lemma PRE_ELIM_THM: "P (PRE n) = (ALL m. (n = 0 --> P 0) & (n = Suc m --> P m))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1407
  by (import arithmetic PRE_ELIM_THM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1408
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1409
lemma MULT_INCREASES: "ALL m n. 1 < m & 0 < n --> Suc n <= m * n"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1410
  by (import arithmetic MULT_INCREASES)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1411
15647
b1f486a9c56b Updated import configuration.
skalberg
parents: 14847
diff changeset
  1412
lemma EXP_ALWAYS_BIG_ENOUGH: "ALL b>1::nat. ALL n::nat. EX m::nat. n <= b ^ m"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1413
  by (import arithmetic EXP_ALWAYS_BIG_ENOUGH)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1414
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1415
lemma EXP_EQ_0: "ALL (n::nat) m::nat. (n ^ m = (0::nat)) = (n = (0::nat) & (0::nat) < m)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1416
  by (import arithmetic EXP_EQ_0)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1417
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1418
lemma EXP_1: "ALL x::nat. (1::nat) ^ x = (1::nat) & x ^ (1::nat) = x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1419
  by (import arithmetic EXP_1)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1420
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1421
lemma EXP_EQ_1: "ALL (n::nat) m::nat. (n ^ m = (1::nat)) = (n = (1::nat) | m = (0::nat))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1422
  by (import arithmetic EXP_EQ_1)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1423
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1424
lemma MIN_MAX_EQ: "ALL (x::nat) xa::nat. (min x xa = max x xa) = (x = xa)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1425
  by (import arithmetic MIN_MAX_EQ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1426
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1427
lemma MIN_MAX_LT: "ALL (x::nat) xa::nat. (min x xa < max x xa) = (x ~= xa)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1428
  by (import arithmetic MIN_MAX_LT)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1429
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1430
lemma MIN_MAX_PRED: "ALL (P::nat => bool) (m::nat) n::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1431
   P m & P n --> P (min m n) & P (max m n)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1432
  by (import arithmetic MIN_MAX_PRED)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1433
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1434
lemma MIN_LT: "ALL (x::nat) xa::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1435
   (min xa x < xa) = (xa ~= x & min xa x = x) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1436
   (min xa x < x) = (xa ~= x & min xa x = xa) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1437
   (xa < min xa x) = False & (x < min xa x) = False"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1438
  by (import arithmetic MIN_LT)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1439
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1440
lemma MAX_LT: "ALL (x::nat) xa::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1441
   (xa < max xa x) = (xa ~= x & max xa x = x) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1442
   (x < max xa x) = (xa ~= x & max xa x = xa) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1443
   (max xa x < xa) = False & (max xa x < x) = False"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1444
  by (import arithmetic MAX_LT)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1445
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1446
lemma MIN_LE: "ALL (x::nat) xa::nat. min xa x <= xa & min xa x <= x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1447
  by (import arithmetic MIN_LE)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1448
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1449
lemma MAX_LE: "ALL (x::nat) xa::nat. xa <= max xa x & x <= max xa x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1450
  by (import arithmetic MAX_LE)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1451
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1452
lemma MIN_0: "ALL x::nat. min x (0::nat) = (0::nat) & min (0::nat) x = (0::nat)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1453
  by (import arithmetic MIN_0)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1454
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1455
lemma MAX_0: "ALL x::nat. max x (0::nat) = x & max (0::nat) x = x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1456
  by (import arithmetic MAX_0)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1457
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1458
lemma EXISTS_GREATEST: "ALL P::nat => bool.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1459
   (Ex P & (EX x::nat. ALL y::nat. x < y --> ~ P y)) =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1460
   (EX x::nat. P x & (ALL y::nat. x < y --> ~ P y))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1461
  by (import arithmetic EXISTS_GREATEST)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1462
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1463
;end_setup
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1464
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1465
;setup_theory hrat
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1466
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1467
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1468
  trat_1 :: "nat * nat" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1469
  "trat_1 == (0, 0)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1470
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1471
lemma trat_1: "trat_1 = (0, 0)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1472
  by (import hrat trat_1)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1473
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1474
constdefs