# HG changeset patch # User bulwahn # Date 1307601141 -7200 # Node ID 893de45ac28d23b8a80fd81c77cd036951e77627 # Parent a9090cabca143883150b93821d9d6c329ce1c758 removing unneccessary manual instantiations and dead definitions; hiding more constants and facts diff -r a9090cabca14 -r 893de45ac28d src/HOL/Quickcheck_Narrowing.thy --- a/src/HOL/Quickcheck_Narrowing.thy Thu Jun 09 08:32:19 2011 +0200 +++ b/src/HOL/Quickcheck_Narrowing.thy Thu Jun 09 08:32:21 2011 +0200 @@ -310,43 +310,11 @@ unfolding apply_def by (auto split: cons.split narrowing_type.split simp add: Let_def) qed -type_synonym pos = "code_int list" -(* -subsubsection {* Term refinement *} - -definition new :: "pos => type list list => term list" -where - "new p ps = map_index (%(c, ts). Ctr c (map_index (%(i, t). Var (p @ [i]) t) ts)) ps" - -fun refine :: "term => pos => term list" and refineList :: "term list => pos => (term list) list" -where - "refine (Var p (SumOfProd ss)) [] = new p ss" -| "refine (Ctr c xs) p = map (Ctr c) (refineList xs p)" -| "refineList xs (i # is) = (let (ls, xrs) = split_At i xs in (case xrs of x#rs => [ls @ y # rs. y <- refine x is]))" - -text {* Find total instantiations of a partial value *} - -function total :: "term => term list" -where - "total (Ctr c xs) = [Ctr c ys. ys <- map total xs]" -| "total (Var p (SumOfProd ss)) = [y. x <- new p ss, y <- total x]" -by pat_completeness auto - -termination sorry -*) subsubsection {* Narrowing generator type class *} class narrowing = fixes narrowing :: "code_int => 'a cons" -definition cons1 :: "('a::narrowing => 'b) => 'b narrowing" -where - "cons1 f = apply (cons f) narrowing" - -definition cons2 :: "('a :: narrowing => 'b :: narrowing => 'c) => 'c narrowing" -where - "cons2 f = apply (apply (cons f) narrowing) narrowing" - definition drawn_from :: "'a list => 'a cons" where "drawn_from xs = C (SumOfProd (map (%_. []) xs)) (map (%x y. x) xs)" @@ -360,128 +328,14 @@ end -instantiation unit :: narrowing -begin - -definition - "narrowing = cons ()" - -instance .. - -end - -instantiation bool :: narrowing -begin - -definition - "narrowing = sum (cons True) (cons False)" - -instance .. - -end - -instantiation option :: (narrowing) narrowing -begin - -definition - "narrowing = sum (cons None) (cons1 Some)" - -instance .. - -end - -instantiation sum :: (narrowing, narrowing) narrowing -begin - -definition - "narrowing = sum (cons1 Inl) (cons1 Inr)" - -instance .. - -end - -instantiation list :: (narrowing) narrowing -begin - -function narrowing_list :: "'a list narrowing" -where - "narrowing_list d = sum (cons []) (apply (apply (cons Cons) narrowing) narrowing_list) d" -by pat_completeness auto - -termination proof (relation "measure nat_of") -qed (auto simp add: of_int_inverse nat_of_def) - -instance .. - -end - -instantiation nat :: narrowing -begin - -function narrowing_nat :: "nat narrowing" -where - "narrowing_nat d = sum (cons 0) (apply (cons Suc) narrowing_nat) d" -by pat_completeness auto - -termination proof (relation "measure nat_of") -qed (auto simp add: of_int_inverse nat_of_def) - -instance .. - -end - -instantiation Enum.finite_1 :: narrowing -begin - -definition narrowing_finite_1 :: "Enum.finite_1 narrowing" -where - "narrowing_finite_1 = cons (Enum.finite_1.a\<^isub>1 :: Enum.finite_1)" - -instance .. - -end - -instantiation Enum.finite_2 :: narrowing -begin - -definition narrowing_finite_2 :: "Enum.finite_2 narrowing" -where - "narrowing_finite_2 = sum (cons (Enum.finite_2.a\<^isub>1 :: Enum.finite_2)) (cons (Enum.finite_2.a\<^isub>2 :: Enum.finite_2))" - -instance .. - -end - -instantiation Enum.finite_3 :: narrowing -begin - -definition narrowing_finite_3 :: "Enum.finite_3 narrowing" -where - "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)))" - -instance .. - -end - -instantiation Enum.finite_4 :: narrowing -begin - -definition narrowing_finite_4 :: "Enum.finite_4 narrowing" -where - "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)))" - -instance .. - -end - 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 (* FIXME: hard-wired maximal depth of 100 here *) -fun exists :: "('a :: {narrowing, partial_term_of} => property) => property" +definition exists :: "('a :: {narrowing, partial_term_of} => property) => property" where "exists f = (case narrowing (100 :: code_int) of C ty cs => Existential ty (\ t. f (conv cs t)) (partial_term_of (TYPE('a))))" -fun "all" :: "('a :: {narrowing, partial_term_of} => property) => property" +definition "all" :: "('a :: {narrowing, partial_term_of} => property) => property" where "all f = (case narrowing (100 :: code_int) of C ty cs => Universal ty (\t. f (conv cs t)) (partial_term_of (TYPE('a))))" @@ -499,7 +353,6 @@ where "ensure_testable f = f" -declare simp_thms(17,19)[code del] subsubsection {* Defining a simple datatype to represent functions in an incomplete and redundant way *} @@ -530,9 +383,9 @@ setup {* Narrowing_Generators.setup *} -hide_type (open) code_int narrowing_type narrowing_term cons -hide_const (open) int_of of_int nth error toEnum map_index split_At empty - C cons conv nonEmpty "apply" sum cons1 cons2 ensure_testable all exists -hide_fact empty_def +hide_type code_int narrowing_type narrowing_term cons property +hide_const int_of of_int nth error toEnum map_index split_At empty + C cons conv nonEmpty "apply" sum ensure_testable all exists +hide_fact empty_def cons_def conv.simps nonEmpty.simps apply_def sum_def ensure_testable_def all_def exists_def end \ No newline at end of file