--- a/src/HOL/Import/HOL/HOL4Prob.thy Fri Apr 01 18:40:14 2005 +0200
+++ b/src/HOL/Import/HOL/HOL4Prob.thy Fri Apr 01 18:59:17 2005 +0200
@@ -1,3 +1,5 @@
+(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)
+
theory HOL4Prob = HOL4Real:
;setup_theory prob_extra
@@ -26,10 +28,10 @@
((op +::nat => nat => nat)
((op *::nat => nat => nat)
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool)))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit)))
q)
r))
((op |::bool => bool => bool)
@@ -39,17 +41,17 @@
((op =::nat => nat => bool) q
((op div::nat => nat => nat) n
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool)))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit)))))
((op =::nat => nat => bool) r
((op mod::nat => nat => nat) n
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool)))))))))"
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit)))))))))"
by (import prob_extra DIV_TWO_UNIQUE)
lemma DIVISION_TWO: "ALL n::nat.
@@ -75,16 +77,16 @@
((op <::nat => nat => bool)
((op div::nat => nat => nat) m
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit))))
((op div::nat => nat => nat) n
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool)))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit)))))
((op <::nat => nat => bool) m n)))"
by (import prob_extra DIV_TWO_MONO)
@@ -97,16 +99,16 @@
((op <::nat => nat => bool)
((op div::nat => nat => nat) m
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit))))
((op div::nat => nat => nat) n
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool)))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit)))))
((op <::nat => nat => bool) m n))))"
by (import prob_extra DIV_TWO_MONO_EVEN)
@@ -203,18 +205,18 @@
((op ^::real => nat => real)
((op /::real => real => real) (1::real)
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit))))
n)
((op ^::real => nat => real)
((op /::real => real => real) (1::real)
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit))))
m))))"
by (import prob_extra POW_HALF_MONO)
@@ -2527,10 +2529,10 @@
((op *::real => real => real)
((op /::real => real => real) (1::real)
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit))))
((prob::((nat => bool) => bool) => real) p)))))"
by (import prob PROB_INTER_SHD)
@@ -3155,10 +3157,10 @@
((op ^::real => nat => real)
((op /::real => real => real) (1::real)
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin)
- (Numeral.Pls::bin) (True::bool))
- (False::bool))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin)
+ (Numeral.Pls::bin) (bit.B1::bit))
+ (bit.B0::bit))))
((size::bool list => nat) x))
((prob::((nat => bool) => bool) => real) q))))))))"
by (import prob_indep INDEP_INDEP_SET_LEMMA)
@@ -3381,10 +3383,10 @@
(op -->::bool => bool => bool)
(P ((op div::nat => nat => nat) ((Suc::nat => nat) v)
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool)))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit)))))
(P ((Suc::nat => nat) v)))))
((All::(nat => bool) => bool) P))"
by (import prob_uniform unif_bound_ind)
@@ -3435,10 +3437,10 @@
(op -->::bool => bool => bool)
(P ((op div::nat => nat => nat) ((Suc::nat => nat) v2)
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin)
- (Numeral.Pls::bin) (True::bool))
- (False::bool))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit))))
s)
(P ((Suc::nat => nat) v2) s)))))
((All::(nat => bool) => bool)
@@ -3715,15 +3717,15 @@
((op <=::nat => nat => bool)
((op ^::nat => nat => nat)
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
- (False::bool)))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+ (bit.B0::bit)))
((unif_bound::nat => nat) n))
((op *::nat => nat => nat)
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
- (False::bool)))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+ (bit.B0::bit)))
n)))"
by (import prob_uniform UNIF_BOUND_UPPER)
@@ -3770,10 +3772,10 @@
((op <=::nat => nat => bool) k
((op ^::nat => nat => nat)
((number_of::bin => nat)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool)))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit)))
((unif_bound::nat => nat) n)))
((op =::real => real => bool)
((prob::((nat => bool) => bool) => real)
@@ -3787,10 +3789,10 @@
((op ^::real => nat => real)
((op /::real => real => real) (1::real)
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit))))
((unif_bound::nat => nat) n))))))"
by (import prob_uniform PROB_UNIF_BOUND)
@@ -3906,10 +3908,10 @@
((op ^::real => nat => real)
((op /::real => real => real) (1::real)
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin)
- (Numeral.Pls::bin) (True::bool))
- (False::bool))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin)
+ (Numeral.Pls::bin) (bit.B1::bit))
+ (bit.B0::bit))))
t))))))"
by (import prob_uniform PROB_UNIFORM_PAIR_SUC)
@@ -3937,10 +3939,10 @@
((op ^::real => nat => real)
((op /::real => real => real) (1::real)
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit))))
t)))))"
by (import prob_uniform PROB_UNIFORM_SUC)
@@ -3968,10 +3970,10 @@
((op ^::real => nat => real)
((op /::real => real => real) (1::real)
((number_of::bin => real)
- ((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
- (True::bool))
- (False::bool))))
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit))))
t)))))"
by (import prob_uniform PROB_UNIFORM)