--- a/src/HOL/Import/HOL/HOL4Prob.thy Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Import/HOL/HOL4Prob.thy Wed Sep 06 13:48:02 2006 +0200
@@ -35,28 +35,28 @@
lemma DIV_TWO_BASIC: "(op &::bool => bool => bool)
((op =::nat => nat => bool)
((op div::nat => nat => nat) (0::nat)
- ((number_of::bin => nat)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+ ((number_of \<Colon> int => nat)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit))))
(0::nat))
((op &::bool => bool => bool)
((op =::nat => nat => bool)
((op div::nat => nat => nat) (1::nat)
- ((number_of::bin => nat)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+ ((number_of \<Colon> int => nat)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit))))
(0::nat))
((op =::nat => nat => bool)
((op div::nat => nat => nat)
- ((number_of::bin => nat)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+ ((number_of \<Colon> int => nat)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit)))
- ((number_of::bin => nat)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+ ((number_of \<Colon> int => nat)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit))))
(1::nat)))"
by (import prob_extra DIV_TWO_BASIC)
@@ -75,19 +75,19 @@
(op =::nat => nat => bool)
((op div::nat => nat => nat)
((op ^::nat => nat => nat)
- ((number_of::bin => nat)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+ ((number_of \<Colon> int => nat)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit)))
((Suc::nat => nat) n))
- ((number_of::bin => nat)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+ ((number_of \<Colon> int => nat)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit))))
((op ^::nat => nat => nat)
- ((number_of::bin => nat)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+ ((number_of \<Colon> int => nat)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit)))
n))"
by (import prob_extra EXP_DIV_TWO)
@@ -125,22 +125,22 @@
lemma HALF_POS: "(op <::real => real => bool) (0::real)
((op /::real => real => real) (1::real)
- ((number_of::bin => real)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+ ((number_of \<Colon> int => real)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit))))"
by (import prob_extra HALF_POS)
lemma HALF_CANCEL: "(op =::real => real => bool)
((op *::real => real => real)
- ((number_of::bin => real)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+ ((number_of \<Colon> int => real)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit)))
((op /::real => real => real) (1::real)
- ((number_of::bin => real)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+ ((number_of \<Colon> int => real)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit)))))
(1::real)"
by (import prob_extra HALF_CANCEL)
@@ -150,9 +150,9 @@
(op <::real => real => bool) (0::real)
((op ^::real => nat => real)
((op /::real => real => real) (1::real)
- ((number_of::bin => real)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+ ((number_of \<Colon> int => real)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit))))
n))"
by (import prob_extra POW_HALF_POS)
@@ -165,17 +165,17 @@
((op <=::real => real => bool)
((op ^::real => nat => real)
((op /::real => real => real) (1::real)
- ((number_of::bin => real)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ ((number_of \<Colon> int => real)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
(bit.B1::bit))
(bit.B0::bit))))
n)
((op ^::real => nat => real)
((op /::real => real => real) (1::real)
- ((number_of::bin => real)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ ((number_of \<Colon> int => real)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
(bit.B1::bit))
(bit.B0::bit))))
m))))"
@@ -186,21 +186,21 @@
(op =::real => real => bool)
((op ^::real => nat => real)
((op /::real => real => real) (1::real)
- ((number_of::bin => real)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+ ((number_of \<Colon> int => real)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit))))
n)
((op *::real => real => real)
- ((number_of::bin => real)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+ ((number_of \<Colon> int => real)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit)))
((op ^::real => nat => real)
((op /::real => real => real) (1::real)
- ((number_of::bin => real)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ ((number_of \<Colon> int => real)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
(bit.B1::bit))
(bit.B0::bit))))
((Suc::nat => nat) n))))"
@@ -227,22 +227,22 @@
lemma ONE_MINUS_HALF: "(op =::real => real => bool)
((op -::real => real => real) (1::real)
((op /::real => real => real) (1::real)
- ((number_of::bin => real)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+ ((number_of \<Colon> int => real)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit)))))
((op /::real => real => real) (1::real)
- ((number_of::bin => real)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+ ((number_of \<Colon> int => real)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit))))"
by (import prob_extra ONE_MINUS_HALF)
lemma HALF_LT_1: "(op <::real => real => bool)
((op /::real => real => real) (1::real)
- ((number_of::bin => real)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+ ((number_of \<Colon> int => real)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit))))
(1::real)"
by (import prob_extra HALF_LT_1)
@@ -252,17 +252,17 @@
(op =::real => real => bool)
((op ^::real => nat => real)
((op /::real => real => real) (1::real)
- ((number_of::bin => real)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+ ((number_of \<Colon> int => real)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit))))
n)
((inverse::real => real)
((real::nat => real)
((op ^::nat => nat => nat)
- ((number_of::bin => nat)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ ((number_of \<Colon> int => nat)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
(bit.B1::bit))
(bit.B0::bit)))
n))))"
@@ -1405,27 +1405,27 @@
((op +::real => real => real)
((op ^::real => nat => real)
((op /::real => real => real) (1::real)
- ((number_of::bin => real)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ ((number_of \<Colon> int => real)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
(bit.B1::bit))
(bit.B0::bit))))
((size::bool list => nat)
((SNOC::bool => bool list => bool list) (True::bool) l)))
((op ^::real => nat => real)
((op /::real => real => real) (1::real)
- ((number_of::bin => real)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ ((number_of \<Colon> int => real)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
(bit.B1::bit))
(bit.B0::bit))))
((size::bool list => nat)
((SNOC::bool => bool list => bool list) (False::bool) l))))
((op ^::real => nat => real)
((op /::real => real => real) (1::real)
- ((number_of::bin => real)
- ((op BIT::bin => bit => bin)
- ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
+ ((number_of \<Colon> int => real)
+ ((op BIT \<Colon> int => bit => int)
+ ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
(bit.B0::bit))))
((size::bool list => nat) l)))"
by (import prob ALG_TWINS_MEASURE)