--- 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 (\<lambda> 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 (\<lambda>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