src/HOL/Import/HOL/HOL4Prob.thy
changeset 15647 b1f486a9c56b
parent 15071 b65fc0787fbe
child 16417 9bc16273c2d4
     1.1 --- a/src/HOL/Import/HOL/HOL4Prob.thy	Fri Apr 01 18:40:14 2005 +0200
     1.2 +++ b/src/HOL/Import/HOL/HOL4Prob.thy	Fri Apr 01 18:59:17 2005 +0200
     1.3 @@ -1,3 +1,5 @@
     1.4 +(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)
     1.5 +
     1.6  theory HOL4Prob = HOL4Real:
     1.7  
     1.8  ;setup_theory prob_extra
     1.9 @@ -26,10 +28,10 @@
    1.10                      ((op +::nat => nat => nat)
    1.11                        ((op *::nat => nat => nat)
    1.12                          ((number_of::bin => nat)
    1.13 -                          ((op BIT::bin => bool => bin)
    1.14 -                            ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
    1.15 -                              (True::bool))
    1.16 -                            (False::bool)))
    1.17 +                          ((op BIT::bin => bit => bin)
    1.18 +                            ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
    1.19 +                              (bit.B1::bit))
    1.20 +                            (bit.B0::bit)))
    1.21                          q)
    1.22                        r))
    1.23                    ((op |::bool => bool => bool)
    1.24 @@ -39,17 +41,17 @@
    1.25                    ((op =::nat => nat => bool) q
    1.26                      ((op div::nat => nat => nat) n
    1.27                        ((number_of::bin => nat)
    1.28 -                        ((op BIT::bin => bool => bin)
    1.29 -                          ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
    1.30 -                            (True::bool))
    1.31 -                          (False::bool)))))
    1.32 +                        ((op BIT::bin => bit => bin)
    1.33 +                          ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
    1.34 +                            (bit.B1::bit))
    1.35 +                          (bit.B0::bit)))))
    1.36                    ((op =::nat => nat => bool) r
    1.37                      ((op mod::nat => nat => nat) n
    1.38                        ((number_of::bin => nat)
    1.39 -                        ((op BIT::bin => bool => bin)
    1.40 -                          ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
    1.41 -                            (True::bool))
    1.42 -                          (False::bool)))))))))"
    1.43 +                        ((op BIT::bin => bit => bin)
    1.44 +                          ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
    1.45 +                            (bit.B1::bit))
    1.46 +                          (bit.B0::bit)))))))))"
    1.47    by (import prob_extra DIV_TWO_UNIQUE)
    1.48  
    1.49  lemma DIVISION_TWO: "ALL n::nat.
    1.50 @@ -75,16 +77,16 @@
    1.51             ((op <::nat => nat => bool)
    1.52               ((op div::nat => nat => nat) m
    1.53                 ((number_of::bin => nat)
    1.54 -                 ((op BIT::bin => bool => bin)
    1.55 -                   ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
    1.56 -                     (True::bool))
    1.57 -                   (False::bool))))
    1.58 +                 ((op BIT::bin => bit => bin)
    1.59 +                   ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
    1.60 +                     (bit.B1::bit))
    1.61 +                   (bit.B0::bit))))
    1.62               ((op div::nat => nat => nat) n
    1.63                 ((number_of::bin => nat)
    1.64 -                 ((op BIT::bin => bool => bin)
    1.65 -                   ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
    1.66 -                     (True::bool))
    1.67 -                   (False::bool)))))
    1.68 +                 ((op BIT::bin => bit => bin)
    1.69 +                   ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
    1.70 +                     (bit.B1::bit))
    1.71 +                   (bit.B0::bit)))))
    1.72             ((op <::nat => nat => bool) m n)))"
    1.73    by (import prob_extra DIV_TWO_MONO)
    1.74  
    1.75 @@ -97,16 +99,16 @@
    1.76               ((op <::nat => nat => bool)
    1.77                 ((op div::nat => nat => nat) m
    1.78                   ((number_of::bin => nat)
    1.79 -                   ((op BIT::bin => bool => bin)
    1.80 -                     ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
    1.81 -                       (True::bool))
    1.82 -                     (False::bool))))
    1.83 +                   ((op BIT::bin => bit => bin)
    1.84 +                     ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
    1.85 +                       (bit.B1::bit))
    1.86 +                     (bit.B0::bit))))
    1.87                 ((op div::nat => nat => nat) n
    1.88                   ((number_of::bin => nat)
    1.89 -                   ((op BIT::bin => bool => bin)
    1.90 -                     ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
    1.91 -                       (True::bool))
    1.92 -                     (False::bool)))))
    1.93 +                   ((op BIT::bin => bit => bin)
    1.94 +                     ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
    1.95 +                       (bit.B1::bit))
    1.96 +                     (bit.B0::bit)))))
    1.97               ((op <::nat => nat => bool) m n))))"
    1.98    by (import prob_extra DIV_TWO_MONO_EVEN)
    1.99  
   1.100 @@ -203,18 +205,18 @@
   1.101               ((op ^::real => nat => real)
   1.102                 ((op /::real => real => real) (1::real)
   1.103                   ((number_of::bin => real)
   1.104 -                   ((op BIT::bin => bool => bin)
   1.105 -                     ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
   1.106 -                       (True::bool))
   1.107 -                     (False::bool))))
   1.108 +                   ((op BIT::bin => bit => bin)
   1.109 +                     ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
   1.110 +                       (bit.B1::bit))
   1.111 +                     (bit.B0::bit))))
   1.112                 n)
   1.113               ((op ^::real => nat => real)
   1.114                 ((op /::real => real => real) (1::real)
   1.115                   ((number_of::bin => real)
   1.116 -                   ((op BIT::bin => bool => bin)
   1.117 -                     ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
   1.118 -                       (True::bool))
   1.119 -                     (False::bool))))
   1.120 +                   ((op BIT::bin => bit => bin)
   1.121 +                     ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
   1.122 +                       (bit.B1::bit))
   1.123 +                     (bit.B0::bit))))
   1.124                 m))))"
   1.125    by (import prob_extra POW_HALF_MONO)
   1.126  
   1.127 @@ -2527,10 +2529,10 @@
   1.128               ((op *::real => real => real)
   1.129                 ((op /::real => real => real) (1::real)
   1.130                   ((number_of::bin => real)
   1.131 -                   ((op BIT::bin => bool => bin)
   1.132 -                     ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
   1.133 -                       (True::bool))
   1.134 -                     (False::bool))))
   1.135 +                   ((op BIT::bin => bit => bin)
   1.136 +                     ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
   1.137 +                       (bit.B1::bit))
   1.138 +                     (bit.B0::bit))))
   1.139                 ((prob::((nat => bool) => bool) => real) p)))))"
   1.140    by (import prob PROB_INTER_SHD)
   1.141  
   1.142 @@ -3155,10 +3157,10 @@
   1.143                          ((op ^::real => nat => real)
   1.144                            ((op /::real => real => real) (1::real)
   1.145                              ((number_of::bin => real)
   1.146 -                              ((op BIT::bin => bool => bin)
   1.147 -                                ((op BIT::bin => bool => bin)
   1.148 -                                  (Numeral.Pls::bin) (True::bool))
   1.149 -                                (False::bool))))
   1.150 +                              ((op BIT::bin => bit => bin)
   1.151 +                                ((op BIT::bin => bit => bin)
   1.152 +                                  (Numeral.Pls::bin) (bit.B1::bit))
   1.153 +                                (bit.B0::bit))))
   1.154                            ((size::bool list => nat) x))
   1.155                          ((prob::((nat => bool) => bool) => real) q))))))))"
   1.156    by (import prob_indep INDEP_INDEP_SET_LEMMA)
   1.157 @@ -3381,10 +3383,10 @@
   1.158                (op -->::bool => bool => bool)
   1.159                 (P ((op div::nat => nat => nat) ((Suc::nat => nat) v)
   1.160                      ((number_of::bin => nat)
   1.161 -                      ((op BIT::bin => bool => bin)
   1.162 -                        ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
   1.163 -                          (True::bool))
   1.164 -                        (False::bool)))))
   1.165 +                      ((op BIT::bin => bit => bin)
   1.166 +                        ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
   1.167 +                          (bit.B1::bit))
   1.168 +                        (bit.B0::bit)))))
   1.169                 (P ((Suc::nat => nat) v)))))
   1.170        ((All::(nat => bool) => bool) P))"
   1.171    by (import prob_uniform unif_bound_ind)
   1.172 @@ -3435,10 +3437,10 @@
   1.173                     (op -->::bool => bool => bool)
   1.174                      (P ((op div::nat => nat => nat) ((Suc::nat => nat) v2)
   1.175                           ((number_of::bin => nat)
   1.176 -                           ((op BIT::bin => bool => bin)
   1.177 -                             ((op BIT::bin => bool => bin)
   1.178 -                               (Numeral.Pls::bin) (True::bool))
   1.179 -                             (False::bool))))
   1.180 +                           ((op BIT::bin => bit => bin)
   1.181 +                             ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
   1.182 +                               (bit.B1::bit))
   1.183 +                             (bit.B0::bit))))
   1.184                        s)
   1.185                      (P ((Suc::nat => nat) v2) s)))))
   1.186        ((All::(nat => bool) => bool)
   1.187 @@ -3715,15 +3717,15 @@
   1.188        ((op <=::nat => nat => bool)
   1.189          ((op ^::nat => nat => nat)
   1.190            ((number_of::bin => nat)
   1.191 -            ((op BIT::bin => bool => bin)
   1.192 -              ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
   1.193 -              (False::bool)))
   1.194 +            ((op BIT::bin => bit => bin)
   1.195 +              ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
   1.196 +              (bit.B0::bit)))
   1.197            ((unif_bound::nat => nat) n))
   1.198          ((op *::nat => nat => nat)
   1.199            ((number_of::bin => nat)
   1.200 -            ((op BIT::bin => bool => bin)
   1.201 -              ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
   1.202 -              (False::bool)))
   1.203 +            ((op BIT::bin => bit => bin)
   1.204 +              ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
   1.205 +              (bit.B0::bit)))
   1.206            n)))"
   1.207    by (import prob_uniform UNIF_BOUND_UPPER)
   1.208  
   1.209 @@ -3770,10 +3772,10 @@
   1.210             ((op <=::nat => nat => bool) k
   1.211               ((op ^::nat => nat => nat)
   1.212                 ((number_of::bin => nat)
   1.213 -                 ((op BIT::bin => bool => bin)
   1.214 -                   ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
   1.215 -                     (True::bool))
   1.216 -                   (False::bool)))
   1.217 +                 ((op BIT::bin => bit => bin)
   1.218 +                   ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
   1.219 +                     (bit.B1::bit))
   1.220 +                   (bit.B0::bit)))
   1.221                 ((unif_bound::nat => nat) n)))
   1.222             ((op =::real => real => bool)
   1.223               ((prob::((nat => bool) => bool) => real)
   1.224 @@ -3787,10 +3789,10 @@
   1.225                 ((op ^::real => nat => real)
   1.226                   ((op /::real => real => real) (1::real)
   1.227                     ((number_of::bin => real)
   1.228 -                     ((op BIT::bin => bool => bin)
   1.229 -                       ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
   1.230 -                         (True::bool))
   1.231 -                       (False::bool))))
   1.232 +                     ((op BIT::bin => bit => bin)
   1.233 +                       ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
   1.234 +                         (bit.B1::bit))
   1.235 +                       (bit.B0::bit))))
   1.236                   ((unif_bound::nat => nat) n))))))"
   1.237    by (import prob_uniform PROB_UNIF_BOUND)
   1.238  
   1.239 @@ -3906,10 +3908,10 @@
   1.240                         ((op ^::real => nat => real)
   1.241                           ((op /::real => real => real) (1::real)
   1.242                             ((number_of::bin => real)
   1.243 -                             ((op BIT::bin => bool => bin)
   1.244 -                               ((op BIT::bin => bool => bin)
   1.245 -                                 (Numeral.Pls::bin) (True::bool))
   1.246 -                               (False::bool))))
   1.247 +                             ((op BIT::bin => bit => bin)
   1.248 +                               ((op BIT::bin => bit => bin)
   1.249 +                                 (Numeral.Pls::bin) (bit.B1::bit))
   1.250 +                               (bit.B0::bit))))
   1.251                           t))))))"
   1.252    by (import prob_uniform PROB_UNIFORM_PAIR_SUC)
   1.253  
   1.254 @@ -3937,10 +3939,10 @@
   1.255                    ((op ^::real => nat => real)
   1.256                      ((op /::real => real => real) (1::real)
   1.257                        ((number_of::bin => real)
   1.258 -                        ((op BIT::bin => bool => bin)
   1.259 -                          ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
   1.260 -                            (True::bool))
   1.261 -                          (False::bool))))
   1.262 +                        ((op BIT::bin => bit => bin)
   1.263 +                          ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
   1.264 +                            (bit.B1::bit))
   1.265 +                          (bit.B0::bit))))
   1.266                      t)))))"
   1.267    by (import prob_uniform PROB_UNIFORM_SUC)
   1.268  
   1.269 @@ -3968,10 +3970,10 @@
   1.270                    ((op ^::real => nat => real)
   1.271                      ((op /::real => real => real) (1::real)
   1.272                        ((number_of::bin => real)
   1.273 -                        ((op BIT::bin => bool => bin)
   1.274 -                          ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
   1.275 -                            (True::bool))
   1.276 -                          (False::bool))))
   1.277 +                        ((op BIT::bin => bit => bin)
   1.278 +                          ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
   1.279 +                            (bit.B1::bit))
   1.280 +                          (bit.B0::bit))))
   1.281                      t)))))"
   1.282    by (import prob_uniform PROB_UNIFORM)
   1.283