--- a/src/HOL/Library/Primes.thy Wed May 06 19:09:31 2009 +0200
+++ b/src/HOL/Library/Primes.thy Wed May 06 19:42:27 2009 +0200
@@ -454,19 +454,11 @@
qed
lemma euclid: "\<exists>p. prime p \<and> p > n" using euclid_bound by auto
+
lemma primes_infinite: "\<not> (finite {p. prime p})"
-proof (auto simp add: finite_conv_nat_seg_image)
- fix n f
- assume H: "Collect prime = f ` {i. i < (n::nat)}"
- let ?P = "Collect prime"
- let ?m = "Max ?P"
- have P0: "?P \<noteq> {}" using two_is_prime by auto
- from H have fP: "finite ?P" using finite_conv_nat_seg_image by blast
- from Max_in [OF fP P0] have "?m \<in> ?P" .
- from Max_ge [OF fP] have contr: "\<forall> p. prime p \<longrightarrow> p \<le> ?m" by blast
- from euclid [of ?m] obtain q where q: "prime q" "q > ?m" by blast
- with contr show False by auto
-qed
+apply(simp add: finite_nat_set_iff_bounded_le)
+apply (metis euclid linorder_not_le)
+done
lemma coprime_prime: assumes ab: "coprime a b"
shows "~(prime p \<and> p dvd a \<and> p dvd b)"
--- a/src/HOL/Library/Product_ord.thy Wed May 06 19:09:31 2009 +0200
+++ b/src/HOL/Library/Product_ord.thy Wed May 06 19:42:27 2009 +0200
@@ -12,25 +12,28 @@
begin
definition
- prod_le_def [code del]: "x \<le> y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x \<le> snd y"
+ prod_le_def [code del]: "x \<le> y \<longleftrightarrow> fst x < fst y \<or> fst x \<le> fst y \<and> snd x \<le> snd y"
definition
- prod_less_def [code del]: "x < y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x < snd y"
+ prod_less_def [code del]: "x < y \<longleftrightarrow> fst x < fst y \<or> fst x \<le> fst y \<and> snd x < snd y"
instance ..
end
lemma [code]:
- "(x1\<Colon>'a\<Colon>{ord, eq}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
- "(x1\<Colon>'a\<Colon>{ord, eq}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
+ "(x1\<Colon>'a\<Colon>{ord, eq}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 \<le> y2"
+ "(x1\<Colon>'a\<Colon>{ord, eq}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 < y2"
unfolding prod_le_def prod_less_def by simp_all
-instance * :: (order, order) order
- by default (auto simp: prod_le_def prod_less_def intro: order_less_trans)
+instance * :: (preorder, preorder) preorder proof
+qed (auto simp: prod_le_def prod_less_def less_le_not_le intro: order_trans)
-instance * :: (linorder, linorder) linorder
- by default (auto simp: prod_le_def)
+instance * :: (order, order) order proof
+qed (auto simp add: prod_le_def)
+
+instance * :: (linorder, linorder) linorder proof
+qed (auto simp: prod_le_def)
instantiation * :: (linorder, linorder) distrib_lattice
begin
@@ -41,9 +44,30 @@
definition
sup_prod_def: "(sup \<Colon> 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = max"
-instance
- by intro_classes
- (auto simp add: inf_prod_def sup_prod_def min_max.sup_inf_distrib1)
+instance proof
+qed (auto simp add: inf_prod_def sup_prod_def min_max.sup_inf_distrib1)
+
+end
+
+instantiation * :: (bot, bot) bot
+begin
+
+definition
+ bot_prod_def: "bot = (bot, bot)"
+
+instance proof
+qed (auto simp add: bot_prod_def prod_le_def)
+
+end
+
+instantiation * :: (top, top) top
+begin
+
+definition
+ top_prod_def: "top = (top, top)"
+
+instance proof
+qed (auto simp add: top_prod_def prod_le_def)
end
--- a/src/HOL/SetInterval.thy Wed May 06 19:09:31 2009 +0200
+++ b/src/HOL/SetInterval.thy Wed May 06 19:42:27 2009 +0200
@@ -397,6 +397,22 @@
apply (rule_tac [2] finite_lessThan, auto)
done
+text {* A set of natural numbers is finite iff it is bounded. *}
+lemma finite_nat_set_iff_bounded:
+ "finite(N::nat set) = (EX m. ALL n:N. n<m)" (is "?F = ?B")
+proof
+ assume f:?F show ?B
+ using Max_ge[OF `?F`, simplified less_Suc_eq_le[symmetric]] by blast
+next
+ assume ?B show ?F using `?B` by(blast intro:bounded_nat_set_is_finite)
+qed
+
+lemma finite_nat_set_iff_bounded_le:
+ "finite(N::nat set) = (EX m. ALL n:N. n<=m)"
+apply(simp add:finite_nat_set_iff_bounded)
+apply(blast dest:less_imp_le_nat le_imp_less_Suc)
+done
+
lemma finite_less_ub:
"!!f::nat=>nat. (!!n. n \<le> f n) ==> finite {n. f n \<le> u}"
by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans)
--- a/src/HOLCF/Cfun.thy Wed May 06 19:09:31 2009 +0200
+++ b/src/HOLCF/Cfun.thy Wed May 06 19:42:27 2009 +0200
@@ -345,21 +345,11 @@
assumes f: "cont (\<lambda>p. f (fst p) (snd p))"
shows "cont (\<lambda>x. \<Lambda> y. f x y)"
proof (rule cont2cont_LAM)
- fix x :: 'a
- have "cont (\<lambda>y. (x, y))"
- by (rule cont_pair2)
- with f have "cont (\<lambda>y. f (fst (x, y)) (snd (x, y)))"
- by (rule cont2cont_app3)
- thus "cont (\<lambda>y. f x y)"
- by (simp only: fst_conv snd_conv)
+ fix x :: 'a show "cont (\<lambda>y. f x y)"
+ using f by (rule cont_fst_snd_D2)
next
- fix y :: 'b
- have "cont (\<lambda>x. (x, y))"
- by (rule cont_pair1)
- with f have "cont (\<lambda>x. f (fst (x, y)) (snd (x, y)))"
- by (rule cont2cont_app3)
- thus "cont (\<lambda>x. f x y)"
- by (simp only: fst_conv snd_conv)
+ fix y :: 'b show "cont (\<lambda>x. f x y)"
+ using f by (rule cont_fst_snd_D1)
qed
lemma cont2cont_LAM_discrete [cont2cont]:
--- a/src/HOLCF/Cont.thy Wed May 06 19:09:31 2009 +0200
+++ b/src/HOLCF/Cont.thy Wed May 06 19:42:27 2009 +0200
@@ -180,31 +180,31 @@
text {* application of functions is continuous *}
-lemma cont2cont_apply:
+lemma cont_apply:
fixes f :: "'a::cpo \<Rightarrow> 'b::cpo \<Rightarrow> 'c::cpo" and t :: "'a \<Rightarrow> 'b"
- assumes f1: "\<And>y. cont (\<lambda>x. f x y)"
- assumes f2: "\<And>x. cont (\<lambda>y. f x y)"
- assumes t: "cont (\<lambda>x. t x)"
+ assumes 1: "cont (\<lambda>x. t x)"
+ assumes 2: "\<And>x. cont (\<lambda>y. f x y)"
+ assumes 3: "\<And>y. cont (\<lambda>x. f x y)"
shows "cont (\<lambda>x. (f x) (t x))"
proof (rule monocontlub2cont [OF monofunI contlubI])
fix x y :: "'a" assume "x \<sqsubseteq> y"
then show "f x (t x) \<sqsubseteq> f y (t y)"
- by (auto intro: cont2monofunE [OF f1]
- cont2monofunE [OF f2]
- cont2monofunE [OF t]
+ by (auto intro: cont2monofunE [OF 1]
+ cont2monofunE [OF 2]
+ cont2monofunE [OF 3]
trans_less)
next
fix Y :: "nat \<Rightarrow> 'a" assume "chain Y"
then show "f (\<Squnion>i. Y i) (t (\<Squnion>i. Y i)) = (\<Squnion>i. f (Y i) (t (Y i)))"
- by (simp only: cont2contlubE [OF t] ch2ch_cont [OF t]
- cont2contlubE [OF f1] ch2ch_cont [OF f1]
- cont2contlubE [OF f2] ch2ch_cont [OF f2]
+ by (simp only: cont2contlubE [OF 1] ch2ch_cont [OF 1]
+ cont2contlubE [OF 2] ch2ch_cont [OF 2]
+ cont2contlubE [OF 3] ch2ch_cont [OF 3]
diag_lub)
qed
-lemma cont2cont_compose:
+lemma cont_compose:
"\<lbrakk>cont c; cont (\<lambda>x. f x)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. c (f x))"
-by (rule cont2cont_apply [OF cont_const])
+by (rule cont_apply [OF _ _ cont_const])
text {* if-then-else is continuous *}
--- a/src/HOLCF/Product_Cpo.thy Wed May 06 19:09:31 2009 +0200
+++ b/src/HOLCF/Product_Cpo.thy Wed May 06 19:42:27 2009 +0200
@@ -206,14 +206,54 @@
assumes f: "cont (\<lambda>x. f x)"
assumes g: "cont (\<lambda>x. g x)"
shows "cont (\<lambda>x. (f x, g x))"
-apply (rule cont2cont_apply [OF _ cont_pair1 f])
-apply (rule cont2cont_apply [OF _ cont_pair2 g])
+apply (rule cont_apply [OF f cont_pair1])
+apply (rule cont_apply [OF g cont_pair2])
apply (rule cont_const)
done
-lemmas cont2cont_fst [cont2cont] = cont2cont_compose [OF cont_fst]
+lemmas cont2cont_fst [cont2cont] = cont_compose [OF cont_fst]
+
+lemmas cont2cont_snd [cont2cont] = cont_compose [OF cont_snd]
+
+lemma cont2cont_split:
+ assumes f1: "\<And>a b. cont (\<lambda>x. f x a b)"
+ assumes f2: "\<And>x b. cont (\<lambda>a. f x a b)"
+ assumes f3: "\<And>x a. cont (\<lambda>b. f x a b)"
+ assumes g: "cont (\<lambda>x. g x)"
+ shows "cont (\<lambda>x. split (\<lambda>a b. f x a b) (g x))"
+unfolding split_def
+apply (rule cont_apply [OF g])
+apply (rule cont_apply [OF cont_fst f2])
+apply (rule cont_apply [OF cont_snd f3])
+apply (rule cont_const)
+apply (rule f1)
+done
+
+lemma cont_fst_snd_D1:
+ "cont (\<lambda>p. f (fst p) (snd p)) \<Longrightarrow> cont (\<lambda>x. f x y)"
+by (drule cont_compose [OF _ cont_pair1], simp)
-lemmas cont2cont_snd [cont2cont] = cont2cont_compose [OF cont_snd]
+lemma cont_fst_snd_D2:
+ "cont (\<lambda>p. f (fst p) (snd p)) \<Longrightarrow> cont (\<lambda>y. f x y)"
+by (drule cont_compose [OF _ cont_pair2], simp)
+
+lemma cont2cont_split' [cont2cont]:
+ assumes f: "cont (\<lambda>p. f (fst p) (fst (snd p)) (snd (snd p)))"
+ assumes g: "cont (\<lambda>x. g x)"
+ shows "cont (\<lambda>x. split (f x) (g x))"
+proof -
+ note f1 = f [THEN cont_fst_snd_D1]
+ note f2 = f [THEN cont_fst_snd_D2, THEN cont_fst_snd_D1]
+ note f3 = f [THEN cont_fst_snd_D2, THEN cont_fst_snd_D2]
+ show ?thesis
+ unfolding split_def
+ apply (rule cont_apply [OF g])
+ apply (rule cont_apply [OF cont_fst f2])
+ apply (rule cont_apply [OF cont_snd f3])
+ apply (rule cont_const)
+ apply (rule f1)
+ done
+qed
subsection {* Compactness and chain-finiteness *}
--- a/src/HOLCF/Sum_Cpo.thy Wed May 06 19:09:31 2009 +0200
+++ b/src/HOLCF/Sum_Cpo.thy Wed May 06 19:42:27 2009 +0200
@@ -130,17 +130,14 @@
subsection {* Continuity of @{term Inl}, @{term Inr}, @{term sum_case} *}
-lemma cont2cont_Inl [simp]: "cont f \<Longrightarrow> cont (\<lambda>x. Inl (f x))"
-by (fast intro: contI is_lub_Inl elim: contE)
-
-lemma cont2cont_Inr [simp]: "cont f \<Longrightarrow> cont (\<lambda>x. Inr (f x))"
-by (fast intro: contI is_lub_Inr elim: contE)
-
lemma cont_Inl: "cont Inl"
-by (rule cont2cont_Inl [OF cont_id])
+by (intro contI is_lub_Inl cpo_lubI)
lemma cont_Inr: "cont Inr"
-by (rule cont2cont_Inr [OF cont_id])
+by (intro contI is_lub_Inr cpo_lubI)
+
+lemmas cont2cont_Inl [cont2cont] = cont_compose [OF cont_Inl]
+lemmas cont2cont_Inr [cont2cont] = cont_compose [OF cont_Inr]
lemmas ch2ch_Inl [simp] = ch2ch_cont [OF cont_Inl]
lemmas ch2ch_Inr [simp] = ch2ch_cont [OF cont_Inr]
@@ -161,16 +158,33 @@
apply (simp add: cont2contlubE [OF cont_Inr, symmetric] contE)
done
-lemma cont2cont_sum_case [simp]:
+lemma cont2cont_sum_case:
assumes f1: "\<And>a. cont (\<lambda>x. f x a)" and f2: "\<And>x. cont (\<lambda>a. f x a)"
assumes g1: "\<And>b. cont (\<lambda>x. g x b)" and g2: "\<And>x. cont (\<lambda>b. g x b)"
assumes h: "cont (\<lambda>x. h x)"
shows "cont (\<lambda>x. case h x of Inl a \<Rightarrow> f x a | Inr b \<Rightarrow> g x b)"
-apply (rule cont2cont_app2 [OF cont2cont_lambda _ h])
+apply (rule cont_apply [OF h])
+apply (rule cont_sum_case2 [OF f2 g2])
apply (rule cont_sum_case1 [OF f1 g1])
-apply (rule cont_sum_case2 [OF f2 g2])
done
+lemma cont2cont_sum_case' [cont2cont]:
+ assumes f: "cont (\<lambda>p. f (fst p) (snd p))"
+ assumes g: "cont (\<lambda>p. g (fst p) (snd p))"
+ assumes h: "cont (\<lambda>x. h x)"
+ shows "cont (\<lambda>x. case h x of Inl a \<Rightarrow> f x a | Inr b \<Rightarrow> g x b)"
+proof -
+ note f1 = f [THEN cont_fst_snd_D1]
+ note f2 = f [THEN cont_fst_snd_D2]
+ note g1 = g [THEN cont_fst_snd_D1]
+ note g2 = g [THEN cont_fst_snd_D2]
+ show ?thesis
+ apply (rule cont_apply [OF h])
+ apply (rule cont_sum_case2 [OF f2 g2])
+ apply (rule cont_sum_case1 [OF f1 g1])
+ done
+qed
+
subsection {* Compactness and chain-finiteness *}
lemma compact_Inl: "compact a \<Longrightarrow> compact (Inl a)"
--- a/src/Pure/Tools/find_theorems.ML Wed May 06 19:09:31 2009 +0200
+++ b/src/Pure/Tools/find_theorems.ML Wed May 06 19:42:27 2009 +0200
@@ -7,7 +7,7 @@
signature FIND_THEOREMS =
sig
datatype 'term criterion =
- Name of string | Intro | Elim | Dest | Solves | Simp of 'term |
+ Name of string | Intro | IntroIff | Elim | Dest | Solves | Simp of 'term |
Pattern of 'term
val tac_limit: int ref
val limit: int ref
@@ -24,11 +24,12 @@
(** search criteria **)
datatype 'term criterion =
- Name of string | Intro | Elim | Dest | Solves | Simp of 'term |
+ Name of string | Intro | IntroIff | Elim | Dest | Solves | Simp of 'term |
Pattern of 'term;
fun read_criterion _ (Name name) = Name name
| read_criterion _ Intro = Intro
+ | read_criterion _ IntroIff = IntroIff
| read_criterion _ Elim = Elim
| read_criterion _ Dest = Dest
| read_criterion _ Solves = Solves
@@ -42,6 +43,7 @@
(case c of
Name name => Pretty.str (prfx "name: " ^ quote name)
| Intro => Pretty.str (prfx "intro")
+ | IntroIff => Pretty.str (prfx "introiff")
| Elim => Pretty.str (prfx "elim")
| Dest => Pretty.str (prfx "dest")
| Solves => Pretty.str (prfx "solves")
@@ -74,17 +76,40 @@
fun is_nontrivial thy = Term.is_Const o Term.head_of o ObjectLogic.drop_judgment thy;
+(* Note: ("op =" : "bool --> bool --> bool") does not exist in Pure. *)
+fun is_Iff c =
+ (case dest_Const c of
+ ("op =", ty) =>
+ (ty
+ |> strip_type
+ |> swap
+ |> (op ::)
+ |> map (fst o dest_Type)
+ |> forall (curry (op =) "bool")
+ handle TYPE _ => false)
+ | _ => false);
+
(*extract terms from term_src, refine them to the parts that concern us,
if po try match them against obj else vice versa.
trivial matches are ignored.
returns: smallest substitution size*)
-fun is_matching_thm (extract_terms, refine_term) ctxt po obj term_src =
+fun is_matching_thm doiff (extract_terms, refine_term) ctxt po obj term_src =
let
val thy = ProofContext.theory_of ctxt;
+ val chkmatch = obj |> (if po then rpair else pair) #> Pattern.matches thy;
fun matches pat =
- is_nontrivial thy pat andalso
- Pattern.matches thy (if po then (pat, obj) else (obj, pat));
+ let
+ val jpat = ObjectLogic.drop_judgment thy pat;
+ val c = Term.head_of jpat;
+ val pats =
+ if Term.is_Const c
+ then if doiff andalso is_Iff c
+ then pat :: map (ObjectLogic.ensure_propT thy) ((snd o strip_comb) jpat)
+ |> filter (is_nontrivial thy)
+ else [pat]
+ else [];
+ in filter chkmatch pats end;
fun substsize pat =
let val (_, subst) =
@@ -96,7 +121,9 @@
val match_thm = matches o refine_term;
in
- map (substsize o refine_term) (filter match_thm (extract_terms term_src))
+ map match_thm (extract_terms term_src)
+ |> flat
+ |> map substsize
|> bestmatch
end;
@@ -117,7 +144,7 @@
hd o Logic.strip_imp_prems);
val prems = Logic.prems_of_goal goal 1;
- fun try_subst prem = is_matching_thm extract_dest ctxt true prem thm;
+ fun try_subst prem = is_matching_thm false extract_dest ctxt true prem thm;
val successful = prems |> map_filter try_subst;
in
(*if possible, keep best substitution (one with smallest size)*)
@@ -127,11 +154,11 @@
then SOME (Thm.nprems_of thm - 1, foldr1 Int.min successful) else NONE
end;
-fun filter_intro ctxt goal (_, thm) =
+fun filter_intro doiff ctxt goal (_, thm) =
let
val extract_intro = (single o Thm.full_prop_of, Logic.strip_imp_concl);
val concl = Logic.concl_of_goal goal 1;
- val ss = is_matching_thm extract_intro ctxt true concl thm;
+ val ss = is_matching_thm doiff extract_intro ctxt true concl thm;
in
if is_some ss then SOME (Thm.nprems_of thm, the ss) else NONE
end;
@@ -148,7 +175,7 @@
val rule_tree = combine rule_mp rule_concl;
fun goal_tree prem = combine prem goal_concl;
fun try_subst prem =
- is_matching_thm (single, I) ctxt true (goal_tree prem) rule_tree;
+ is_matching_thm false (single, I) ctxt true (goal_tree prem) rule_tree;
val successful = prems |> map_filter try_subst;
in
(*elim rules always have assumptions, so an elim with one
@@ -183,7 +210,7 @@
val mksimps = Simplifier.mksimps (Simplifier.local_simpset_of ctxt);
val extract_simp =
(map Thm.full_prop_of o mksimps, #1 o Logic.dest_equals o Logic.strip_imp_concl);
- val ss = is_matching_thm extract_simp ctxt false t thm;
+ val ss = is_matching_thm false extract_simp ctxt false t thm;
in
if is_some ss then SOME (Thm.nprems_of thm, the ss) else NONE
end;
@@ -233,7 +260,8 @@
| filter_crit _ NONE Elim = err_no_goal "elim"
| filter_crit _ NONE Dest = err_no_goal "dest"
| filter_crit _ NONE Solves = err_no_goal "solves"
- | filter_crit ctxt (SOME goal) Intro = apfst (filter_intro ctxt (fix_goal goal))
+ | filter_crit ctxt (SOME goal) Intro = apfst (filter_intro false ctxt (fix_goal goal))
+ | filter_crit ctxt (SOME goal) IntroIff = apfst (filter_intro true ctxt (fix_goal goal))
| filter_crit ctxt (SOME goal) Elim = apfst (filter_elim ctxt (fix_goal goal))
| filter_crit ctxt (SOME goal) Dest = apfst (filter_dest ctxt (fix_goal goal))
| filter_crit ctxt (SOME goal) Solves = apfst (filter_solves ctxt goal)
@@ -428,6 +456,7 @@
val criterion =
P.reserved "name" |-- P.!!! (P.$$$ ":" |-- P.xname) >> Name ||
P.reserved "intro" >> K Intro ||
+ P.reserved "introiff" >> K IntroIff ||
P.reserved "elim" >> K Elim ||
P.reserved "dest" >> K Dest ||
P.reserved "solves" >> K Solves ||