author bulwahn Mon, 14 Mar 2011 12:34:08 +0100 changeset 41961 fdd37cfcd4a3 parent 41960 8a399da4cde1 child 41962 27a61a3266d8
renaming series and serial to narrowing in Quickcheck_Narrowing
```--- a/src/HOL/Library/Quickcheck_Narrowing.thy	Sun Mar 13 23:12:38 2011 +0100
+++ b/src/HOL/Library/Quickcheck_Narrowing.thy	Mon Mar 14 12:34:08 2011 +0100
@@ -86,7 +86,7 @@
code_type code_int
(Haskell "Int")

-subsubsection {* LSC's deep representation of types of terms *}
+subsubsection {* Narrowing's deep representation of types and terms *}

datatype type = SumOfProd "type list list"

@@ -94,7 +94,7 @@

datatype 'a cons = C type "(term list => 'a) list"

-subsubsection {* auxilary functions for LSC *}
+subsubsection {* auxilary functions for Narrowing *}

consts nth :: "'a list => code_int => 'a"

@@ -112,15 +112,15 @@

consts split_At :: "code_int => 'a list => 'a list * 'a list"

-subsubsection {* LSC's basic operations *}
+subsubsection {* Narrowing's basic operations *}

-type_synonym 'a series = "code_int => 'a cons"
+type_synonym 'a narrowing = "code_int => 'a cons"

-definition empty :: "'a series"
+definition empty :: "'a narrowing"
where
"empty d = C (SumOfProd []) []"

-definition cons :: "'a => 'a series"
+definition cons :: "'a => 'a narrowing"
where
"cons a d = (C (SumOfProd [[]]) [(%_. a)])"

@@ -133,7 +133,7 @@
where
"nonEmpty (SumOfProd ps) = (\<not> (List.null ps))"

-definition "apply" :: "('a => 'b) series => 'a series => 'b series"
+definition "apply" :: "('a => 'b) narrowing => 'a narrowing => 'b narrowing"
where
"apply f a d =
(case f d of C (SumOfProd ps) cfs =>
@@ -143,7 +143,7 @@
cs = [(%xs'. (case xs' of [] => undefined | x # xs => cf xs (conv cas x))). shallow, cf <- cfs]
in C (SumOfProd [ta # p. shallow, p <- ps]) cs)"

-definition sum :: "'a series => 'a series => 'a series"
+definition sum :: "'a narrowing => 'a narrowing => 'a narrowing"
where
"sum a b d =
(case a d of C (SumOfProd ssa) ca =>
@@ -170,7 +170,7 @@
unfolding apply_def by (auto split: cons.split type.split simp add: Let_def)
qed

-definition cons0 :: "'a => 'a series"
+definition cons0 :: "'a => 'a narrowing"
where
"cons0 f = cons f"

@@ -198,65 +198,65 @@

termination sorry
*)
-subsubsection {* LSC's type class for enumeration *}
+subsubsection {* Narrowing generator type class *}

-class serial =
-  fixes series :: "code_int => 'a cons"
+class narrowing =
+  fixes narrowing :: "code_int => 'a cons"

-definition cons1 :: "('a::serial => 'b) => 'b series"
+definition cons1 :: "('a::narrowing => 'b) => 'b narrowing"
where
-  "cons1 f = apply (cons f) series"
+  "cons1 f = apply (cons f) narrowing"

-definition cons2 :: "('a :: serial => 'b :: serial => 'c) => 'c series"
+definition cons2 :: "('a :: narrowing => 'b :: narrowing => 'c) => 'c narrowing"
where
-  "cons2 f = apply (apply (cons f) series) series"
+  "cons2 f = apply (apply (cons f) narrowing) narrowing"

-instantiation unit :: serial
+instantiation unit :: narrowing
begin

definition
-  "series = cons0 ()"
+  "narrowing = cons0 ()"

instance ..

end

-instantiation bool :: serial
+instantiation bool :: narrowing
begin

definition
-  "series = sum (cons0 True) (cons0 False)"
+  "narrowing = sum (cons0 True) (cons0 False)"

instance ..

end

-instantiation option :: (serial) serial
+instantiation option :: (narrowing) narrowing
begin

definition
-  "series = sum (cons0 None) (cons1 Some)"
+  "narrowing = sum (cons0 None) (cons1 Some)"

instance ..

end

-instantiation sum :: (serial, serial) serial
+instantiation sum :: (narrowing, narrowing) narrowing
begin

definition
-  "series = sum (cons1 Inl) (cons1 Inr)"
+  "narrowing = sum (cons1 Inl) (cons1 Inr)"

instance ..

end

-instantiation list :: (serial) serial
+instantiation list :: (narrowing) narrowing
begin

-function series_list :: "'a list series"
+function narrowing_list :: "'a list narrowing"
where
-  "series_list d = sum (cons []) (apply (apply (cons Cons) series) series_list) d"
+  "narrowing_list d = sum (cons []) (apply (apply (cons Cons) narrowing) narrowing_list) d"
by pat_completeness auto

termination proof (relation "measure nat_of")
@@ -266,12 +266,12 @@

end

-instantiation nat :: serial
+instantiation nat :: narrowing
begin

-function series_nat :: "nat series"
+function narrowing_nat :: "nat narrowing"
where
-  "series_nat d = sum (cons 0) (apply (cons Suc) series_nat) d"
+  "narrowing_nat d = sum (cons 0) (apply (cons Suc) narrowing_nat) d"
by pat_completeness auto

termination proof (relation "measure nat_of")
@@ -281,45 +281,45 @@

end

-instantiation Enum.finite_1 :: serial
+instantiation Enum.finite_1 :: narrowing
begin

-definition series_finite_1 :: "Enum.finite_1 series"
+definition narrowing_finite_1 :: "Enum.finite_1 narrowing"
where
-  "series_finite_1 = cons (Enum.finite_1.a\<^isub>1 :: Enum.finite_1)"
+  "narrowing_finite_1 = cons (Enum.finite_1.a\<^isub>1 :: Enum.finite_1)"

instance ..

end

-instantiation Enum.finite_2 :: serial
+instantiation Enum.finite_2 :: narrowing
begin

-definition series_finite_2 :: "Enum.finite_2 series"
+definition narrowing_finite_2 :: "Enum.finite_2 narrowing"
where
-  "series_finite_2 = sum (cons (Enum.finite_2.a\<^isub>1 :: Enum.finite_2)) (cons (Enum.finite_2.a\<^isub>2 :: Enum.finite_2))"
+  "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 :: serial
+instantiation Enum.finite_3 :: narrowing
begin

-definition series_finite_3 :: "Enum.finite_3 series"
+definition narrowing_finite_3 :: "Enum.finite_3 narrowing"
where
-  "series_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)))"
+  "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 :: serial
+instantiation Enum.finite_4 :: narrowing
begin

-definition series_finite_4 :: "Enum.finite_4 series"
+definition narrowing_finite_4 :: "Enum.finite_4 narrowing"
where
-  "series_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)))"
+  "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 ..

@@ -333,7 +333,7 @@

instance bool :: is_testable ..

-instance "fun" :: ("{term_of, serial}", is_testable) is_testable ..
+instance "fun" :: ("{term_of, narrowing}", is_testable) is_testable ..

definition ensure_testable :: "'a :: is_testable => 'a :: is_testable"
where```