src/HOL/Import/HOLLight/HOLLight.thy
changeset 34974 18b41bba42b5
parent 19233 77ca20b0ed77
child 35416 d8d7d1b785af
     1.1 --- a/src/HOL/Import/HOLLight/HOLLight.thy	Thu Jan 28 11:48:43 2010 +0100
     1.2 +++ b/src/HOL/Import/HOLLight/HOLLight.thy	Thu Jan 28 11:48:49 2010 +0100
     1.3 @@ -1119,37 +1119,37 @@
     1.4     (%x::nat.
     1.5         (All::(nat => bool) => bool)
     1.6          (%xa::nat.
     1.7 -            (op =::nat => nat => bool) ((HOL.plus::nat => nat => nat) x xa)
     1.8 -             ((HOL.plus::nat => nat => nat) x xa))))
     1.9 +            (op =::nat => nat => bool) ((plus::nat => nat => nat) x xa)
    1.10 +             ((plus::nat => nat => nat) x xa))))
    1.11   ((op &::bool => bool => bool)
    1.12 -   ((op =::nat => nat => bool) ((HOL.plus::nat => nat => nat) (0::nat) (0::nat))
    1.13 +   ((op =::nat => nat => bool) ((plus::nat => nat => nat) (0::nat) (0::nat))
    1.14       (0::nat))
    1.15     ((op &::bool => bool => bool)
    1.16       ((All::(nat => bool) => bool)
    1.17         (%x::nat.
    1.18             (op =::nat => nat => bool)
    1.19 -            ((HOL.plus::nat => nat => nat) (0::nat)
    1.20 +            ((plus::nat => nat => nat) (0::nat)
    1.21                ((NUMERAL_BIT0::nat => nat) x))
    1.22              ((NUMERAL_BIT0::nat => nat) x)))
    1.23       ((op &::bool => bool => bool)
    1.24         ((All::(nat => bool) => bool)
    1.25           (%x::nat.
    1.26               (op =::nat => nat => bool)
    1.27 -              ((HOL.plus::nat => nat => nat) (0::nat)
    1.28 +              ((plus::nat => nat => nat) (0::nat)
    1.29                  ((NUMERAL_BIT1::nat => nat) x))
    1.30                ((NUMERAL_BIT1::nat => nat) x)))
    1.31         ((op &::bool => bool => bool)
    1.32           ((All::(nat => bool) => bool)
    1.33             (%x::nat.
    1.34                 (op =::nat => nat => bool)
    1.35 -                ((HOL.plus::nat => nat => nat) ((NUMERAL_BIT0::nat => nat) x)
    1.36 +                ((plus::nat => nat => nat) ((NUMERAL_BIT0::nat => nat) x)
    1.37                    (0::nat))
    1.38                  ((NUMERAL_BIT0::nat => nat) x)))
    1.39           ((op &::bool => bool => bool)
    1.40             ((All::(nat => bool) => bool)
    1.41               (%x::nat.
    1.42                   (op =::nat => nat => bool)
    1.43 -                  ((HOL.plus::nat => nat => nat) ((NUMERAL_BIT1::nat => nat) x)
    1.44 +                  ((plus::nat => nat => nat) ((NUMERAL_BIT1::nat => nat) x)
    1.45                      (0::nat))
    1.46                    ((NUMERAL_BIT1::nat => nat) x)))
    1.47             ((op &::bool => bool => bool)
    1.48 @@ -1158,44 +1158,44 @@
    1.49                     (All::(nat => bool) => bool)
    1.50                      (%xa::nat.
    1.51                          (op =::nat => nat => bool)
    1.52 -                         ((HOL.plus::nat => nat => nat)
    1.53 +                         ((plus::nat => nat => nat)
    1.54                             ((NUMERAL_BIT0::nat => nat) x)
    1.55                             ((NUMERAL_BIT0::nat => nat) xa))
    1.56                           ((NUMERAL_BIT0::nat => nat)
    1.57 -                           ((HOL.plus::nat => nat => nat) x xa)))))
    1.58 +                           ((plus::nat => nat => nat) x xa)))))
    1.59               ((op &::bool => bool => bool)
    1.60                 ((All::(nat => bool) => bool)
    1.61                   (%x::nat.
    1.62                       (All::(nat => bool) => bool)
    1.63                        (%xa::nat.
    1.64                            (op =::nat => nat => bool)
    1.65 -                           ((HOL.plus::nat => nat => nat)
    1.66 +                           ((plus::nat => nat => nat)
    1.67                               ((NUMERAL_BIT0::nat => nat) x)
    1.68                               ((NUMERAL_BIT1::nat => nat) xa))
    1.69                             ((NUMERAL_BIT1::nat => nat)
    1.70 -                             ((HOL.plus::nat => nat => nat) x xa)))))
    1.71 +                             ((plus::nat => nat => nat) x xa)))))
    1.72                 ((op &::bool => bool => bool)
    1.73                   ((All::(nat => bool) => bool)
    1.74                     (%x::nat.
    1.75                         (All::(nat => bool) => bool)
    1.76                          (%xa::nat.
    1.77                              (op =::nat => nat => bool)
    1.78 -                             ((HOL.plus::nat => nat => nat)
    1.79 +                             ((plus::nat => nat => nat)
    1.80                                 ((NUMERAL_BIT1::nat => nat) x)
    1.81                                 ((NUMERAL_BIT0::nat => nat) xa))
    1.82                               ((NUMERAL_BIT1::nat => nat)
    1.83 -                               ((HOL.plus::nat => nat => nat) x xa)))))
    1.84 +                               ((plus::nat => nat => nat) x xa)))))
    1.85                   ((All::(nat => bool) => bool)
    1.86                     (%x::nat.
    1.87                         (All::(nat => bool) => bool)
    1.88                          (%xa::nat.
    1.89                              (op =::nat => nat => bool)
    1.90 -                             ((HOL.plus::nat => nat => nat)
    1.91 +                             ((plus::nat => nat => nat)
    1.92                                 ((NUMERAL_BIT1::nat => nat) x)
    1.93                                 ((NUMERAL_BIT1::nat => nat) xa))
    1.94                               ((NUMERAL_BIT0::nat => nat)
    1.95                                 ((Suc::nat => nat)
    1.96 -                                 ((HOL.plus::nat => nat => nat) x
    1.97 +                                 ((plus::nat => nat => nat) x
    1.98                                     xa))))))))))))))"
    1.99    by (import hollight ARITH_ADD)
   1.100  
   1.101 @@ -1258,7 +1258,7 @@
   1.102                             ((op *::nat => nat => nat)
   1.103                               ((NUMERAL_BIT0::nat => nat) x)
   1.104                               ((NUMERAL_BIT1::nat => nat) xa))
   1.105 -                           ((HOL.plus::nat => nat => nat)
   1.106 +                           ((plus::nat => nat => nat)
   1.107                               ((NUMERAL_BIT0::nat => nat) x)
   1.108                               ((NUMERAL_BIT0::nat => nat)
   1.109                                 ((NUMERAL_BIT0::nat => nat)
   1.110 @@ -1272,7 +1272,7 @@
   1.111                               ((op *::nat => nat => nat)
   1.112                                 ((NUMERAL_BIT1::nat => nat) x)
   1.113                                 ((NUMERAL_BIT0::nat => nat) xa))
   1.114 -                             ((HOL.plus::nat => nat => nat)
   1.115 +                             ((plus::nat => nat => nat)
   1.116                                 ((NUMERAL_BIT0::nat => nat) xa)
   1.117                                 ((NUMERAL_BIT0::nat => nat)
   1.118                                   ((NUMERAL_BIT0::nat => nat)
   1.119 @@ -1285,9 +1285,9 @@
   1.120                               ((op *::nat => nat => nat)
   1.121                                 ((NUMERAL_BIT1::nat => nat) x)
   1.122                                 ((NUMERAL_BIT1::nat => nat) xa))
   1.123 -                             ((HOL.plus::nat => nat => nat)
   1.124 +                             ((plus::nat => nat => nat)
   1.125                                 ((NUMERAL_BIT1::nat => nat) x)
   1.126 -                               ((HOL.plus::nat => nat => nat)
   1.127 +                               ((plus::nat => nat => nat)
   1.128                                   ((NUMERAL_BIT0::nat => nat) xa)
   1.129                                   ((NUMERAL_BIT0::nat => nat)
   1.130                                     ((NUMERAL_BIT0::nat => nat)
   1.131 @@ -7462,7 +7462,7 @@
   1.132        (%i::nat.
   1.133            ($::('A::type, ('M::type, 'N::type) finite_sum) cart
   1.134                => nat => 'A::type)
   1.135 -           u ((HOL.plus::nat => nat => nat) i
   1.136 +           u ((plus::nat => nat => nat) i
   1.137                 ((dimindex::('M::type => bool) => nat)
   1.138                   (hollight.UNIV::'M::type => bool)))))"
   1.139  
   1.140 @@ -7478,14 +7478,14 @@
   1.141        (%i::nat.
   1.142            ($::('A::type, ('M::type, 'N::type) finite_sum) cart
   1.143                => nat => 'A::type)
   1.144 -           u ((HOL.plus::nat => nat => nat) i
   1.145 +           u ((plus::nat => nat => nat) i
   1.146                 ((dimindex::('M::type => bool) => nat)
   1.147                   (hollight.UNIV::'M::type => bool)))))"
   1.148    by (import hollight DEF_sndcart)
   1.149  
   1.150  lemma DIMINDEX_HAS_SIZE_FINITE_SUM: "(HAS_SIZE::(('M::type, 'N::type) finite_sum => bool) => nat => bool)
   1.151   (hollight.UNIV::('M::type, 'N::type) finite_sum => bool)
   1.152 - ((HOL.plus::nat => nat => nat)
   1.153 + ((plus::nat => nat => nat)
   1.154     ((dimindex::('M::type => bool) => nat) (hollight.UNIV::'M::type => bool))
   1.155     ((dimindex::('N::type => bool) => nat)
   1.156       (hollight.UNIV::'N::type => bool)))"
   1.157 @@ -7494,7 +7494,7 @@
   1.158  lemma DIMINDEX_FINITE_SUM: "(op =::nat => nat => bool)
   1.159   ((dimindex::(('M::type, 'N::type) finite_sum => bool) => nat)
   1.160     (hollight.UNIV::('M::type, 'N::type) finite_sum => bool))
   1.161 - ((HOL.plus::nat => nat => nat)
   1.162 + ((plus::nat => nat => nat)
   1.163     ((dimindex::('M::type => bool) => nat) (hollight.UNIV::'M::type => bool))
   1.164     ((dimindex::('N::type => bool) => nat)
   1.165       (hollight.UNIV::'N::type => bool)))"
   1.166 @@ -8025,7 +8025,7 @@
   1.167   (nsum::('q_51017::type => bool) => ('q_51017::type => nat) => nat)
   1.168   ((iterate::(nat => nat => nat)
   1.169              => ('q_51017::type => bool) => ('q_51017::type => nat) => nat)
   1.170 -   (HOL.plus::nat => nat => nat))"
   1.171 +   (plus::nat => nat => nat))"
   1.172  
   1.173  lemma DEF_nsum: "(op =::(('q_51017::type => bool) => ('q_51017::type => nat) => nat)
   1.174         => (('q_51017::type => bool) => ('q_51017::type => nat) => nat)
   1.175 @@ -8033,17 +8033,17 @@
   1.176   (nsum::('q_51017::type => bool) => ('q_51017::type => nat) => nat)
   1.177   ((iterate::(nat => nat => nat)
   1.178              => ('q_51017::type => bool) => ('q_51017::type => nat) => nat)
   1.179 -   (HOL.plus::nat => nat => nat))"
   1.180 +   (plus::nat => nat => nat))"
   1.181    by (import hollight DEF_nsum)
   1.182  
   1.183  lemma NEUTRAL_ADD: "(op =::nat => nat => bool)
   1.184 - ((neutral::(nat => nat => nat) => nat) (HOL.plus::nat => nat => nat)) (0::nat)"
   1.185 + ((neutral::(nat => nat => nat) => nat) (plus::nat => nat => nat)) (0::nat)"
   1.186    by (import hollight NEUTRAL_ADD)
   1.187  
   1.188  lemma NEUTRAL_MUL: "neutral op * = NUMERAL_BIT1 0"
   1.189    by (import hollight NEUTRAL_MUL)
   1.190  
   1.191 -lemma MONOIDAL_ADD: "(monoidal::(nat => nat => nat) => bool) (HOL.plus::nat => nat => nat)"
   1.192 +lemma MONOIDAL_ADD: "(monoidal::(nat => nat => nat) => bool) (plus::nat => nat => nat)"
   1.193    by (import hollight MONOIDAL_ADD)
   1.194  
   1.195  lemma MONOIDAL_MUL: "(monoidal::(nat => nat => nat) => bool) (op *::nat => nat => nat)"
   1.196 @@ -8068,7 +8068,7 @@
   1.197    by (import hollight NSUM_DIFF)
   1.198  
   1.199  lemma NSUM_SUPPORT: "ALL (x::'q_51214::type => nat) xa::'q_51214::type => bool.
   1.200 -   FINITE (support HOL.plus x xa) --> nsum (support HOL.plus x xa) x = nsum xa x"
   1.201 +   FINITE (support plus x xa) --> nsum (support plus x xa) x = nsum xa x"
   1.202    by (import hollight NSUM_SUPPORT)
   1.203  
   1.204  lemma NSUM_ADD: "ALL (f::'q_51260::type => nat) (g::'q_51260::type => nat)