--- a/src/HOL/Int.thy Thu Mar 01 22:26:29 2012 +0100
+++ b/src/HOL/Int.thy Fri Mar 02 19:05:13 2012 +0100
@@ -2179,6 +2179,36 @@
qed
+subsection {* Finiteness of intervals *}
+
+lemma finite_interval_int1 [iff]: "finite {i :: int. a <= i & i <= b}"
+proof (cases "a <= b")
+ case True
+ from this show ?thesis
+ proof (induct b rule: int_ge_induct)
+ case base
+ have "{i. a <= i & i <= a} = {a}" by auto
+ from this show ?case by simp
+ next
+ case (step b)
+ from this have "{i. a <= i & i <= b + 1} = {i. a <= i & i <= b} \<union> {b + 1}" by auto
+ from this step show ?case by simp
+ qed
+next
+ case False from this show ?thesis
+ by (metis (lifting, no_types) Collect_empty_eq finite.emptyI order_trans)
+qed
+
+lemma finite_interval_int2 [iff]: "finite {i :: int. a <= i & i < b}"
+by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto
+
+lemma finite_interval_int3 [iff]: "finite {i :: int. a < i & i <= b}"
+by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto
+
+lemma finite_interval_int4 [iff]: "finite {i :: int. a < i & i < b}"
+by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto
+
+
subsection {* Configuration of the code generator *}
code_datatype Pls Min Bit0 Bit1 "number_of \<Colon> int \<Rightarrow> int"
--- a/src/HOL/Library/Binomial.thy Thu Mar 01 22:26:29 2012 +0100
+++ b/src/HOL/Library/Binomial.thy Fri Mar 02 19:05:13 2012 +0100
@@ -203,16 +203,14 @@
lemma setprod_nat_ivl_Suc: "setprod f {0 .. Suc n} = setprod f {0..n} * f (Suc n)"
proof-
- have th: "finite {0..n}" "finite {Suc n}" "{0..n} \<inter> {Suc n} = {}" by auto
have eq: "{0..Suc n} = {0..n} \<union> {Suc n}" by auto
- show ?thesis unfolding eq setprod_Un_disjoint[OF th] by simp
+ show ?thesis unfolding eq by (simp add: field_simps)
qed
lemma setprod_nat_ivl_1_Suc: "setprod f {0 .. Suc n} = f 0 * setprod f {1.. Suc n}"
proof-
- have th: "finite {0}" "finite {1..Suc n}" "{0} \<inter> {1.. Suc n} = {}" by auto
have eq: "{0..Suc n} = {0} \<union> {1 .. Suc n}" by auto
- show ?thesis unfolding eq setprod_Un_disjoint[OF th] by simp
+ show ?thesis unfolding eq by simp
qed
@@ -221,7 +219,7 @@
{assume "n=0" then have ?thesis by simp}
moreover
{fix m assume m: "n = Suc m"
- have ?thesis unfolding m pochhammer_Suc_setprod setprod_nat_ivl_Suc ..}
+ have ?thesis unfolding m pochhammer_Suc_setprod setprod_nat_ivl_Suc ..}
ultimately show ?thesis by (cases n, auto)
qed
--- a/src/HOL/Library/Formal_Power_Series.thy Thu Mar 01 22:26:29 2012 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy Fri Mar 02 19:05:13 2012 +0100
@@ -420,10 +420,9 @@
lemma X_mult_nth[simp]: "(X * (f :: ('a::semiring_1) fps)) $n = (if n = 0 then 0 else f $ (n - 1))"
proof-
{assume n: "n \<noteq> 0"
- have fN: "finite {0 .. n}" by simp
have "(X * f) $n = (\<Sum>i = 0..n. X $ i * f $ (n - i))" by (simp add: fps_mult_nth)
also have "\<dots> = f $ (n - 1)"
- using n by (simp add: X_def mult_delta_left setsum_delta [OF fN])
+ using n by (simp add: X_def mult_delta_left setsum_delta)
finally have ?thesis using n by simp }
moreover
{assume n: "n=0" hence ?thesis by (simp add: fps_mult_nth X_def)}
@@ -686,7 +685,6 @@
{fix n::nat assume np: "n >0 "
from np have eq: "{0..n} = {0} \<union> {1 .. n}" by auto
have d: "{0} \<inter> {1 .. n} = {}" by auto
- have f: "finite {0::nat}" "finite {1..n}" by auto
from f0 np have th0: "- (inverse f$n) =
(setsum (\<lambda>i. f$i * natfun_inverse f (n - i)) {1..n}) / (f$0)"
by (cases n, simp, simp add: divide_inverse fps_inverse_def)
@@ -698,8 +696,7 @@
unfolding fps_mult_nth ifn ..
also have "\<dots> = f$0 * natfun_inverse f n
+ (\<Sum>i = 1..n. f$i * natfun_inverse f (n-i))"
- unfolding setsum_Un_disjoint[OF f d, unfolded eq[symmetric]]
- by simp
+ by (simp add: eq)
also have "\<dots> = 0" unfolding th1 ifn by simp
finally have "(inverse f * f)$n = 0" unfolding c . }
with th0 show ?thesis by (simp add: fps_eq_iff)
@@ -1449,8 +1446,7 @@
fixes m :: nat and a :: "('a::comm_ring_1) fps"
shows "(a ^ Suc m)$n = setsum (\<lambda>v. setprod (\<lambda>j. a $ (v!j)) {0..m}) (natpermute n (m+1))"
proof-
- have f: "finite {0 ..m}" by simp
- have th0: "a^Suc m = setprod (\<lambda>i. a) {0..m}" unfolding setprod_constant[OF f, of a] by simp
+ have th0: "a^Suc m = setprod (\<lambda>i. a) {0..m}" by (simp add: setprod_constant)
show ?thesis unfolding th0 fps_setprod_nth ..
qed
lemma fps_power_nth:
@@ -1565,7 +1561,6 @@
{assume "k=0" hence ?thesis by simp }
moreover
{fix h assume h: "k = Suc h"
- have fh: "finite {0..h}" by simp
have eq1: "fps_radical r k a ^ k $ 0 = (\<Prod>j\<in>{0..h}. fps_radical r k a $ (replicate k 0) ! j)"
unfolding fps_power_nth h by simp
also have "\<dots> = (\<Prod>j\<in>{0..h}. r k (a$0))"
@@ -1575,7 +1570,7 @@
apply (subgoal_tac "replicate k (0::nat) ! x = 0")
by (auto intro: nth_replicate simp del: replicate.simps)
also have "\<dots> = a$0"
- unfolding setprod_constant[OF fh] using r by (simp add: h)
+ using r by (simp add: h setprod_constant)
finally have ?thesis using h by simp}
ultimately show ?thesis by (cases k, auto)
qed
@@ -1618,7 +1613,6 @@
using fps_radical_power_nth[of r "Suc k" a, OF r0] by simp}
moreover
{fix n1 assume n1: "n = Suc n1"
- have fK: "finite {0..k}" by simp
have nz: "n \<noteq> 0" using n1 by arith
let ?Pnk = "natpermute n (k + 1)"
let ?Pnkn = "{xs \<in> ?Pnk. n \<in> set xs}"
@@ -1639,7 +1633,7 @@
apply (rule setprod_cong, simp)
using i r0 by (simp del: replicate.simps)
also have "\<dots> = (fps_radical r (Suc k) a $ n) * r (Suc k) (a$0) ^ k"
- unfolding setprod_gen_delta[OF fK] using i r0 by simp
+ using i r0 by (simp add: setprod_gen_delta)
finally show ?ths .
qed
then have "setsum ?f ?Pnkn = of_nat (k+1) * ?r $ n * r (Suc k) (a $ 0) ^ k"
@@ -1737,7 +1731,6 @@
moreover
{assume H: "a^Suc k = b"
have ceq: "card {0..k} = Suc k" by simp
- have fk: "finite {0..k}" by simp
from a0 have a0r0: "a$0 = ?r$0" by simp
{fix n have "a $ n = ?r $ n"
proof(induct n rule: nat_less_induct)
@@ -1767,7 +1760,7 @@
apply (rule setprod_cong, simp)
using i a0 by (simp del: replicate.simps)
also have "\<dots> = a $ n * (?r $ 0)^k"
- unfolding setprod_gen_delta[OF fK] using i by simp
+ using i by (simp add: setprod_gen_delta)
finally show ?ths .
qed
then have th0: "setsum ?g ?Pnkn = of_nat (k+1) * a $ n * (?r $ 0)^k"
--- a/src/HOL/Library/Multiset.thy Thu Mar 01 22:26:29 2012 +0100
+++ b/src/HOL/Library/Multiset.thy Fri Mar 02 19:05:13 2012 +0100
@@ -476,6 +476,8 @@
lemma finite_set_of [iff]: "finite (set_of M)"
using count [of M] by (simp add: multiset_def set_of_def)
+lemma finite_Collect_mem [iff]: "finite {x. x :# M}"
+ unfolding set_of_def[symmetric] by simp
subsubsection {* Size *}
--- a/src/HOL/Old_Number_Theory/Gauss.thy Thu Mar 01 22:26:29 2012 +0100
+++ b/src/HOL/Old_Number_Theory/Gauss.thy Fri Mar 02 19:05:13 2012 +0100
@@ -67,10 +67,7 @@
subsection {* Basic Properties of the Gauss Sets *}
lemma finite_A: "finite (A)"
- apply (auto simp add: A_def)
- apply (subgoal_tac "{x. 0 < x & x \<le> (p - 1) div 2} \<subseteq> {x. 0 \<le> x & x < 1 + (p - 1) div 2}")
- apply (auto simp add: bdd_int_set_l_finite finite_subset)
- done
+by (auto simp add: A_def)
lemma finite_B: "finite (B)"
by (auto simp add: B_def finite_A)
--- a/src/HOL/Quickcheck_Narrowing.thy Thu Mar 01 22:26:29 2012 +0100
+++ b/src/HOL/Quickcheck_Narrowing.thy Fri Mar 02 19:05:13 2012 +0100
@@ -202,13 +202,13 @@
subsubsection {* Narrowing's deep representation of types and terms *}
-datatype narrowing_type = SumOfProd "narrowing_type list list"
-datatype narrowing_term = Var "code_int list" narrowing_type | Ctr code_int "narrowing_term list"
-datatype 'a cons = C narrowing_type "(narrowing_term list => 'a) list"
+datatype narrowing_type = Narrowing_sum_of_products "narrowing_type list list"
+datatype narrowing_term = Narrowing_variable "code_int list" narrowing_type | Narrowing_constructor code_int "narrowing_term list"
+datatype 'a narrowing_cons = Narrowing_cons narrowing_type "(narrowing_term list => 'a) list"
-primrec map_cons :: "('a => 'b) => 'a cons => 'b cons"
+primrec map_cons :: "('a => 'b) => 'a narrowing_cons => 'b narrowing_cons"
where
- "map_cons f (C ty cs) = C ty (map (%c. f o c) cs)"
+ "map_cons f (Narrowing_cons ty cs) = Narrowing_cons ty (map (%c. f o c) cs)"
subsubsection {* From narrowing's deep representation of terms to @{theory Code_Evaluation}'s terms *}
@@ -238,46 +238,46 @@
subsubsection {* Narrowing's basic operations *}
-type_synonym 'a narrowing = "code_int => 'a cons"
+type_synonym 'a narrowing = "code_int => 'a narrowing_cons"
definition empty :: "'a narrowing"
where
- "empty d = C (SumOfProd []) []"
+ "empty d = Narrowing_cons (Narrowing_sum_of_products []) []"
definition cons :: "'a => 'a narrowing"
where
- "cons a d = (C (SumOfProd [[]]) [(%_. a)])"
+ "cons a d = (Narrowing_cons (Narrowing_sum_of_products [[]]) [(%_. a)])"
fun conv :: "(narrowing_term list => 'a) list => narrowing_term => 'a"
where
- "conv cs (Var p _) = error (marker # map toEnum p)"
-| "conv cs (Ctr i xs) = (nth cs i) xs"
+ "conv cs (Narrowing_variable p _) = error (marker # map toEnum p)"
+| "conv cs (Narrowing_constructor i xs) = (nth cs i) xs"
-fun nonEmpty :: "narrowing_type => bool"
+fun non_empty :: "narrowing_type => bool"
where
- "nonEmpty (SumOfProd ps) = (\<not> (List.null ps))"
+ "non_empty (Narrowing_sum_of_products ps) = (\<not> (List.null ps))"
definition "apply" :: "('a => 'b) narrowing => 'a narrowing => 'b narrowing"
where
"apply f a d =
- (case f d of C (SumOfProd ps) cfs =>
- case a (d - 1) of C ta cas =>
+ (case f d of Narrowing_cons (Narrowing_sum_of_products ps) cfs =>
+ case a (d - 1) of Narrowing_cons ta cas =>
let
- shallow = (d > 0 \<and> nonEmpty ta);
+ shallow = (d > 0 \<and> non_empty ta);
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)"
+ in Narrowing_cons (Narrowing_sum_of_products [ta # p. shallow, p <- ps]) cs)"
definition sum :: "'a narrowing => 'a narrowing => 'a narrowing"
where
"sum a b d =
- (case a d of C (SumOfProd ssa) ca =>
- case b d of C (SumOfProd ssb) cb =>
- C (SumOfProd (ssa @ ssb)) (ca @ cb))"
+ (case a d of Narrowing_cons (Narrowing_sum_of_products ssa) ca =>
+ case b d of Narrowing_cons (Narrowing_sum_of_products ssb) cb =>
+ Narrowing_cons (Narrowing_sum_of_products (ssa @ ssb)) (ca @ cb))"
lemma [fundef_cong]:
assumes "a d = a' d" "b d = b' d" "d = d'"
shows "sum a b d = sum a' b' d'"
-using assms unfolding sum_def by (auto split: cons.split narrowing_type.split)
+using assms unfolding sum_def by (auto split: narrowing_cons.split narrowing_type.split)
lemma [fundef_cong]:
assumes "f d = f' d" "(\<And>d'. 0 <= d' & d' < d ==> a d' = a' d')"
@@ -291,24 +291,24 @@
have "int_of (of_int (int_of d' - int_of (of_int 1))) < int_of d'"
by (simp add: of_int_inverse)
ultimately show ?thesis
- unfolding apply_def by (auto split: cons.split narrowing_type.split simp add: Let_def)
+ unfolding apply_def by (auto split: narrowing_cons.split narrowing_type.split simp add: Let_def)
qed
subsubsection {* Narrowing generator type class *}
class narrowing =
- fixes narrowing :: "code_int => 'a cons"
+ fixes narrowing :: "code_int => 'a narrowing_cons"
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 *)
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))))"
+ "exists f = (case narrowing (100 :: code_int) of Narrowing_cons ty cs => Existential ty (\<lambda> t. f (conv cs t)) (partial_term_of (TYPE('a))))"
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))))"
+ "all f = (case narrowing (100 :: code_int) of Narrowing_cons ty cs => Universal ty (\<lambda>t. f (conv cs t)) (partial_term_of (TYPE('a))))"
subsubsection {* class @{text is_testable} *}
@@ -356,14 +356,14 @@
where
"narrowing_dummy_partial_term_of = partial_term_of"
-definition narrowing_dummy_narrowing :: "code_int => ('a :: narrowing) cons"
+definition narrowing_dummy_narrowing :: "code_int => ('a :: narrowing) narrowing_cons"
where
"narrowing_dummy_narrowing = narrowing"
lemma [code]:
"ensure_testable f =
(let
- x = narrowing_dummy_narrowing :: code_int => bool cons;
+ x = narrowing_dummy_narrowing :: code_int => bool narrowing_cons;
y = narrowing_dummy_partial_term_of :: bool itself => narrowing_term => term;
z = (conv :: _ => _ => unit) in f)"
unfolding Let_def ensure_testable_def ..
@@ -382,8 +382,8 @@
subsection {* Narrowing for integers *}
-definition drawn_from :: "'a list => 'a cons"
-where "drawn_from xs = C (SumOfProd (map (%_. []) xs)) (map (%x y. x) xs)"
+definition drawn_from :: "'a list => 'a narrowing_cons"
+where "drawn_from xs = Narrowing_cons (Narrowing_sum_of_products (map (%_. []) xs)) (map (%x y. x) xs)"
function around_zero :: "int => int list"
where
@@ -419,8 +419,8 @@
by (rule partial_term_of_anything)+
lemma [code]:
- "partial_term_of (ty :: int itself) (Var p t) == Code_Evaluation.Free (STR ''_'') (Typerep.Typerep (STR ''Int.int'') [])"
- "partial_term_of (ty :: int itself) (Ctr i []) == (if i mod 2 = 0 then
+ "partial_term_of (ty :: int itself) (Narrowing_variable p t) == Code_Evaluation.Free (STR ''_'') (Typerep.Typerep (STR ''Int.int'') [])"
+ "partial_term_of (ty :: int itself) (Narrowing_constructor i []) == (if i mod 2 = 0 then
Code_Evaluation.term_of (- (int_of i) div 2) else Code_Evaluation.term_of ((int_of i + 1) div 2))"
by (rule partial_term_of_anything)+
@@ -459,9 +459,9 @@
subsection {* Closing up *}
-hide_type code_int narrowing_type narrowing_term cons property
-hide_const int_of of_int nat_of map_cons nth error toEnum marker empty C conv nonEmpty ensure_testable all exists drawn_from around_zero
-hide_const (open) Var Ctr "apply" sum cons
-hide_fact empty_def cons_def conv.simps nonEmpty.simps apply_def sum_def ensure_testable_def all_def exists_def
+hide_type code_int narrowing_type narrowing_term narrowing_cons property
+hide_const int_of of_int nat_of map_cons nth error toEnum marker empty Narrowing_cons conv non_empty ensure_testable all exists drawn_from around_zero
+hide_const (open) Narrowing_variable Narrowing_constructor "apply" sum cons
+hide_fact empty_def cons_def conv.simps non_empty.simps apply_def sum_def ensure_testable_def all_def exists_def
end
--- a/src/HOL/Rat.thy Thu Mar 01 22:26:29 2012 +0100
+++ b/src/HOL/Rat.thy Fri Mar 02 19:05:13 2012 +0100
@@ -1184,8 +1184,8 @@
end
lemma [code]:
- "partial_term_of (ty :: rat itself) (Quickcheck_Narrowing.Var p tt) == Code_Evaluation.Free (STR ''_'') (Typerep.Typerep (STR ''Rat.rat'') [])"
- "partial_term_of (ty :: rat itself) (Quickcheck_Narrowing.Ctr 0 [l, k]) ==
+ "partial_term_of (ty :: rat itself) (Quickcheck_Narrowing.Narrowing_variable p tt) == Code_Evaluation.Free (STR ''_'') (Typerep.Typerep (STR ''Rat.rat'') [])"
+ "partial_term_of (ty :: rat itself) (Quickcheck_Narrowing.Narrowing_constructor 0 [l, k]) ==
Code_Evaluation.App (Code_Evaluation.Const (STR ''Rat.Frct'')
(Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''Product_Type.prod'') [Typerep.Typerep (STR ''Int.int'') [], Typerep.Typerep (STR ''Int.int'') []],
Typerep.Typerep (STR ''Rat.rat'') []])) (Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.Const (STR ''Product_Type.Pair'') (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''Int.int'') [], Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''Int.int'') [], Typerep.Typerep (STR ''Product_Type.prod'') [Typerep.Typerep (STR ''Int.int'') [], Typerep.Typerep (STR ''Int.int'') []]]])) (partial_term_of (TYPE(int)) l)) (partial_term_of (TYPE(int)) k))"
--- a/src/HOL/SupInf.thy Thu Mar 01 22:26:29 2012 +0100
+++ b/src/HOL/SupInf.thy Fri Mar 02 19:05:13 2012 +0100
@@ -445,11 +445,9 @@
fixes x :: real
shows "max x y = Sup {x,y}"
proof-
- have f: "finite {x, y}" "{x,y} \<noteq> {}" by simp_all
- from Sup_finite_le_iff[OF f, of "max x y"] have "Sup {x,y} \<le> max x y" by simp
+ have "Sup {x,y} \<le> max x y" by (simp add: Sup_finite_le_iff)
moreover
- have "max x y \<le> Sup {x,y}" using Sup_finite_ge_iff[OF f, of "max x y"]
- by (simp add: linorder_linear)
+ have "max x y \<le> Sup {x,y}" by (simp add: linorder_linear Sup_finite_ge_iff)
ultimately show ?thesis by arith
qed
@@ -457,12 +455,9 @@
fixes x :: real
shows "min x y = Inf {x,y}"
proof-
- have f: "finite {x, y}" "{x,y} \<noteq> {}" by simp_all
- from Inf_finite_le_iff[OF f, of "min x y"] have "Inf {x,y} \<le> min x y"
- by (simp add: linorder_linear)
+ have "Inf {x,y} \<le> min x y" by (simp add: linorder_linear Inf_finite_le_iff)
moreover
- have "min x y \<le> Inf {x,y}" using Inf_finite_ge_iff[OF f, of "min x y"]
- by simp
+ have "min x y \<le> Inf {x,y}" by (simp add: Inf_finite_ge_iff)
ultimately show ?thesis by arith
qed
--- a/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs Thu Mar 01 22:26:29 2012 +0100
+++ b/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs Fri Mar 02 19:05:13 2012 +0100
@@ -11,12 +11,12 @@
-- Term refinement
new :: Pos -> [[Generated_Code.Narrowing_type]] -> [Generated_Code.Narrowing_term];
-new p ps = [ Generated_Code.Ctr c (zipWith (\i t -> Generated_Code.Var (p++[i]) t) [0..] ts)
+new p ps = [ Generated_Code.Narrowing_constructor c (zipWith (\i t -> Generated_Code.Narrowing_variable (p++[i]) t) [0..] ts)
| (c, ts) <- zip [0..] ps ];
refine :: Generated_Code.Narrowing_term -> Pos -> [Generated_Code.Narrowing_term];
-refine (Generated_Code.Var p (Generated_Code.SumOfProd ss)) [] = new p ss;
-refine (Generated_Code.Ctr c xs) p = map (Generated_Code.Ctr c) (refineList xs p);
+refine (Generated_Code.Narrowing_variable p (Generated_Code.Narrowing_sum_of_products ss)) [] = new p ss;
+refine (Generated_Code.Narrowing_constructor c xs) p = map (Generated_Code.Narrowing_constructor c) (refineList xs p);
refineList :: [Generated_Code.Narrowing_term] -> Pos -> [[Generated_Code.Narrowing_term]];
refineList xs (i:is) = let (ls, x:rs) = splitAt i xs in [ls ++ y:rs | y <- refine x is];
@@ -24,8 +24,8 @@
-- Find total instantiations of a partial value
total :: Generated_Code.Narrowing_term -> [Generated_Code.Narrowing_term];
-total (Generated_Code.Ctr c xs) = [Generated_Code.Ctr c ys | ys <- mapM total xs];
-total (Generated_Code.Var p (Generated_Code.SumOfProd ss)) = [y | x <- new p ss, y <- total x];
+total (Generated_Code.Narrowing_constructor c xs) = [Generated_Code.Narrowing_constructor c ys | ys <- mapM total xs];
+total (Generated_Code.Narrowing_variable p (Generated_Code.Narrowing_sum_of_products ss)) = [y | x <- new p ss, y <- total x];
-- Answers
@@ -99,10 +99,10 @@
instance (Generated_Code.Partial_term_of a, Generated_Code.Narrowing a, Testable b) => Testable (a -> b) where {
property f = P $ \n d ->
- let Generated_Code.C t c = Generated_Code.narrowing d
+ let Generated_Code.Narrowing_cons t c = Generated_Code.narrowing d
c' = Generated_Code.conv c
r = run (\(x:xs) -> f xs (c' x)) (n+1) d
- in r { args = Generated_Code.Var [n] t : args r,
+ in r { args = Generated_Code.Narrowing_variable [n] t : args r,
showArgs = (show . Generated_Code.partial_term_of (Generated_Code.Type :: Generated_Code.Itself a)) : showArgs r };
};
--- a/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs Thu Mar 01 22:26:29 2012 +0100
+++ b/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs Fri Mar 02 19:05:13 2012 +0100
@@ -27,8 +27,8 @@
tailPosEdge (CtrB pos ts) = CtrB (tail pos) ts
termOf :: Pos -> Path -> Generated_Code.Narrowing_term
-termOf pos (CtrB [] i : es) = Generated_Code.Ctr i (termListOf pos es)
-termOf pos [VN [] ty] = Generated_Code.Var pos ty
+termOf pos (CtrB [] i : es) = Generated_Code.Narrowing_constructor i (termListOf pos es)
+termOf pos [VN [] ty] = Generated_Code.Narrowing_variable pos ty
termListOf :: Pos -> Path -> [Generated_Code.Narrowing_term]
termListOf pos es = termListOf' 0 es
@@ -149,7 +149,7 @@
refineTree es p t = updateTree refine (pathPrefix p es) t
where
pathPrefix p es = takeWhile (\e -> posOf e /= p) es
- refine (VarNode q r p (Generated_Code.SumOfProd ps) t) =
+ refine (VarNode q r p (Generated_Code.Narrowing_sum_of_products ps) t) =
CtrBranch q r p [ foldr (\(i,ty) t -> VarNode q r (p++[i]) ty t) t (zip [0..] ts) | ts <- ps ]
-- refute
@@ -230,7 +230,7 @@
termlist_of :: Pos -> ([Generated_Code.Narrowing_term], QuantTree) -> ([Generated_Code.Narrowing_term], QuantTree)
termlist_of p' (terms, Node b) = (terms, Node b)
termlist_of p' (terms, VarNode q r p ty t) = if p' == take (length p') p then
- termlist_of p' (terms ++ [Generated_Code.Var p ty], t)
+ termlist_of p' (terms ++ [Generated_Code.Narrowing_variable p ty], t)
else
(terms, VarNode q r p ty t)
termlist_of p' (terms, CtrBranch q r p ts) = if p' == take (length p') p then
@@ -238,7 +238,7 @@
Just i = findIndex (\t -> evalOf t == Eval False) ts
(subterms, t') = fixp (\j -> termlist_of (p ++ [j])) 0 ([], ts !! i)
in
- (terms ++ [Generated_Code.Ctr i subterms], t')
+ (terms ++ [Generated_Code.Narrowing_constructor i subterms], t')
else
(terms, CtrBranch q r p ts)
where
@@ -248,7 +248,7 @@
alltermlist_of :: Pos -> ([Generated_Code.Narrowing_term], QuantTree) -> [([Generated_Code.Narrowing_term], QuantTree)]
alltermlist_of p' (terms, Node b) = [(terms, Node b)]
alltermlist_of p' (terms, VarNode q r p ty t) = if p' == take (length p') p then
- alltermlist_of p' (terms ++ [Generated_Code.Var p ty], t)
+ alltermlist_of p' (terms ++ [Generated_Code.Narrowing_variable p ty], t)
else
[(terms, VarNode q r p ty t)]
alltermlist_of p' (terms, CtrBranch q r p ts) =
@@ -257,7 +257,7 @@
its = filter (\(i, t) -> evalOf t == Eval False) (zip [0..] ts)
in
concatMap
- (\(i, t) -> map (\(subterms, t') -> (terms ++ [Generated_Code.Ctr i subterms], t'))
+ (\(i, t) -> map (\(subterms, t') -> (terms ++ [Generated_Code.Narrowing_constructor i subterms], t'))
(fixp (\j -> alltermlist_of (p ++ [j])) 0 ([], t))) its
else
[(terms, CtrBranch q r p ts)]
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Thu Mar 01 22:26:29 2012 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Mar 02 19:05:13 2012 +0100
@@ -68,7 +68,7 @@
fun mk_partial_term_of_eq thy ty (i, (c, (_, tys))) =
let
val frees = map Free (Name.invent_names Name.context "a" (map (K @{typ narrowing_term}) tys))
- val narrowing_term = @{term "Quickcheck_Narrowing.Ctr"} $ HOLogic.mk_number @{typ code_int} i
+ val narrowing_term = @{term "Quickcheck_Narrowing.Narrowing_constructor"} $ HOLogic.mk_number @{typ code_int} i
$ (HOLogic.mk_list @{typ narrowing_term} (rev frees))
val rhs = fold (fn u => fn t => @{term "Code_Evaluation.App"} $ t $ u)
(map mk_partial_term_of (frees ~~ tys))
@@ -94,7 +94,7 @@
val const = AxClass.param_of_inst thy (@{const_name partial_term_of}, tyco);
val var_insts =
map (SOME o Thm.cterm_of thy o Logic.unvarify_types_global o Logic.varify_global)
- [Free ("ty", Term.itselfT ty), @{term "Quickcheck_Narrowing.Var p tt"},
+ [Free ("ty", Term.itselfT ty), @{term "Quickcheck_Narrowing.Narrowing_variable p tt"},
@{term "Code_Evaluation.Free (STR ''_'')"} $ HOLogic.mk_typerep ty];
val var_eq =
@{thm partial_term_of_anything}
@@ -122,7 +122,7 @@
val narrowingN = "narrowing";
fun narrowingT T =
- @{typ Quickcheck_Narrowing.code_int} --> Type (@{type_name Quickcheck_Narrowing.cons}, [T])
+ @{typ Quickcheck_Narrowing.code_int} --> Type (@{type_name Quickcheck_Narrowing.narrowing_cons}, [T])
fun mk_empty T = Const (@{const_name Quickcheck_Narrowing.empty}, narrowingT T)
--- a/src/Tools/quickcheck.ML Thu Mar 01 22:26:29 2012 +0100
+++ b/src/Tools/quickcheck.ML Fri Mar 02 19:05:13 2012 +0100
@@ -314,7 +314,27 @@
tester ctxt (length testers > 1) insts goals |>
(fn result => if exists found_counterexample result then SOME result else NONE)) testers)
(fn () => (message ctxt "Quickcheck ran out of time"; NONE)) ();
-
+
+fun all_axioms_of ctxt t =
+ let
+ val intros = Locale.get_intros ctxt
+ val unfolds = Locale.get_unfolds ctxt
+ fun retrieve_prems thms t =
+ case filter (fn th => Term.could_unify (Thm.concl_of th, t)) thms of
+ [] => NONE
+ | [th] =>
+ let
+ val (tyenv, tenv) =
+ Pattern.match (Proof_Context.theory_of ctxt) (Thm.concl_of th, t) (Vartab.empty, Vartab.empty)
+ in SOME (map (Envir.subst_term (tyenv, tenv)) (Thm.prems_of th)) end
+ fun all t =
+ case retrieve_prems intros t of
+ NONE => retrieve_prems unfolds t
+ | SOME ts => SOME (maps (fn t => the_default [t] (all t)) ts)
+ in
+ all t
+ end
+
fun test_goal (time_limit, is_interactive) (insts, eval_terms) i state =
let
val lthy = Proof.context_of state;
@@ -332,21 +352,17 @@
of NONE => Assumption.all_assms_of lthy
| SOME locale => Assumption.local_assms_of lthy (Locale.init locale thy);
val proto_goal = Logic.list_implies (map Thm.term_of assms, subst_bounds (frees, strip gi));
- fun assms_of locale = case fst (Locale.intros_of thy locale) of NONE => []
- | SOME th =>
- let
- val t = the_single (Assumption.all_assms_of (Locale.init locale thy))
- val (tyenv, tenv) =
- Pattern.match thy (concl_of th, term_of t) (Vartab.empty, Vartab.empty)
- in
- map (Envir.subst_term (tyenv, tenv)) (prems_of th)
- end
+ fun axioms_of locale = case fst (Locale.specification_of thy locale) of
+ NONE => []
+ | SOME t => the_default [] (all_axioms_of lthy t)
val goals = case some_locale
of NONE => [(proto_goal, eval_terms)]
| SOME locale =>
- (Logic.list_implies (assms_of locale, proto_goal), eval_terms) ::
+ (Logic.list_implies (axioms_of locale, proto_goal), eval_terms) ::
map (fn (_, phi) => (Morphism.term phi proto_goal, map (Morphism.term phi) eval_terms))
(Locale.registrations_of (Context.Theory thy) (*FIXME*) locale);
+ val _ = verbose_message lthy (Pretty.string_of
+ (Pretty.big_list ("Checking goals: ") (map (Syntax.pretty_term lthy o fst) goals)))
in
test_terms lthy (time_limit, is_interactive) insts goals
end