merged;

--- a/NEWS	Thu Jun 23 17:17:40 2011 +0200
+++ b/NEWS	Thu Jun 23 18:32:13 2011 +0200
@@ -22,8 +22,10 @@
 
 * Theory loader: source files are exclusively located via the master
 directory of each theory node (where the .thy file itself resides).
-The global load path (such as src/HOL/Library) is has been
-discontinued.  INCOMPATIBILITY.
+The global load path (such as src/HOL/Library) has been discontinued.
+Note that the path element ~~ may be used to reference theories in the
+Isabelle home folder -- for instance, "~~/src/HOL/Library/FuncSet".
+INCOMPATIBILITY.
 
 * Various optional external tools are referenced more robustly and
 uniformly by explicit Isabelle settings as follows:

--- a/src/HOL/HOLCF/IsaMakefile	Thu Jun 23 17:17:40 2011 +0200
+++ b/src/HOL/HOLCF/IsaMakefile	Thu Jun 23 18:32:13 2011 +0200
@@ -135,6 +135,7 @@
 
 $(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF \
   ../Library/Nat_Infinity.thy \
+  ex/Concurrency_Monad.thy \
   ex/Dagstuhl.thy \
   ex/Dnat.thy \
   ex/Domain_Proofs.thy \

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/HOLCF/ex/Concurrency_Monad.thy	Thu Jun 23 18:32:13 2011 +0200
@@ -0,0 +1,415 @@
+(*  Title:      HOL/HOLCF/ex/Concurrency_Monad.thy
+    Author:     Brian Huffman
+*)
+
+theory Concurrency_Monad
+imports HOLCF
+begin
+
+text {* This file contains the concurrency monad example from
+  Chapter 7 of the author's PhD thesis. *}
+
+subsection {* State/nondeterminism monad, as a type synonym *}
+
+type_synonym ('s, 'a) N = "'s \<rightarrow> ('a u \<otimes> 's u)\<natural>"
+
+definition mapN :: "('a \<rightarrow> 'b) \<rightarrow> ('s, 'a) N \<rightarrow> ('s, 'b) N"
+  where "mapN = (\<Lambda> f. cfun_map\<cdot>ID\<cdot>(convex_map\<cdot>(sprod_map\<cdot>(u_map\<cdot>f)\<cdot>ID)))"
+
+definition unitN :: "'a \<rightarrow> ('s, 'a) N"
+  where "unitN = (\<Lambda> x. (\<Lambda> s. convex_unit\<cdot>(:up\<cdot>x, up\<cdot>s:)))"
+
+definition bindN :: "('s, 'a) N \<rightarrow> ('a \<rightarrow> ('s, 'b) N) \<rightarrow> ('s, 'b) N"
+  where "bindN = (\<Lambda> c k. (\<Lambda> s. convex_bind\<cdot>(c\<cdot>s)\<cdot>(\<Lambda> (:up\<cdot>x, up\<cdot>s':). k\<cdot>x\<cdot>s')))"
+
+definition plusN :: "('s, 'a) N \<rightarrow> ('s, 'a) N \<rightarrow> ('s, 'a) N"
+  where "plusN = (\<Lambda> a b. (\<Lambda> s. convex_plus\<cdot>(a\<cdot>s)\<cdot>(b\<cdot>s)))"
+
+lemma mapN_ID: "mapN\<cdot>ID = ID"
+by (simp add: mapN_def domain_map_ID)
+
+lemma mapN_mapN: "mapN\<cdot>f\<cdot>(mapN\<cdot>g\<cdot>m) = mapN\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>m"
+unfolding mapN_def ID_def
+by (simp add: cfun_map_map convex_map_map sprod_map_map u_map_map eta_cfun)
+
+lemma mapN_unitN: "mapN\<cdot>f\<cdot>(unitN\<cdot>x) = unitN\<cdot>(f\<cdot>x)"
+unfolding mapN_def unitN_def
+by (simp add: cfun_map_def)
+
+lemma bindN_unitN: "bindN\<cdot>(unitN\<cdot>a)\<cdot>f = f\<cdot>a"
+by (simp add: unitN_def bindN_def eta_cfun)
+
+lemma mapN_conv_bindN: "mapN\<cdot>f\<cdot>m = bindN\<cdot>m\<cdot>(unitN oo f)"
+apply (simp add: mapN_def bindN_def unitN_def)
+apply (rule cfun_eqI, simp)
+apply (simp add: convex_map_def)
+apply (rule cfun_arg_cong)
+apply (rule cfun_eqI, simp, rename_tac p)
+apply (case_tac p, simp)
+apply (case_tac x, simp)
+apply (case_tac y, simp)
+apply simp
+done
+
+lemma bindN_unitN_right: "bindN\<cdot>m\<cdot>unitN = m"
+proof -
+  have "mapN\<cdot>ID\<cdot>m = m" by (simp add: mapN_ID)
+  thus ?thesis by (simp add: mapN_conv_bindN)
+qed
+
+lemma bindN_bindN:
+  "bindN\<cdot>(bindN\<cdot>m\<cdot>f)\<cdot>g = bindN\<cdot>m\<cdot>(\<Lambda> x. bindN\<cdot>(f\<cdot>x)\<cdot>g)"
+apply (rule cfun_eqI, rename_tac s)
+apply (simp add: bindN_def)
+apply (simp add: convex_bind_bind)
+apply (rule cfun_arg_cong)
+apply (rule cfun_eqI, rename_tac w)
+apply (case_tac w, simp)
+apply (case_tac x, simp)
+apply (case_tac y, simp)
+apply simp
+done
+
+lemma mapN_bindN: "mapN\<cdot>f\<cdot>(bindN\<cdot>m\<cdot>g) = bindN\<cdot>m\<cdot>(\<Lambda> x. mapN\<cdot>f\<cdot>(g\<cdot>x))"
+by (simp add: mapN_conv_bindN bindN_bindN)
+
+lemma bindN_mapN: "bindN\<cdot>(mapN\<cdot>f\<cdot>m)\<cdot>g = bindN\<cdot>m\<cdot>(\<Lambda> x. g\<cdot>(f\<cdot>x))"
+by (simp add: mapN_conv_bindN bindN_bindN bindN_unitN)
+
+lemma mapN_plusN:
+  "mapN\<cdot>f\<cdot>(plusN\<cdot>a\<cdot>b) = plusN\<cdot>(mapN\<cdot>f\<cdot>a)\<cdot>(mapN\<cdot>f\<cdot>b)"
+unfolding mapN_def plusN_def by (simp add: cfun_map_def)
+
+lemma plusN_commute: "plusN\<cdot>a\<cdot>b = plusN\<cdot>b\<cdot>a"
+unfolding plusN_def by (simp add: convex_plus_commute)
+
+lemma plusN_assoc: "plusN\<cdot>(plusN\<cdot>a\<cdot>b)\<cdot>c = plusN\<cdot>a\<cdot>(plusN\<cdot>b\<cdot>c)"
+unfolding plusN_def by (simp add: convex_plus_assoc)
+
+lemma plusN_absorb: "plusN\<cdot>a\<cdot>a = a"
+unfolding plusN_def by (simp add: eta_cfun)
+
+
+subsection {* Resumption-state-nondeterminism monad *}
+
+domain ('s, 'a) R = Done (lazy "'a") | More (lazy "('s, ('s, 'a) R) N")
+
+thm R.take_induct
+
+lemma R_induct [case_names adm bottom Done More, induct type: R]:
+  fixes P :: "('s, 'a) R \<Rightarrow> bool"
+  assumes adm: "adm P"
+  assumes bottom: "P \<bottom>"
+  assumes Done: "\<And>x. P (Done\<cdot>x)"
+  assumes More: "\<And>p c. (\<And>r::('s, 'a) R. P (p\<cdot>r)) \<Longrightarrow> P (More\<cdot>(mapN\<cdot>p\<cdot>c))"
+  shows "P r"
+proof (induct r rule: R.take_induct)
+  show "adm P" by fact
+next
+  fix n
+  show "P (R_take n\<cdot>r)"
+  proof (induct n arbitrary: r)
+    case 0 show ?case by (simp add: bottom)
+  next
+    case (Suc n r)
+    show ?case
+      apply (cases r)
+      apply (simp add: bottom)
+      apply (simp add: Done)
+      using More [OF Suc]
+      apply (simp add: mapN_def)
+      done
+  qed
+qed
+
+declare R.take_rews(2) [simp del]
+
+lemma R_take_Suc_More [simp]:
+  "R_take (Suc n)\<cdot>(More\<cdot>k) = More\<cdot>(mapN\<cdot>(R_take n)\<cdot>k)"
+by (simp add: mapN_def R.take_rews(2))
+
+
+subsection {* Map function *}
+
+fixrec mapR :: "('a \<rightarrow> 'b) \<rightarrow> ('s, 'a) R \<rightarrow> ('s, 'b) R"
+  where "mapR\<cdot>f\<cdot>(Done\<cdot>a) = Done\<cdot>(f\<cdot>a)"
+  | "mapR\<cdot>f\<cdot>(More\<cdot>k) = More\<cdot>(mapN\<cdot>(mapR\<cdot>f)\<cdot>k)"
+
+lemma mapR_strict [simp]: "mapR\<cdot>f\<cdot>\<bottom> = \<bottom>"
+by fixrec_simp
+
+lemma mapR_mapR: "mapR\<cdot>f\<cdot>(mapR\<cdot>g\<cdot>r) = mapR\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>r"
+by (induct r) (simp_all add: mapN_mapN)
+
+lemma mapR_ID: "mapR\<cdot>ID\<cdot>r = r"
+by (induct r) (simp_all add: mapN_mapN eta_cfun)
+
+lemma "mapR\<cdot>f\<cdot>(mapR\<cdot>g\<cdot>r) = mapR\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>r"
+apply (induct r)
+apply simp
+apply simp
+apply simp
+apply (simp (no_asm))
+apply (simp (no_asm) add: mapN_mapN)
+apply simp
+done
+
+
+subsection {* Monadic bind function *}
+
+fixrec bindR :: "('s, 'a) R \<rightarrow> ('a \<rightarrow> ('s, 'b) R) \<rightarrow> ('s, 'b) R"
+  where "bindR\<cdot>(Done\<cdot>x)\<cdot>k = k\<cdot>x"
+  | "bindR\<cdot>(More\<cdot>c)\<cdot>k = More\<cdot>(mapN\<cdot>(\<Lambda> r. bindR\<cdot>r\<cdot>k)\<cdot>c)"
+
+lemma bindR_strict [simp]: "bindR\<cdot>\<bottom>\<cdot>k = \<bottom>"
+by fixrec_simp
+
+lemma bindR_Done_right: "bindR\<cdot>r\<cdot>Done = r"
+by (induct r) (simp_all add: mapN_mapN eta_cfun)
+
+lemma mapR_conv_bindR: "mapR\<cdot>f\<cdot>r = bindR\<cdot>r\<cdot>(\<Lambda> x. Done\<cdot>(f\<cdot>x))"
+by (induct r) (simp_all add: mapN_mapN)
+
+lemma bindR_bindR: "bindR\<cdot>(bindR\<cdot>r\<cdot>f)\<cdot>g = bindR\<cdot>r\<cdot>(\<Lambda> x. bindR\<cdot>(f\<cdot>x)\<cdot>g)"
+by (induct r) (simp_all add: mapN_mapN)
+
+lemma "bindR\<cdot>(bindR\<cdot>r\<cdot>f)\<cdot>g = bindR\<cdot>r\<cdot>(\<Lambda> x. bindR\<cdot>(f\<cdot>x)\<cdot>g)"
+apply (induct r)
+apply (simp_all add: mapN_mapN)
+done
+
+subsection {* Zip function *}
+
+fixrec zipR :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('s, 'a) R \<rightarrow> ('s, 'b) R \<rightarrow> ('s, 'c) R"
+  where zipR_Done_Done:
+    "zipR\<cdot>f\<cdot>(Done\<cdot>x)\<cdot>(Done\<cdot>y) = Done\<cdot>(f\<cdot>x\<cdot>y)"
+  | zipR_Done_More:
+    "zipR\<cdot>f\<cdot>(Done\<cdot>x)\<cdot>(More\<cdot>b) =
+      More\<cdot>(mapN\<cdot>(\<Lambda> r. zipR\<cdot>f\<cdot>(Done\<cdot>x)\<cdot>r)\<cdot>b)"
+  | zipR_More_Done:
+    "zipR\<cdot>f\<cdot>(More\<cdot>a)\<cdot>(Done\<cdot>y) =
+      More\<cdot>(mapN\<cdot>(\<Lambda> r. zipR\<cdot>f\<cdot>r\<cdot>(Done\<cdot>y))\<cdot>a)"
+  | zipR_More_More:
+    "zipR\<cdot>f\<cdot>(More\<cdot>a)\<cdot>(More\<cdot>b) =
+      More\<cdot>(plusN\<cdot>(mapN\<cdot>(\<Lambda> r. zipR\<cdot>f\<cdot>(More\<cdot>a)\<cdot>r)\<cdot>b)
+                 \<cdot>(mapN\<cdot>(\<Lambda> r. zipR\<cdot>f\<cdot>r\<cdot>(More\<cdot>b))\<cdot>a))"
+
+lemma zipR_strict1 [simp]: "zipR\<cdot>f\<cdot>\<bottom>\<cdot>r = \<bottom>"
+by fixrec_simp
+
+lemma zipR_strict2 [simp]: "zipR\<cdot>f\<cdot>r\<cdot>\<bottom> = \<bottom>"
+by (fixrec_simp, cases r, simp_all)
+
+abbreviation apR (infixl "\<diamond>" 70)
+  where "a \<diamond> b \<equiv> zipR\<cdot>ID\<cdot>a\<cdot>b"
+
+text {* Proofs that @{text zipR} satisfies the applicative functor laws: *}
+
+lemma R_homomorphism: "Done\<cdot>f \<diamond> Done\<cdot>x = Done\<cdot>(f\<cdot>x)"
+  by simp
+
+lemma R_identity: "Done\<cdot>ID \<diamond> r = r"
+  by (induct r, simp_all add: mapN_mapN eta_cfun)
+
+lemma R_interchange: "r \<diamond> Done\<cdot>x = Done\<cdot>(\<Lambda> f. f\<cdot>x) \<diamond> r"
+  by (induct r, simp_all add: mapN_mapN)
+
+text {* The associativity rule is the hard one! *}
+
+lemma R_associativity: "Done\<cdot>cfcomp \<diamond> r1 \<diamond> r2 \<diamond> r3 = r1 \<diamond> (r2 \<diamond> r3)"
+proof (induct r1 arbitrary: r2 r3)
+  case (Done x1) thus ?case
+  proof (induct r2 arbitrary: r3)
+    case (Done x2) thus ?case
+    proof (induct r3)
+      case (More p3 c3) thus ?case (* Done/Done/More *)
+        by (simp add: mapN_mapN)
+    qed simp_all
+  next
+    case (More p2 c2) thus ?case
+    proof (induct r3)
+      case (Done x3) thus ?case (* Done/More/Done *)
+        by (simp add: mapN_mapN)
+    next
+      case (More p3 c3) thus ?case (* Done/More/More *)
+        by (simp add: mapN_mapN mapN_plusN)
+    qed simp_all
+  qed simp_all
+next
+  case (More p1 c1) thus ?case
+  proof (induct r2 arbitrary: r3)
+    case (Done y) thus ?case
+    proof (induct r3)
+      case (Done x3) thus ?case
+        by (simp add: mapN_mapN)
+    next
+      case (More p3 c3) thus ?case
+        by (simp add: mapN_mapN)
+    qed simp_all
+  next
+    case (More p2 c2) thus ?case
+    proof (induct r3)
+      case (Done x3) thus ?case
+        by (simp add: mapN_mapN mapN_plusN)
+    next
+      case (More p3 c3) thus ?case
+        by (simp add: mapN_mapN mapN_plusN plusN_assoc)
+    qed simp_all
+  qed simp_all
+qed simp_all
+
+text {* Other miscellaneous properties about @{text zipR}: *}
+
+lemma zipR_Done_left:
+  shows "zipR\<cdot>f\<cdot>(Done\<cdot>x)\<cdot>r = mapR\<cdot>(f\<cdot>x)\<cdot>r"
+by (induct r) (simp_all add: mapN_mapN)
+
+lemma zipR_Done_right:
+  shows "zipR\<cdot>f\<cdot>r\<cdot>(Done\<cdot>y) = mapR\<cdot>(\<Lambda> x. f\<cdot>x\<cdot>y)\<cdot>r"
+by (induct r) (simp_all add: mapN_mapN)
+
+lemma mapR_zipR: "mapR\<cdot>h\<cdot>(zipR\<cdot>f\<cdot>a\<cdot>b) = zipR\<cdot>(\<Lambda> x y. h\<cdot>(f\<cdot>x\<cdot>y))\<cdot>a\<cdot>b"
+apply (induct a arbitrary: b)
+apply simp
+apply simp
+apply (simp add: zipR_Done_left zipR_Done_right mapR_mapR)
+apply (induct_tac b)
+apply simp
+apply simp
+apply (simp add: mapN_mapN)
+apply (simp add: mapN_mapN mapN_plusN)
+done
+
+lemma zipR_mapR_left: "zipR\<cdot>f\<cdot>(mapR\<cdot>h\<cdot>a)\<cdot>b = zipR\<cdot>(\<Lambda> x y. f\<cdot>(h\<cdot>x)\<cdot>y)\<cdot>a\<cdot>b"
+apply (induct a arbitrary: b)
+apply simp
+apply simp
+apply (simp add: zipR_Done_left zipR_Done_right eta_cfun)
+apply (simp add: mapN_mapN)
+apply (induct_tac b)
+apply simp
+apply simp
+apply (simp add: mapN_mapN)
+apply (simp add: mapN_mapN)
+done
+
+lemma zipR_mapR_right: "zipR\<cdot>f\<cdot>a\<cdot>(mapR\<cdot>h\<cdot>b) = zipR\<cdot>(\<Lambda> x y. f\<cdot>x\<cdot>(h\<cdot>y))\<cdot>a\<cdot>b"
+apply (induct b arbitrary: a)
+apply simp
+apply simp
+apply (simp add: zipR_Done_left zipR_Done_right)
+apply (simp add: mapN_mapN)
+apply (induct_tac a)
+apply simp
+apply simp
+apply (simp add: mapN_mapN)
+apply (simp add: mapN_mapN)
+done
+
+lemma zipR_commute:
+  assumes f: "\<And>x y. f\<cdot>x\<cdot>y = g\<cdot>y\<cdot>x"
+  shows "zipR\<cdot>f\<cdot>a\<cdot>b = zipR\<cdot>g\<cdot>b\<cdot>a"
+apply (induct a arbitrary: b)
+apply simp
+apply simp
+apply (simp add: zipR_Done_left zipR_Done_right f [symmetric] eta_cfun)
+apply (induct_tac b)
+apply simp
+apply simp
+apply (simp add: mapN_mapN)
+apply (simp add: mapN_mapN mapN_plusN plusN_commute)
+done
+
+lemma zipR_assoc:
+  fixes a :: "('s, 'a) R" and b :: "('s, 'b) R" and c :: "('s, 'c) R"
+  fixes f :: "'a \<rightarrow> 'b \<rightarrow> 'd" and g :: "'d \<rightarrow> 'c \<rightarrow> 'e"
+  assumes gf: "\<And>x y z. g\<cdot>(f\<cdot>x\<cdot>y)\<cdot>z = h\<cdot>x\<cdot>(k\<cdot>y\<cdot>z)"
+  shows "zipR\<cdot>g\<cdot>(zipR\<cdot>f\<cdot>a\<cdot>b)\<cdot>c = zipR\<cdot>h\<cdot>a\<cdot>(zipR\<cdot>k\<cdot>b\<cdot>c)" (is "?P a b c")
+ apply (induct a arbitrary: b c)
+    apply simp
+   apply simp
+  apply (simp add: zipR_Done_left zipR_Done_right)
+  apply (simp add: zipR_mapR_left mapR_zipR gf)
+ apply (rename_tac pA kA b c)
+ apply (rule_tac x=c in spec)
+ apply (induct_tac b)
+    apply simp
+   apply simp
+  apply (simp add: mapN_mapN)
+  apply (simp add: zipR_Done_left zipR_Done_right eta_cfun)
+  apply (simp add: zipR_mapR_right)
+  apply (rule allI, rename_tac c)
+  apply (induct_tac c)
+     apply simp
+    apply simp
+   apply (rename_tac z)
+   apply (simp add: mapN_mapN)
+   apply (simp add: zipR_mapR_left gf)
+  apply (rename_tac pC kC)
+  apply (simp add: mapN_mapN)
+  apply (simp add: zipR_mapR_left gf)
+ apply (rename_tac pB kB)
+ apply (rule allI, rename_tac c)
+ apply (induct_tac c)
+    apply simp
+   apply simp
+  apply (simp add: mapN_mapN mapN_plusN)
+ apply (rename_tac pC kC)
+ apply (simp add: mapN_mapN mapN_plusN plusN_assoc)
+done
+
+text {* Alternative proof using take lemma. *}
+
+lemma
+  fixes a :: "('s, 'a) R" and b :: "('s, 'b) R" and c :: "('s, 'c) R"
+  fixes f :: "'a \<rightarrow> 'b \<rightarrow> 'd" and g :: "'d \<rightarrow> 'c \<rightarrow> 'e"
+  assumes gf: "\<And>x y z. g\<cdot>(f\<cdot>x\<cdot>y)\<cdot>z = h\<cdot>x\<cdot>(k\<cdot>y\<cdot>z)"
+  shows "zipR\<cdot>g\<cdot>(zipR\<cdot>f\<cdot>a\<cdot>b)\<cdot>c = zipR\<cdot>h\<cdot>a\<cdot>(zipR\<cdot>k\<cdot>b\<cdot>c)"
+    (is "?lhs = ?rhs" is "?P a b c")
+proof (rule R.take_lemma)
+  fix n show "R_take n\<cdot>?lhs = R_take n\<cdot>?rhs"
+  proof (induct n arbitrary: a b c)
+    case (0 a b c)
+    show ?case by simp
+  next
+    case (Suc n a b c)
+    note IH = this
+    let ?P = ?case
+    show ?case
+    proof (cases a)
+      case bottom thus ?P by simp
+    next
+      case (Done x) thus ?P
+        by (simp add: zipR_Done_left zipR_mapR_left mapR_zipR gf)
+    next
+      case (More nA) thus ?P
+      proof (cases b)
+        case bottom thus ?P by simp
+      next
+        case (Done y) thus ?P
+          by (simp add: zipR_Done_left zipR_Done_right
+            zipR_mapR_left zipR_mapR_right gf)
+      next
+        case (More nB) thus ?P
+        proof (cases c)
+          case bottom thus ?P by simp
+        next
+          case (Done z) thus ?P
+            by (simp add: zipR_Done_right mapR_zipR zipR_mapR_right gf)
+        next
+          case (More nC)
+          note H = `a = More\<cdot>nA` `b = More\<cdot>nB` `c = More\<cdot>nC`
+          show ?P
+            apply (simp only: H zipR_More_More)
+            apply (simplesubst zipR_More_More [of f, symmetric])
+            apply (simplesubst zipR_More_More [of k, symmetric])
+            apply (simp only: H [symmetric])
+            apply (simp add: mapN_mapN mapN_plusN plusN_assoc IH)
+            done
+        qed
+      qed
+    qed
+  qed
+qed
+
+end

--- a/src/HOL/HOLCF/ex/ROOT.ML	Thu Jun 23 17:17:40 2011 +0200
+++ b/src/HOL/HOLCF/ex/ROOT.ML	Thu Jun 23 18:32:13 2011 +0200
@@ -4,6 +4,7 @@
 *)
 
 use_thys ["Dnat", "Dagstuhl", "Focus_ex", "Fix2", "Hoare",
+  "Concurrency_Monad",
   "Loop", "Powerdomain_ex", "Domain_Proofs",
   "Letrec",
   "Pattern_Match"];

--- a/src/HOL/Int.thy	Thu Jun 23 17:17:40 2011 +0200
+++ b/src/HOL/Int.thy	Thu Jun 23 18:32:13 2011 +0200
@@ -941,6 +941,15 @@
 class number_ring = number + comm_ring_1 +
   assumes number_of_eq: "number_of k = of_int k"
 
+class number_semiring = number + comm_semiring_1 +
+  assumes number_of_int: "number_of (of_nat n) = of_nat n"
+
+instance number_ring \<subseteq> number_semiring
+proof
+  fix n show "number_of (of_nat n) = (of_nat n :: 'a)"
+    unfolding number_of_eq by (rule of_int_of_nat_eq)
+qed
+
 text {* self-embedding of the integers *}
 
 instantiation int :: number_ring
@@ -995,13 +1004,23 @@
   Converting numerals 0 and 1 to their abstract versions.
 *}
 
+lemma semiring_numeral_0_eq_0:
+  "Numeral0 = (0::'a::number_semiring)"
+  using number_of_int [where 'a='a and n=0]
+  unfolding numeral_simps by simp
+
+lemma semiring_numeral_1_eq_1:
+  "Numeral1 = (1::'a::number_semiring)"
+  using number_of_int [where 'a='a and n=1]
+  unfolding numeral_simps by simp
+
 lemma numeral_0_eq_0 [simp, code_post]:
   "Numeral0 = (0::'a::number_ring)"
-  unfolding number_of_eq numeral_simps by simp
+  by (rule semiring_numeral_0_eq_0)
 
 lemma numeral_1_eq_1 [simp, code_post]:
   "Numeral1 = (1::'a::number_ring)"
-  unfolding number_of_eq numeral_simps by simp
+  by (rule semiring_numeral_1_eq_1)
 
 text {*
   Special-case simplification for small constants.
@@ -1467,8 +1486,12 @@
 lemmas add_number_of_eq = number_of_add [symmetric]
 
 text{*Allow 1 on either or both sides*}
+lemma semiring_one_add_one_is_two: "1 + 1 = (2::'a::number_semiring)"
+  using number_of_int [where 'a='a and n="Suc (Suc 0)"]
+  by (simp add: numeral_simps)
+
 lemma one_add_one_is_two: "1 + 1 = (2::'a::number_ring)"
-by (simp del: numeral_1_eq_1 add: numeral_1_eq_1 [symmetric])
+by (rule semiring_one_add_one_is_two)
 
 lemmas add_special =
     one_add_one_is_two
@@ -1555,11 +1578,18 @@
 by (simp add: number_of_eq) 
 
 text{*Lemmas for specialist use, NOT as default simprules*}
+(* TODO: see if semiring duplication can be removed without breaking proofs *)
+lemma semiring_mult_2: "2 * z = (z+z::'a::number_semiring)"
+unfolding semiring_one_add_one_is_two [symmetric] left_distrib by simp
+
+lemma semiring_mult_2_right: "z * 2 = (z+z::'a::number_semiring)"
+by (subst mult_commute, rule semiring_mult_2)
+
 lemma mult_2: "2 * z = (z+z::'a::number_ring)"
-unfolding one_add_one_is_two [symmetric] left_distrib by simp
+by (rule semiring_mult_2)
 
 lemma mult_2_right: "z * 2 = (z+z::'a::number_ring)"
-by (subst mult_commute, rule mult_2)
+by (rule semiring_mult_2_right)
 
 
 subsection{*More Inequality Reasoning*}

--- a/src/HOL/IsaMakefile	Thu Jun 23 17:17:40 2011 +0200
+++ b/src/HOL/IsaMakefile	Thu Jun 23 18:32:13 2011 +0200
@@ -1594,6 +1594,7 @@
 HOLCF-ex: HOLCF $(LOG)/HOLCF-ex.gz
 
 $(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF \
+  HOLCF/ex/Concurrency_Monad.thy \
   HOLCF/ex/Dagstuhl.thy \
   HOLCF/ex/Dnat.thy \
   HOLCF/ex/Domain_Proofs.thy \

--- a/src/HOL/Library/Nat_Infinity.thy	Thu Jun 23 17:17:40 2011 +0200
+++ b/src/HOL/Library/Nat_Infinity.thy	Thu Jun 23 18:32:13 2011 +0200
@@ -240,6 +240,12 @@
   apply (simp add: plus_1_iSuc iSuc_Fin)
   done
 
+instance inat :: number_semiring
+proof
+  fix n show "number_of (int n) = (of_nat n :: inat)"
+    unfolding number_of_inat_def number_of_int of_nat_id of_nat_eq_Fin ..
+qed
+
 instance inat :: semiring_char_0 proof
   have "inj Fin" by (rule injI) simp
   then show "inj (\<lambda>n. of_nat n :: inat)" by (simp add: of_nat_eq_Fin)

--- a/src/HOL/Nat_Numeral.thy	Thu Jun 23 17:17:40 2011 +0200
+++ b/src/HOL/Nat_Numeral.thy	Thu Jun 23 18:32:13 2011 +0200
@@ -15,14 +15,17 @@
   Arithmetic for naturals is reduced to that for the non-negative integers.
 *}
 
-instantiation nat :: number
+instantiation nat :: number_semiring
 begin
 
 definition
   nat_number_of_def [code_unfold, code del]: "number_of v = nat (number_of v)"
 
-instance ..
-
+instance proof
+  fix n show "number_of (int n) = (of_nat n :: nat)"
+    unfolding nat_number_of_def number_of_eq by simp
+qed
+ 
 end
 
 lemma [code_post]:
@@ -250,9 +253,9 @@
 end
 
 lemma power2_sum:
-  fixes x y :: "'a::number_ring"
+  fixes x y :: "'a::number_semiring"
   shows "(x + y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> + 2 * x * y"
-  by (simp add: ring_distribs power2_eq_square mult_2) (rule mult_commute)
+  by (simp add: algebra_simps power2_eq_square semiring_mult_2_right)
 
 lemma power2_diff:
   fixes x y :: "'a::number_ring"
@@ -345,6 +348,9 @@
   unfolding nat_number_of_def number_of_is_id neg_def
   by simp
 
+lemma nonneg_int_cases:
+  fixes k :: int assumes "0 \<le> k" obtains n where "k = of_nat n"
+  using assms by (cases k, simp, simp)
 
 subsubsection{*Successor *}
 
@@ -390,7 +396,30 @@
   by (simp add: nat_add_distrib)
 
 lemma nat_1_add_1 [simp]: "1 + 1 = (2::nat)"
-  by (rule int_int_eq [THEN iffD1]) simp
+  by (rule semiring_one_add_one_is_two)
+
+text {* TODO: replace simp rules above with these generic ones: *}
+
+lemma semiring_add_number_of:
+  "\<lbrakk>Int.Pls \<le> v; Int.Pls \<le> v'\<rbrakk> \<Longrightarrow>
+    (number_of v :: 'a::number_semiring) + number_of v' = number_of (v + v')"
+  unfolding Int.Pls_def
+  by (elim nonneg_int_cases,
+    simp only: number_of_int of_nat_add [symmetric])
+
+lemma semiring_number_of_add_1:
+  "Int.Pls \<le> v \<Longrightarrow>
+    number_of v + (1::'a::number_semiring) = number_of (Int.succ v)"
+  unfolding Int.Pls_def Int.succ_def
+  by (elim nonneg_int_cases,
+    simp only: number_of_int add_commute [where b=1] of_nat_Suc [symmetric])
+
+lemma semiring_1_add_number_of:
+  "Int.Pls \<le> v \<Longrightarrow>
+    (1::'a::number_semiring) + number_of v = number_of (Int.succ v)"
+  unfolding Int.Pls_def Int.succ_def
+  by (elim nonneg_int_cases,
+    simp only: number_of_int add_commute [where b=1] of_nat_Suc [symmetric])
 
 
 subsubsection{*Subtraction *}
@@ -426,6 +455,14 @@
   unfolding nat_number_of_def number_of_is_id numeral_simps
   by (simp add: nat_mult_distrib)
 
+(* TODO: replace mult_nat_number_of with this next rule *)
+lemma semiring_mult_number_of:
+  "\<lbrakk>Int.Pls \<le> v; Int.Pls \<le> v'\<rbrakk> \<Longrightarrow>
+    (number_of v :: 'a::number_semiring) * number_of v' = number_of (v * v')"
+  unfolding Int.Pls_def
+  by (elim nonneg_int_cases,
+    simp only: number_of_int of_nat_mult [symmetric])
+
 
 subsection{*Comparisons*}
 
@@ -647,13 +684,13 @@
 text{*For arbitrary rings*}
 
 lemma power_number_of_even:
-  fixes z :: "'a::number_ring"
+  fixes z :: "'a::monoid_mult"
   shows "z ^ number_of (Int.Bit0 w) = (let w = z ^ (number_of w) in w * w)"
 by (cases "w \<ge> 0") (auto simp add: Let_def Bit0_def nat_number_of_def number_of_is_id
   nat_add_distrib power_add simp del: nat_number_of)
 
 lemma power_number_of_odd:
-  fixes z :: "'a::number_ring"
+  fixes z :: "'a::monoid_mult"
   shows "z ^ number_of (Int.Bit1 w) = (if (0::int) <= number_of w
      then (let w = z ^ (number_of w) in z * w * w) else 1)"
 unfolding Let_def Bit1_def nat_number_of_def number_of_is_id
@@ -842,10 +879,10 @@
 
 text{*Lemmas for specialist use, NOT as default simprules*}
 lemma nat_mult_2: "2 * z = (z+z::nat)"
-unfolding nat_1_add_1 [symmetric] left_distrib by simp
+by (rule semiring_mult_2)
 
 lemma nat_mult_2_right: "z * 2 = (z+z::nat)"
-by (subst mult_commute, rule nat_mult_2)
+by (rule semiring_mult_2_right)
 
 text{*Case analysis on @{term "n<2"}*}
 lemma less_2_cases: "(n::nat) < 2 ==> n = 0 | n = Suc 0"

--- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Jun 23 17:17:40 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Jun 23 18:32:13 2011 +0200
@@ -406,7 +406,7 @@
                (K (750, ["mangled_tags?"]) (* FUDGE *))
 val remote_vampire =
   remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"]
-               (K (150, ["mangled_preds?"]) (* FUDGE *))
+               (K (200, ["mangled_preds?"]) (* FUDGE *))
 val remote_z3_atp =
   remotify_atp z3_atp "Z3" ["2.18"] (K (250, ["mangled_preds?"]) (* FUDGE *))
 val remote_leo2 =
@@ -418,7 +418,7 @@
 val remote_sine_e =
   remote_atp sine_eN "SInE" ["0.4"] [] (#known_failures e_config)
              Axiom Conjecture [FOF]
-             (K (500, ["poly_tags_heavy"]) (* FUDGE *))
+             (K (500, ["mangled_preds?"]) (* FUDGE *))
 val remote_snark =
   remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
              [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis

--- a/src/HOL/Tools/ATP/scripts/remote_atp	Thu Jun 23 17:17:40 2011 +0200
+++ b/src/HOL/Tools/ATP/scripts/remote_atp	Thu Jun 23 18:32:13 2011 +0200
@@ -94,7 +94,7 @@
 $Agent->env_proxy;
 if (exists($Options{'t'})) {
   # give server more time to respond
-  $Agent->timeout($Options{'t'} + 10);
+  $Agent->timeout($Options{'t'} + 15);
 }
 my $Request = POST($SystemOnTPTPFormReplyURL,
 	Content_Type => 'form-data',Content => \%URLParameters);