remove more clutter related to old "fast_descrs" optimization
authorblanchet
Tue Sep 14 16:33:38 2010 +0200 (2010-09-14)
changeset 393659cab71c20613
parent 39364 61f0d36840c5
child 39366 f58fbb959826
remove more clutter related to old "fast_descrs" optimization
src/HOL/Nitpick.thy
     1.1 --- a/src/HOL/Nitpick.thy	Tue Sep 14 15:39:57 2010 +0200
     1.2 +++ b/src/HOL/Nitpick.thy	Tue Sep 14 16:33:38 2010 +0200
     1.3 @@ -30,13 +30,10 @@
     1.4  
     1.5  axiomatization unknown :: 'a
     1.6             and is_unknown :: "'a \<Rightarrow> bool"
     1.7 -           and undefined_fast_The :: 'a
     1.8 -           and undefined_fast_Eps :: 'a
     1.9             and bisim :: "bisim_iterator \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
    1.10             and bisim_iterator_max :: bisim_iterator
    1.11             and Quot :: "'a \<Rightarrow> 'b"
    1.12             and safe_The :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
    1.13 -           and safe_Eps :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
    1.14  
    1.15  datatype ('a, 'b) fin_fun = FinFun "('a \<Rightarrow> 'b)"
    1.16  datatype ('a, 'b) fun_box = FunBox "('a \<Rightarrow> 'b)"
    1.17 @@ -95,10 +92,10 @@
    1.18                  else THE y. wfrec_rel R (%f x. F (Recdef.cut f R x) x) x y"
    1.19  
    1.20  definition card' :: "('a \<Rightarrow> bool) \<Rightarrow> nat" where
    1.21 -"card' A \<equiv> if finite A then length (safe_Eps (\<lambda>xs. set xs = A \<and> distinct xs)) else 0"
    1.22 +"card' A \<equiv> if finite A then length (SOME xs. set xs = A \<and> distinct xs) else 0"
    1.23  
    1.24  definition setsum' :: "('a \<Rightarrow> 'b\<Colon>comm_monoid_add) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'b" where
    1.25 -"setsum' f A \<equiv> if finite A then listsum (map f (safe_Eps (\<lambda>xs. set xs = A \<and> distinct xs))) else 0"
    1.26 +"setsum' f A \<equiv> if finite A then listsum (map f (SOME xs. set xs = A \<and> distinct xs)) else 0"
    1.27  
    1.28  inductive fold_graph' :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> bool" where
    1.29  "fold_graph' f z {} z" |
    1.30 @@ -239,12 +236,11 @@
    1.31  
    1.32  setup {* Nitpick_Isar.setup *}
    1.33  
    1.34 -hide_const (open) unknown is_unknown undefined_fast_The undefined_fast_Eps bisim 
    1.35 -    bisim_iterator_max Quot safe_The safe_Eps FinFun FunBox PairBox Word refl'
    1.36 -    wf' wf_wfrec wf_wfrec' wfrec' card' setsum' fold_graph' nat_gcd nat_lcm
    1.37 -    int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac one_frac num denom
    1.38 -    norm_frac frac plus_frac times_frac uminus_frac number_of_frac inverse_frac
    1.39 -    less_frac less_eq_frac of_frac
    1.40 +hide_const (open) unknown is_unknown bisim bisim_iterator_max Quot safe_The
    1.41 +    FinFun FunBox PairBox Word refl' wf' wf_wfrec wf_wfrec' wfrec' card' setsum'
    1.42 +    fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac
    1.43 +    one_frac num denom norm_frac frac plus_frac times_frac uminus_frac
    1.44 +    number_of_frac inverse_frac less_frac less_eq_frac of_frac
    1.45  hide_type (open) bisim_iterator fin_fun fun_box pair_box unsigned_bit signed_bit
    1.46      word
    1.47  hide_fact (open) If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def