--- a/CONTRIBUTORS Fri Nov 13 14:14:04 2009 +0100
+++ b/CONTRIBUTORS Fri Nov 13 14:14:16 2009 +0100
@@ -6,6 +6,10 @@
Contributions to this Isabelle version
--------------------------------------
+
+* November 2009: Stefan Berghofer, Lukas Bulwahn, TUM
+ A tabled implementation of the reflexive transitive closure
+
* November 2009: Lukas Bulwahn, TUM
Predicate Compiler: a compiler for inductive predicates to equational specfications
--- a/NEWS Fri Nov 13 14:14:04 2009 +0100
+++ b/NEWS Fri Nov 13 14:14:16 2009 +0100
@@ -37,6 +37,8 @@
*** HOL ***
+* A tabled implementation of the reflexive transitive closure
+
* New commands "code_pred" and "values" to invoke the predicate compiler
and to enumerate values of inductive predicates.
--- a/src/HOL/Deriv.thy Fri Nov 13 14:14:04 2009 +0100
+++ b/src/HOL/Deriv.thy Fri Nov 13 14:14:16 2009 +0100
@@ -273,6 +273,11 @@
"DERIV f x :> D ==> DERIV (%x. c * f x) x :> c*D"
by (drule DERIV_mult' [OF DERIV_const], simp)
+lemma DERIV_cdivide: "DERIV f x :> D ==> DERIV (%x. f x / c) x :> D / c"
+ apply (subgoal_tac "DERIV (%x. (1 / c) * f x) x :> (1 / c) * D", force)
+ apply (erule DERIV_cmult)
+ done
+
text {* Standard version *}
lemma DERIV_chain: "[| DERIV f (g x) :> Da; DERIV g x :> Db |] ==> DERIV (f o g) x :> Da * Db"
by (drule (1) DERIV_chain', simp add: o_def real_scaleR_def mult_commute)
@@ -702,14 +707,10 @@
apply safe
apply simp_all
apply (rename_tac x xa ya M Ma)
-apply (cut_tac x = M and y = Ma in linorder_linear, safe)
-apply (rule_tac x = Ma in exI, clarify)
-apply (cut_tac x = xb and y = xa in linorder_linear, force)
-apply (rule_tac x = M in exI, clarify)
-apply (cut_tac x = xb and y = xa in linorder_linear, force)
+apply (metis linorder_not_less order_le_less real_le_trans)
apply (case_tac "a \<le> x & x \<le> b")
-apply (rule_tac [2] x = 1 in exI)
-prefer 2 apply force
+ prefer 2
+ apply (rule_tac x = 1 in exI, force)
apply (simp add: LIM_eq isCont_iff)
apply (drule_tac x = x in spec, auto)
apply (erule_tac V = "\<forall>M. \<exists>x. a \<le> x & x \<le> b & ~ f x \<le> M" in thin_rl)
@@ -815,7 +816,7 @@
text{*If @{term "0 < f'(x)"} then @{term x} is Locally Strictly Increasing At The Right*}
-lemma DERIV_left_inc:
+lemma DERIV_pos_inc_right:
fixes f :: "real => real"
assumes der: "DERIV f x :> l"
and l: "0 < l"
@@ -845,7 +846,7 @@
qed
qed
-lemma DERIV_left_dec:
+lemma DERIV_neg_dec_left:
fixes f :: "real => real"
assumes der: "DERIV f x :> l"
and l: "l < 0"
@@ -875,6 +876,21 @@
qed
qed
+
+lemma DERIV_pos_inc_left:
+ fixes f :: "real => real"
+ shows "DERIV f x :> l \<Longrightarrow> 0 < l \<Longrightarrow> \<exists>d > 0. \<forall>h > 0. h < d --> f(x - h) < f(x)"
+ apply (rule DERIV_neg_dec_left [of "%x. - f x" x "-l", simplified])
+ apply (auto simp add: DERIV_minus)
+ done
+
+lemma DERIV_neg_dec_right:
+ fixes f :: "real => real"
+ shows "DERIV f x :> l \<Longrightarrow> l < 0 \<Longrightarrow> \<exists>d > 0. \<forall>h > 0. h < d --> f(x) > f(x + h)"
+ apply (rule DERIV_pos_inc_right [of "%x. - f x" x "-l", simplified])
+ apply (auto simp add: DERIV_minus)
+ done
+
lemma DERIV_local_max:
fixes f :: "real => real"
assumes der: "DERIV f x :> l"
@@ -885,7 +901,7 @@
case equal thus ?thesis .
next
case less
- from DERIV_left_dec [OF der less]
+ from DERIV_neg_dec_left [OF der less]
obtain d' where d': "0 < d'"
and lt: "\<forall>h > 0. h < d' \<longrightarrow> f x < f (x-h)" by blast
from real_lbound_gt_zero [OF d d']
@@ -894,7 +910,7 @@
show ?thesis by (auto simp add: abs_if)
next
case greater
- from DERIV_left_inc [OF der greater]
+ from DERIV_pos_inc_right [OF der greater]
obtain d' where d': "0 < d'"
and lt: "\<forall>h > 0. h < d' \<longrightarrow> f x < f (x + h)" by blast
from real_lbound_gt_zero [OF d d']
@@ -1205,6 +1221,87 @@
ultimately show ?thesis using neq by (force simp add: add_commute)
qed
+(* A function with positive derivative is increasing.
+ A simple proof using the MVT, by Jeremy Avigad. And variants.
+*)
+
+lemma DERIV_pos_imp_increasing:
+ fixes a::real and b::real and f::"real => real"
+ assumes "a < b" and "\<forall>x. a \<le> x & x \<le> b --> (EX y. DERIV f x :> y & y > 0)"
+ shows "f a < f b"
+proof (rule ccontr)
+ assume "~ f a < f b"
+ from assms have "EX l z. a < z & z < b & DERIV f z :> l
+ & f b - f a = (b - a) * l"
+ by (metis MVT DERIV_isCont differentiableI real_less_def)
+ then obtain l z where "a < z" and "z < b" and "DERIV f z :> l"
+ and "f b - f a = (b - a) * l"
+ by auto
+
+ from prems have "~(l > 0)"
+ by (metis assms(1) linorder_not_le mult_le_0_iff real_le_eq_diff)
+ with prems show False
+ by (metis DERIV_unique real_less_def)
+qed
+
+
+lemma DERIV_nonneg_imp_nonincreasing:
+ fixes a::real and b::real and f::"real => real"
+ assumes "a \<le> b" and
+ "\<forall>x. a \<le> x & x \<le> b --> (\<exists>y. DERIV f x :> y & y \<ge> 0)"
+ shows "f a \<le> f b"
+proof (rule ccontr, cases "a = b")
+ assume "~ f a \<le> f b"
+ assume "a = b"
+ with prems show False by auto
+ next assume "~ f a \<le> f b"
+ assume "a ~= b"
+ with assms have "EX l z. a < z & z < b & DERIV f z :> l
+ & f b - f a = (b - a) * l"
+ apply (intro MVT)
+ apply auto
+ apply (metis DERIV_isCont)
+ apply (metis differentiableI real_less_def)
+ done
+ then obtain l z where "a < z" and "z < b" and "DERIV f z :> l"
+ and "f b - f a = (b - a) * l"
+ by auto
+ from prems have "~(l >= 0)"
+ by (metis diff_self le_eqI le_iff_diff_le_0 real_le_anti_sym real_le_linear
+ split_mult_pos_le)
+ with prems show False
+ by (metis DERIV_unique order_less_imp_le)
+qed
+
+lemma DERIV_neg_imp_decreasing:
+ fixes a::real and b::real and f::"real => real"
+ assumes "a < b" and
+ "\<forall>x. a \<le> x & x \<le> b --> (\<exists>y. DERIV f x :> y & y < 0)"
+ shows "f a > f b"
+proof -
+ have "(%x. -f x) a < (%x. -f x) b"
+ apply (rule DERIV_pos_imp_increasing [of a b "%x. -f x"])
+ apply (insert prems, auto)
+ apply (metis DERIV_minus neg_0_less_iff_less)
+ done
+ thus ?thesis
+ by simp
+qed
+
+lemma DERIV_nonpos_imp_nonincreasing:
+ fixes a::real and b::real and f::"real => real"
+ assumes "a \<le> b" and
+ "\<forall>x. a \<le> x & x \<le> b --> (\<exists>y. DERIV f x :> y & y \<le> 0)"
+ shows "f a \<ge> f b"
+proof -
+ have "(%x. -f x) a \<le> (%x. -f x) b"
+ apply (rule DERIV_nonneg_imp_nonincreasing [of a b "%x. -f x"])
+ apply (insert prems, auto)
+ apply (metis DERIV_minus neg_0_le_iff_le)
+ done
+ thus ?thesis
+ by simp
+qed
subsection {* Continuous injective functions *}
--- a/src/HOL/IsaMakefile Fri Nov 13 14:14:04 2009 +0100
+++ b/src/HOL/IsaMakefile Fri Nov 13 14:14:16 2009 +0100
@@ -382,8 +382,9 @@
Library/Order_Relation.thy Library/Nested_Environment.thy \
Library/Ramsey.thy Library/Zorn.thy Library/Library/ROOT.ML \
Library/Library/document/root.tex Library/Library/document/root.bib \
- Library/While_Combinator.thy Library/Product_ord.thy \
- Library/Char_nat.thy Library/Char_ord.thy Library/Option_ord.thy \
+ Library/Transitive_Closure_Table.thy Library/While_Combinator.thy \
+ Library/Product_ord.thy Library/Char_nat.thy \
+ Library/Char_ord.thy Library/Option_ord.thy \
Library/Sublist_Order.thy Library/List_lexord.thy \
Library/Coinductive_List.thy Library/AssocList.thy \
Library/Formal_Power_Series.thy Library/Binomial.thy \
--- a/src/HOL/Library/Library.thy Fri Nov 13 14:14:04 2009 +0100
+++ b/src/HOL/Library/Library.thy Fri Nov 13 14:14:16 2009 +0100
@@ -51,6 +51,7 @@
SML_Quickcheck
State_Monad
Sum_Of_Squares
+ Transitive_Closure_Table
Univ_Poly
While_Combinator
Word
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Transitive_Closure_Table.thy Fri Nov 13 14:14:16 2009 +0100
@@ -0,0 +1,230 @@
+(* Author: Stefan Berghofer, Lukas Bulwahn, TU Muenchen *)
+
+header {* A tabled implementation of the reflexive transitive closure *}
+
+theory Transitive_Closure_Table
+imports Main
+begin
+
+inductive rtrancl_path :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool"
+ for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+where
+ base: "rtrancl_path r x [] x"
+| step: "r x y \<Longrightarrow> rtrancl_path r y ys z \<Longrightarrow> rtrancl_path r x (y # ys) z"
+
+lemma rtranclp_eq_rtrancl_path: "r\<^sup>*\<^sup>* x y = (\<exists>xs. rtrancl_path r x xs y)"
+proof
+ assume "r\<^sup>*\<^sup>* x y"
+ then show "\<exists>xs. rtrancl_path r x xs y"
+ proof (induct rule: converse_rtranclp_induct)
+ case 1
+ have "rtrancl_path r y [] y" by (rule rtrancl_path.base)
+ then show ?case ..
+ next
+ case (2 x z)
+ from `\<exists>xs. rtrancl_path r z xs y`
+ obtain xs where "rtrancl_path r z xs y" ..
+ with `r x z` have "rtrancl_path r x (z # xs) y"
+ by (rule rtrancl_path.step)
+ then show ?case ..
+ qed
+next
+ assume "\<exists>xs. rtrancl_path r x xs y"
+ then obtain xs where "rtrancl_path r x xs y" ..
+ then show "r\<^sup>*\<^sup>* x y"
+ proof induct
+ case (base x)
+ show ?case by (rule rtranclp.rtrancl_refl)
+ next
+ case (step x y ys z)
+ from `r x y` `r\<^sup>*\<^sup>* y z` show ?case
+ by (rule converse_rtranclp_into_rtranclp)
+ qed
+qed
+
+lemma rtrancl_path_trans:
+ assumes xy: "rtrancl_path r x xs y"
+ and yz: "rtrancl_path r y ys z"
+ shows "rtrancl_path r x (xs @ ys) z" using xy yz
+proof (induct arbitrary: z)
+ case (base x)
+ then show ?case by simp
+next
+ case (step x y xs)
+ then have "rtrancl_path r y (xs @ ys) z"
+ by simp
+ with `r x y` have "rtrancl_path r x (y # (xs @ ys)) z"
+ by (rule rtrancl_path.step)
+ then show ?case by simp
+qed
+
+lemma rtrancl_path_appendE:
+ assumes xz: "rtrancl_path r x (xs @ y # ys) z"
+ obtains "rtrancl_path r x (xs @ [y]) y" and "rtrancl_path r y ys z" using xz
+proof (induct xs arbitrary: x)
+ case Nil
+ then have "rtrancl_path r x (y # ys) z" by simp
+ then obtain xy: "r x y" and yz: "rtrancl_path r y ys z"
+ by cases auto
+ from xy have "rtrancl_path r x [y] y"
+ by (rule rtrancl_path.step [OF _ rtrancl_path.base])
+ then have "rtrancl_path r x ([] @ [y]) y" by simp
+ then show ?thesis using yz by (rule Nil)
+next
+ case (Cons a as)
+ then have "rtrancl_path r x (a # (as @ y # ys)) z" by simp
+ then obtain xa: "r x a" and az: "rtrancl_path r a (as @ y # ys) z"
+ by cases auto
+ show ?thesis
+ proof (rule Cons(1) [OF _ az])
+ assume "rtrancl_path r y ys z"
+ assume "rtrancl_path r a (as @ [y]) y"
+ with xa have "rtrancl_path r x (a # (as @ [y])) y"
+ by (rule rtrancl_path.step)
+ then have "rtrancl_path r x ((a # as) @ [y]) y"
+ by simp
+ then show ?thesis using `rtrancl_path r y ys z`
+ by (rule Cons(2))
+ qed
+qed
+
+lemma rtrancl_path_distinct:
+ assumes xy: "rtrancl_path r x xs y"
+ obtains xs' where "rtrancl_path r x xs' y" and "distinct (x # xs')" using xy
+proof (induct xs rule: measure_induct_rule [of length])
+ case (less xs)
+ show ?case
+ proof (cases "distinct (x # xs)")
+ case True
+ with `rtrancl_path r x xs y` show ?thesis by (rule less)
+ next
+ case False
+ then have "\<exists>as bs cs a. x # xs = as @ [a] @ bs @ [a] @ cs"
+ by (rule not_distinct_decomp)
+ then obtain as bs cs a where xxs: "x # xs = as @ [a] @ bs @ [a] @ cs"
+ by iprover
+ show ?thesis
+ proof (cases as)
+ case Nil
+ with xxs have x: "x = a" and xs: "xs = bs @ a # cs"
+ by auto
+ from x xs `rtrancl_path r x xs y` have cs: "rtrancl_path r x cs y"
+ by (auto elim: rtrancl_path_appendE)
+ from xs have "length cs < length xs" by simp
+ then show ?thesis
+ by (rule less(1)) (iprover intro: cs less(2))+
+ next
+ case (Cons d ds)
+ with xxs have xs: "xs = ds @ a # (bs @ [a] @ cs)"
+ by auto
+ with `rtrancl_path r x xs y` obtain xa: "rtrancl_path r x (ds @ [a]) a"
+ and ay: "rtrancl_path r a (bs @ a # cs) y"
+ by (auto elim: rtrancl_path_appendE)
+ from ay have "rtrancl_path r a cs y" by (auto elim: rtrancl_path_appendE)
+ with xa have xy: "rtrancl_path r x ((ds @ [a]) @ cs) y"
+ by (rule rtrancl_path_trans)
+ from xs have "length ((ds @ [a]) @ cs) < length xs" by simp
+ then show ?thesis
+ by (rule less(1)) (iprover intro: xy less(2))+
+ qed
+ qed
+qed
+
+inductive rtrancl_tab :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+ for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+where
+ base: "rtrancl_tab r xs x x"
+| step: "x \<notin> set xs \<Longrightarrow> r x y \<Longrightarrow> rtrancl_tab r (x # xs) y z \<Longrightarrow> rtrancl_tab r xs x z"
+
+lemma rtrancl_path_imp_rtrancl_tab:
+ assumes path: "rtrancl_path r x xs y"
+ and x: "distinct (x # xs)"
+ and ys: "({x} \<union> set xs) \<inter> set ys = {}"
+ shows "rtrancl_tab r ys x y" using path x ys
+proof (induct arbitrary: ys)
+ case base
+ show ?case by (rule rtrancl_tab.base)
+next
+ case (step x y zs z)
+ then have "x \<notin> set ys" by auto
+ from step have "distinct (y # zs)" by simp
+ moreover from step have "({y} \<union> set zs) \<inter> set (x # ys) = {}"
+ by auto
+ ultimately have "rtrancl_tab r (x # ys) y z"
+ by (rule step)
+ with `x \<notin> set ys` `r x y`
+ show ?case by (rule rtrancl_tab.step)
+qed
+
+lemma rtrancl_tab_imp_rtrancl_path:
+ assumes tab: "rtrancl_tab r ys x y"
+ obtains xs where "rtrancl_path r x xs y" using tab
+proof induct
+ case base
+ from rtrancl_path.base show ?case by (rule base)
+next
+ case step show ?case by (iprover intro: step rtrancl_path.step)
+qed
+
+lemma rtranclp_eq_rtrancl_tab_nil: "r\<^sup>*\<^sup>* x y = rtrancl_tab r [] x y"
+proof
+ assume "r\<^sup>*\<^sup>* x y"
+ then obtain xs where "rtrancl_path r x xs y"
+ by (auto simp add: rtranclp_eq_rtrancl_path)
+ then obtain xs' where xs': "rtrancl_path r x xs' y"
+ and distinct: "distinct (x # xs')"
+ by (rule rtrancl_path_distinct)
+ have "({x} \<union> set xs') \<inter> set [] = {}" by simp
+ with xs' distinct show "rtrancl_tab r [] x y"
+ by (rule rtrancl_path_imp_rtrancl_tab)
+next
+ assume "rtrancl_tab r [] x y"
+ then obtain xs where "rtrancl_path r x xs y"
+ by (rule rtrancl_tab_imp_rtrancl_path)
+ then show "r\<^sup>*\<^sup>* x y"
+ by (auto simp add: rtranclp_eq_rtrancl_path)
+qed
+
+declare rtranclp_eq_rtrancl_tab_nil [code_unfold]
+
+declare rtranclp_eq_rtrancl_tab_nil[THEN iffD2, code_pred_intro]
+
+code_pred rtranclp using rtranclp_eq_rtrancl_tab_nil[THEN iffD1] by fastsimp
+
+subsection {* A simple example *}
+
+datatype ty = A | B | C
+
+inductive test :: "ty \<Rightarrow> ty \<Rightarrow> bool"
+where
+ "test A B"
+| "test B A"
+| "test B C"
+
+subsubsection {* Invoking with the SML code generator *}
+
+code_module Test
+contains
+test1 = "test\<^sup>*\<^sup>* A C"
+test2 = "test\<^sup>*\<^sup>* C A"
+test3 = "test\<^sup>*\<^sup>* A _"
+test4 = "test\<^sup>*\<^sup>* _ C"
+
+ML "Test.test1"
+ML "Test.test2"
+ML "DSeq.list_of Test.test3"
+ML "DSeq.list_of Test.test4"
+
+subsubsection {* Invoking with the predicate compiler and the generic code generator *}
+
+code_pred test .
+
+values "{x. test\<^sup>*\<^sup>* A C}"
+values "{x. test\<^sup>*\<^sup>* C A}"
+values "{x. test\<^sup>*\<^sup>* A x}"
+values "{x. test\<^sup>*\<^sup>* x C}"
+
+hide const test
+
+end
+
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Nov 13 14:14:04 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Nov 13 14:14:16 2009 +0100
@@ -1047,7 +1047,6 @@
let
val _ = tracing ("Clause " ^ string_of_int (i + 1) ^ " of " ^
p ^ " violates mode " ^ string_of_mode thy p m)
- val _ = tracing (string_of_clause thy p (nth rs i))
in () end
else ()
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Nov 13 14:14:04 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Nov 13 14:14:16 2009 +0100
@@ -23,6 +23,8 @@
val options = Options {
expected_modes = NONE,
+ proposed_modes = [],
+ proposed_names = [],
show_steps = true,
show_intermediate_results = true,
show_proof_trace = false,
--- a/src/HOL/Transitive_Closure.thy Fri Nov 13 14:14:04 2009 +0100
+++ b/src/HOL/Transitive_Closure.thy Fri Nov 13 14:14:16 2009 +0100
@@ -575,6 +575,25 @@
"(x,y) \<in> R\<^sup>* = (x=y \<or> x\<noteq>y \<and> (x,y) \<in> R\<^sup>+)"
by (fast elim: trancl_into_rtrancl dest: rtranclD)
+lemma trancl_unfold_right: "r^+ = r^* O r"
+by (auto dest: tranclD2 intro: rtrancl_into_trancl1)
+
+lemma trancl_unfold_left: "r^+ = r O r^*"
+by (auto dest: tranclD intro: rtrancl_into_trancl2)
+
+
+text {* Simplifying nested closures *}
+
+lemma rtrancl_trancl_absorb[simp]: "(R^*)^+ = R^*"
+by (simp add: trans_rtrancl)
+
+lemma trancl_rtrancl_absorb[simp]: "(R^+)^* = R^*"
+by (subst reflcl_trancl[symmetric]) simp
+
+lemma rtrancl_reflcl_absorb[simp]: "(R^*)^= = R^*"
+by auto
+
+
text {* @{text Domain} and @{text Range} *}
lemma Domain_rtrancl [simp]: "Domain (R^*) = UNIV"
--- a/src/HOL/ex/ROOT.ML Fri Nov 13 14:14:04 2009 +0100
+++ b/src/HOL/ex/ROOT.ML Fri Nov 13 14:14:16 2009 +0100
@@ -13,7 +13,8 @@
"Codegenerator_Pretty_Test",
"NormalForm",
"Predicate_Compile",
- "Predicate_Compile_ex"
+ "Predicate_Compile_ex",
+ "Predicate_Compile_Quickcheck"
];
use_thys [