dropped superfluos prefixes
authorhaftmann
Tue May 26 17:29:33 2009 +0200 (2009-05-26)
changeset 31261900ebbc35e30
parent 31260 4d273d043d59
child 31262 580510315dda
dropped superfluos prefixes
src/HOL/Random.thy
     1.1 --- a/src/HOL/Random.thy	Tue May 26 17:29:32 2009 +0200
     1.2 +++ b/src/HOL/Random.thy	Tue May 26 17:29:33 2009 +0200
     1.3 @@ -119,7 +119,7 @@
     1.4  qed
     1.5  
     1.6  lemma select_weigth_drop_zero:
     1.7 -  "Random.select_weight (filter (\<lambda>(k, _). k > 0) xs) = Random.select_weight xs"
     1.8 +  "select_weight (filter (\<lambda>(k, _). k > 0) xs) = select_weight xs"
     1.9  proof -
    1.10    have "listsum (map fst [(k, _)\<leftarrow>xs . 0 < k]) = listsum (map fst xs)"
    1.11      by (induct xs) auto
    1.12 @@ -128,9 +128,9 @@
    1.13  
    1.14  lemma select_weigth_select:
    1.15    assumes "xs \<noteq> []"
    1.16 -  shows "Random.select_weight (map (Pair 1) xs) = Random.select xs"
    1.17 +  shows "select_weight (map (Pair 1) xs) = select xs"
    1.18  proof -
    1.19 -  have less: "\<And>s. fst (Random.range (Code_Numeral.of_nat (length xs)) s) < Code_Numeral.of_nat (length xs)"
    1.20 +  have less: "\<And>s. fst (range (Code_Numeral.of_nat (length xs)) s) < Code_Numeral.of_nat (length xs)"
    1.21      using assms by (intro range) simp
    1.22    moreover have "listsum (map fst (map (Pair 1) xs)) = Code_Numeral.of_nat (length xs)"
    1.23      by (induct xs) simp_all