removing unneccessary manual instantiations and dead definitions; hiding more constants and facts
authorbulwahn
Thu Jun 09 08:32:21 2011 +0200 (2011-06-09)
changeset 43315893de45ac28d
parent 43314 a9090cabca14
child 43316 3e274608f06b
removing unneccessary manual instantiations and dead definitions; hiding more constants and facts
src/HOL/Quickcheck_Narrowing.thy
     1.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Thu Jun 09 08:32:19 2011 +0200
     1.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Thu Jun 09 08:32:21 2011 +0200
     1.3 @@ -310,43 +310,11 @@
     1.4      unfolding apply_def by (auto split: cons.split narrowing_type.split simp add: Let_def)
     1.5  qed
     1.6  
     1.7 -type_synonym pos = "code_int list"
     1.8 -(*
     1.9 -subsubsection {* Term refinement *}
    1.10 -
    1.11 -definition new :: "pos => type list list => term list"
    1.12 -where
    1.13 -  "new p ps = map_index (%(c, ts). Ctr c (map_index (%(i, t). Var (p @ [i]) t) ts)) ps"
    1.14 -
    1.15 -fun refine :: "term => pos => term list" and refineList :: "term list => pos => (term list) list"
    1.16 -where
    1.17 -  "refine (Var p (SumOfProd ss)) [] = new p ss"
    1.18 -| "refine (Ctr c xs) p = map (Ctr c) (refineList xs p)"
    1.19 -| "refineList xs (i # is) = (let (ls, xrs) = split_At i xs in (case xrs of x#rs => [ls @ y # rs. y <- refine x is]))"
    1.20 -
    1.21 -text {* Find total instantiations of a partial value *}
    1.22 -
    1.23 -function total :: "term => term list"
    1.24 -where
    1.25 -  "total (Ctr c xs) = [Ctr c ys. ys <- map total xs]"
    1.26 -| "total (Var p (SumOfProd ss)) = [y. x <- new p ss, y <- total x]"
    1.27 -by pat_completeness auto
    1.28 -
    1.29 -termination sorry
    1.30 -*)
    1.31  subsubsection {* Narrowing generator type class *}
    1.32  
    1.33  class narrowing =
    1.34    fixes narrowing :: "code_int => 'a cons"
    1.35  
    1.36 -definition cons1 :: "('a::narrowing => 'b) => 'b narrowing"
    1.37 -where
    1.38 -  "cons1 f = apply (cons f) narrowing"
    1.39 -
    1.40 -definition cons2 :: "('a :: narrowing => 'b :: narrowing => 'c) => 'c narrowing"
    1.41 -where
    1.42 -  "cons2 f = apply (apply (cons f) narrowing) narrowing"
    1.43 -
    1.44  definition drawn_from :: "'a list => 'a cons"
    1.45  where "drawn_from xs = C (SumOfProd (map (%_. []) xs)) (map (%x y. x) xs)"
    1.46  
    1.47 @@ -360,128 +328,14 @@
    1.48  
    1.49  end
    1.50  
    1.51 -instantiation unit :: narrowing
    1.52 -begin
    1.53 -
    1.54 -definition
    1.55 -  "narrowing = cons ()"
    1.56 -
    1.57 -instance ..
    1.58 -
    1.59 -end
    1.60 -
    1.61 -instantiation bool :: narrowing
    1.62 -begin
    1.63 -
    1.64 -definition
    1.65 -  "narrowing = sum (cons True) (cons False)" 
    1.66 -
    1.67 -instance ..
    1.68 -
    1.69 -end
    1.70 -
    1.71 -instantiation option :: (narrowing) narrowing
    1.72 -begin
    1.73 -
    1.74 -definition
    1.75 -  "narrowing = sum (cons None) (cons1 Some)"
    1.76 -
    1.77 -instance ..
    1.78 -
    1.79 -end
    1.80 -
    1.81 -instantiation sum :: (narrowing, narrowing) narrowing
    1.82 -begin
    1.83 -
    1.84 -definition
    1.85 -  "narrowing = sum (cons1 Inl) (cons1 Inr)"
    1.86 -
    1.87 -instance ..
    1.88 -
    1.89 -end
    1.90 -
    1.91 -instantiation list :: (narrowing) narrowing
    1.92 -begin
    1.93 -
    1.94 -function narrowing_list :: "'a list narrowing"
    1.95 -where
    1.96 -  "narrowing_list d = sum (cons []) (apply (apply (cons Cons) narrowing) narrowing_list) d"
    1.97 -by pat_completeness auto
    1.98 -
    1.99 -termination proof (relation "measure nat_of")
   1.100 -qed (auto simp add: of_int_inverse nat_of_def)
   1.101 -    
   1.102 -instance ..
   1.103 -
   1.104 -end
   1.105 -
   1.106 -instantiation nat :: narrowing
   1.107 -begin
   1.108 -
   1.109 -function narrowing_nat :: "nat narrowing"
   1.110 -where
   1.111 -  "narrowing_nat d = sum (cons 0) (apply (cons Suc) narrowing_nat) d"
   1.112 -by pat_completeness auto
   1.113 -
   1.114 -termination proof (relation "measure nat_of")
   1.115 -qed (auto simp add: of_int_inverse nat_of_def)
   1.116 -
   1.117 -instance ..
   1.118 -
   1.119 -end
   1.120 -
   1.121 -instantiation Enum.finite_1 :: narrowing
   1.122 -begin
   1.123 -
   1.124 -definition narrowing_finite_1 :: "Enum.finite_1 narrowing"
   1.125 -where
   1.126 -  "narrowing_finite_1 = cons (Enum.finite_1.a\<^isub>1 :: Enum.finite_1)"
   1.127 -
   1.128 -instance ..
   1.129 -
   1.130 -end
   1.131 -
   1.132 -instantiation Enum.finite_2 :: narrowing
   1.133 -begin
   1.134 -
   1.135 -definition narrowing_finite_2 :: "Enum.finite_2 narrowing"
   1.136 -where
   1.137 -  "narrowing_finite_2 = sum (cons (Enum.finite_2.a\<^isub>1 :: Enum.finite_2)) (cons (Enum.finite_2.a\<^isub>2 :: Enum.finite_2))"
   1.138 -
   1.139 -instance ..
   1.140 -
   1.141 -end
   1.142 -
   1.143 -instantiation Enum.finite_3 :: narrowing
   1.144 -begin
   1.145 -
   1.146 -definition narrowing_finite_3 :: "Enum.finite_3 narrowing"
   1.147 -where
   1.148 -  "narrowing_finite_3 = sum (cons (Enum.finite_3.a\<^isub>1 :: Enum.finite_3)) (sum (cons (Enum.finite_3.a\<^isub>2 :: Enum.finite_3)) (cons (Enum.finite_3.a\<^isub>3 :: Enum.finite_3)))"
   1.149 -
   1.150 -instance ..
   1.151 -
   1.152 -end
   1.153 -
   1.154 -instantiation Enum.finite_4 :: narrowing
   1.155 -begin
   1.156 -
   1.157 -definition narrowing_finite_4 :: "Enum.finite_4 narrowing"
   1.158 -where
   1.159 -  "narrowing_finite_4 = sum (cons Enum.finite_4.a\<^isub>1) (sum (cons Enum.finite_4.a\<^isub>2) (sum (cons Enum.finite_4.a\<^isub>3) (cons Enum.finite_4.a\<^isub>4)))"
   1.160 -
   1.161 -instance ..
   1.162 -
   1.163 -end
   1.164 -
   1.165  datatype property = Universal narrowing_type "(narrowing_term => property)" "narrowing_term => Code_Evaluation.term" | Existential narrowing_type "(narrowing_term => property)" "narrowing_term => Code_Evaluation.term" | Property bool
   1.166  
   1.167  (* FIXME: hard-wired maximal depth of 100 here *)
   1.168 -fun exists :: "('a :: {narrowing, partial_term_of} => property) => property"
   1.169 +definition exists :: "('a :: {narrowing, partial_term_of} => property) => property"
   1.170  where
   1.171    "exists f = (case narrowing (100 :: code_int) of C ty cs => Existential ty (\<lambda> t. f (conv cs t)) (partial_term_of (TYPE('a))))"
   1.172  
   1.173 -fun "all" :: "('a :: {narrowing, partial_term_of} => property) => property"
   1.174 +definition "all" :: "('a :: {narrowing, partial_term_of} => property) => property"
   1.175  where
   1.176    "all f = (case narrowing (100 :: code_int) of C ty cs => Universal ty (\<lambda>t. f (conv cs t)) (partial_term_of (TYPE('a))))"
   1.177  
   1.178 @@ -499,7 +353,6 @@
   1.179  where
   1.180    "ensure_testable f = f"
   1.181  
   1.182 -declare simp_thms(17,19)[code del]
   1.183  
   1.184  subsubsection {* Defining a simple datatype to represent functions in an incomplete and redundant way *}
   1.185  
   1.186 @@ -530,9 +383,9 @@
   1.187  
   1.188  setup {* Narrowing_Generators.setup *}
   1.189  
   1.190 -hide_type (open) code_int narrowing_type narrowing_term cons
   1.191 -hide_const (open) int_of of_int nth error toEnum map_index split_At empty
   1.192 -  C cons conv nonEmpty "apply" sum cons1 cons2 ensure_testable all exists
   1.193 -hide_fact empty_def
   1.194 +hide_type code_int narrowing_type narrowing_term cons property
   1.195 +hide_const int_of of_int nth error toEnum map_index split_At empty
   1.196 +  C cons conv nonEmpty "apply" sum ensure_testable all exists 
   1.197 +hide_fact empty_def cons_def conv.simps nonEmpty.simps apply_def sum_def ensure_testable_def all_def exists_def
   1.198  
   1.199  end
   1.200 \ No newline at end of file