# HG changeset patch
# User haftmann
# Date 1241631747 -7200
# Node ID 0954ed96e2d5de711b94d9c917eb6d440e7339e5
# Parent  01ac77eb660b636590991b9ecd47e31fdbf1dffd# Parent  6896c2498ac0e7f0a89bb9d93c37047124ff7609
merged

diff -r 01ac77eb660b -r 0954ed96e2d5 src/HOL/Library/Primes.thy
--- 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)"
diff -r 01ac77eb660b -r 0954ed96e2d5 src/HOL/Library/Product_ord.thy
--- 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
 
diff -r 01ac77eb660b -r 0954ed96e2d5 src/HOL/SetInterval.thy
--- 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)
diff -r 01ac77eb660b -r 0954ed96e2d5 src/HOLCF/Cfun.thy
--- 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]:
diff -r 01ac77eb660b -r 0954ed96e2d5 src/HOLCF/Cont.thy
--- 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 *}
 
diff -r 01ac77eb660b -r 0954ed96e2d5 src/HOLCF/Product_Cpo.thy
--- 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 *}
 
diff -r 01ac77eb660b -r 0954ed96e2d5 src/HOLCF/Sum_Cpo.thy
--- 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)"
diff -r 01ac77eb660b -r 0954ed96e2d5 src/Pure/Tools/find_theorems.ML
--- 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 ||