# HG changeset patch
# User nipkow
# Date 1253098983 -7200
# Node ID db1afe8ee3d72c21aa21afe1119482e8be992c4e
# Parent  89b1f0cd9180491e431941ed447dbdc9aed2af0a# Parent  e788b33dd2b4eb76c35ed071bff2ba137e11b15d
merged

diff -r e788b33dd2b4 -r db1afe8ee3d7 src/HOL/Imperative_HOL/Array.thy
--- a/src/HOL/Imperative_HOL/Array.thy	Wed Sep 16 12:47:14 2009 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy	Wed Sep 16 13:03:03 2009 +0200
@@ -176,12 +176,11 @@
 
 code_type array (OCaml "_/ array")
 code_const Array (OCaml "failwith/ \"bare Array\"")
-code_const Array.new' (OCaml "(fun/ ()/ ->/ Array.make/ _/ _)")
+code_const Array.new' (OCaml "(fun/ ()/ ->/ Array.make/ (Big'_int.int'_of'_big'_int/ _)/ _)")
 code_const Array.of_list (OCaml "(fun/ ()/ ->/ Array.of'_list/ _)")
-code_const Array.make' (OCaml "(fun/ ()/ ->/ Array.init/ _/ _)")
-code_const Array.length' (OCaml "(fun/ ()/ ->/ Array.length/ _)")
-code_const Array.nth' (OCaml "(fun/ ()/ ->/ Array.get/ _/ _)")
-code_const Array.upd' (OCaml "(fun/ ()/ ->/ Array.set/ _/ _/ _)")
+code_const Array.length' (OCaml "(fun/ ()/ ->/ Big'_int.big'_int'_of'_int/ (Array.length/ _))")
+code_const Array.nth' (OCaml "(fun/ ()/ ->/ Array.get/ _/ (Big'_int.int'_of'_big'_int/ _))")
+code_const Array.upd' (OCaml "(fun/ ()/ ->/ Array.set/ _/ (Big'_int.int'_of'_big'_int/ _)/ _)")
 
 code_reserved OCaml Array
 
diff -r e788b33dd2b4 -r db1afe8ee3d7 src/HOL/Imperative_HOL/ex/Sublist.thy
--- a/src/HOL/Imperative_HOL/ex/Sublist.thy	Wed Sep 16 12:47:14 2009 +0200
+++ b/src/HOL/Imperative_HOL/ex/Sublist.thy	Wed Sep 16 13:03:03 2009 +0200
@@ -1,4 +1,3 @@
-(* $Id$ *)
 
 header {* Slices of lists *}
 
@@ -6,7 +5,6 @@
 imports Multiset
 begin
 
-
 lemma sublist_split: "i \<le> j \<and> j \<le> k \<Longrightarrow> sublist xs {i..<j} @ sublist xs {j..<k} = sublist xs {i..<k}" 
 apply (induct xs arbitrary: i j k)
 apply simp
diff -r e788b33dd2b4 -r db1afe8ee3d7 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Wed Sep 16 12:47:14 2009 +0200
+++ b/src/HOL/Predicate.thy	Wed Sep 16 13:03:03 2009 +0200
@@ -366,7 +366,7 @@
 definition bind :: "'a pred \<Rightarrow> ('a \<Rightarrow> 'b pred) \<Rightarrow> 'b pred" (infixl "\<guillemotright>=" 70) where
   "P \<guillemotright>= f = Pred (\<lambda>x. (\<exists>y. eval P y \<and> eval (f y) x))"
 
-instantiation pred :: (type) complete_lattice
+instantiation pred :: (type) "{complete_lattice, boolean_algebra}"
 begin
 
 definition
@@ -393,10 +393,16 @@
 definition
   [code del]: "\<Squnion>A = Pred (SUPR A eval)"
 
-instance by default
-  (auto simp add: less_eq_pred_def less_pred_def
+definition
+  "- P = Pred (- eval P)"
+
+definition
+  "P - Q = Pred (eval P - eval Q)"
+
+instance proof
+qed (auto simp add: less_eq_pred_def less_pred_def
     inf_pred_def sup_pred_def bot_pred_def top_pred_def
-    Inf_pred_def Sup_pred_def,
+    Inf_pred_def Sup_pred_def uminus_pred_def minus_pred_def fun_Compl_def bool_Compl_def,
     auto simp add: le_fun_def less_fun_def le_bool_def less_bool_def
     eval_inject mem_def)
 
@@ -464,6 +470,127 @@
 lemma supE: "eval (A \<squnion> B) x \<Longrightarrow> (eval A x \<Longrightarrow> P) \<Longrightarrow> (eval B x \<Longrightarrow> P) \<Longrightarrow> P"
   unfolding sup_pred_def by auto
 
+lemma single_not_bot [simp]:
+  "single x \<noteq> \<bottom>"
+  by (auto simp add: single_def bot_pred_def expand_fun_eq)
+
+lemma not_bot:
+  assumes "A \<noteq> \<bottom>"
+  obtains x where "eval A x"
+using assms by (cases A)
+  (auto simp add: bot_pred_def, auto simp add: mem_def)
+  
+
+subsubsection {* Emptiness check and definite choice *}
+
+definition is_empty :: "'a pred \<Rightarrow> bool" where
+  "is_empty A \<longleftrightarrow> A = \<bottom>"
+
+lemma is_empty_bot:
+  "is_empty \<bottom>"
+  by (simp add: is_empty_def)
+
+lemma not_is_empty_single:
+  "\<not> is_empty (single x)"
+  by (auto simp add: is_empty_def single_def bot_pred_def expand_fun_eq)
+
+lemma is_empty_sup:
+  "is_empty (A \<squnion> B) \<longleftrightarrow> is_empty A \<and> is_empty B"
+  by (auto simp add: is_empty_def intro: sup_eq_bot_eq1 sup_eq_bot_eq2)
+
+definition singleton :: "'a pred \<Rightarrow> 'a" where
+  "singleton A = (if \<exists>!x. eval A x then THE x. eval A x else undefined)"
+
+lemma singleton_eqI:
+  "\<exists>!x. eval A x \<Longrightarrow> eval A x \<Longrightarrow> singleton A = x"
+  by (auto simp add: singleton_def)
+
+lemma eval_singletonI:
+  "\<exists>!x. eval A x \<Longrightarrow> eval A (singleton A)"
+proof -
+  assume assm: "\<exists>!x. eval A x"
+  then obtain x where "eval A x" ..
+  moreover with assm have "singleton A = x" by (rule singleton_eqI)
+  ultimately show ?thesis by simp 
+qed
+
+lemma single_singleton:
+  "\<exists>!x. eval A x \<Longrightarrow> single (singleton A) = A"
+proof -
+  assume assm: "\<exists>!x. eval A x"
+  then have "eval A (singleton A)"
+    by (rule eval_singletonI)
+  moreover from assm have "\<And>x. eval A x \<Longrightarrow> singleton A = x"
+    by (rule singleton_eqI)
+  ultimately have "eval (single (singleton A)) = eval A"
+    by (simp (no_asm_use) add: single_def expand_fun_eq) blast
+  then show ?thesis by (simp add: eval_inject)
+qed
+
+lemma singleton_undefinedI:
+  "\<not> (\<exists>!x. eval A x) \<Longrightarrow> singleton A = undefined"
+  by (simp add: singleton_def)
+
+lemma singleton_bot:
+  "singleton \<bottom> = undefined"
+  by (auto simp add: bot_pred_def intro: singleton_undefinedI)
+
+lemma singleton_single:
+  "singleton (single x) = x"
+  by (auto simp add: intro: singleton_eqI singleI elim: singleE)
+
+lemma singleton_sup_single_single:
+  "singleton (single x \<squnion> single y) = (if x = y then x else undefined)"
+proof (cases "x = y")
+  case True then show ?thesis by (simp add: singleton_single)
+next
+  case False
+  have "eval (single x \<squnion> single y) x"
+    and "eval (single x \<squnion> single y) y"
+  by (auto intro: supI1 supI2 singleI)
+  with False have "\<not> (\<exists>!z. eval (single x \<squnion> single y) z)"
+    by blast
+  then have "singleton (single x \<squnion> single y) = undefined"
+    by (rule singleton_undefinedI)
+  with False show ?thesis by simp
+qed
+
+lemma singleton_sup_aux:
+  "singleton (A \<squnion> B) = (if A = \<bottom> then singleton B
+    else if B = \<bottom> then singleton A
+    else singleton
+      (single (singleton A) \<squnion> single (singleton B)))"
+proof (cases "(\<exists>!x. eval A x) \<and> (\<exists>!y. eval B y)")
+  case True then show ?thesis by (simp add: single_singleton)
+next
+  case False
+  from False have A_or_B:
+    "singleton A = undefined \<or> singleton B = undefined"
+    by (auto intro!: singleton_undefinedI)
+  then have rhs: "singleton
+    (single (singleton A) \<squnion> single (singleton B)) = undefined"
+    by (auto simp add: singleton_sup_single_single singleton_single)
+  from False have not_unique:
+    "\<not> (\<exists>!x. eval A x) \<or> \<not> (\<exists>!y. eval B y)" by simp
+  show ?thesis proof (cases "A \<noteq> \<bottom> \<and> B \<noteq> \<bottom>")
+    case True
+    then obtain a b where a: "eval A a" and b: "eval B b"
+      by (blast elim: not_bot)
+    with True not_unique have "\<not> (\<exists>!x. eval (A \<squnion> B) x)"
+      by (auto simp add: sup_pred_def bot_pred_def)
+    then have "singleton (A \<squnion> B) = undefined" by (rule singleton_undefinedI)
+    with True rhs show ?thesis by simp
+  next
+    case False then show ?thesis by auto
+  qed
+qed
+
+lemma singleton_sup:
+  "singleton (A \<squnion> B) = (if A = \<bottom> then singleton B
+    else if B = \<bottom> then singleton A
+    else if singleton A = singleton B then singleton A else undefined)"
+using singleton_sup_aux [of A B] by (simp only: singleton_sup_single_single)
+
 
 subsubsection {* Derived operations *}
 
@@ -630,6 +757,46 @@
 definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a pred \<Rightarrow> 'b pred" where
   "map f P = P \<guillemotright>= (single o f)"
 
+primrec null :: "'a seq \<Rightarrow> bool" where
+    "null Empty \<longleftrightarrow> True"
+  | "null (Insert x P) \<longleftrightarrow> False"
+  | "null (Join P xq) \<longleftrightarrow> is_empty P \<and> null xq"
+
+lemma null_is_empty:
+  "null xq \<longleftrightarrow> is_empty (pred_of_seq xq)"
+  by (induct xq) (simp_all add: is_empty_bot not_is_empty_single is_empty_sup)
+
+lemma is_empty_code [code]:
+  "is_empty (Seq f) \<longleftrightarrow> null (f ())"
+  by (simp add: null_is_empty Seq_def)
+
+primrec the_only :: "'a seq \<Rightarrow> 'a" where
+  [code del]: "the_only Empty = undefined"
+  | "the_only (Insert x P) = (if is_empty P then x else let y = singleton P in if x = y then x else undefined)"
+  | "the_only (Join P xq) = (if is_empty P then the_only xq else if null xq then singleton P
+       else let x = singleton P; y = the_only xq in
+       if x = y then x else undefined)"
+
+lemma the_only_singleton:
+  "the_only xq = singleton (pred_of_seq xq)"
+  by (induct xq)
+    (auto simp add: singleton_bot singleton_single is_empty_def
+    null_is_empty Let_def singleton_sup)
+
+lemma singleton_code [code]:
+  "singleton (Seq f) = (case f ()
+   of Empty \<Rightarrow> undefined
+    | Insert x P \<Rightarrow> if is_empty P then x
+        else let y = singleton P in
+          if x = y then x else undefined
+    | Join P xq \<Rightarrow> if is_empty P then the_only xq
+        else if null xq then singleton P
+        else let x = singleton P; y = the_only xq in
+          if x = y then x else undefined)"
+  by (cases "f ()")
+   (auto simp add: Seq_def the_only_singleton is_empty_def
+      null_is_empty singleton_bot singleton_single singleton_sup Let_def)
+
 ML {*
 signature PREDICATE =
 sig
@@ -707,7 +874,7 @@
   bind (infixl "\<guillemotright>=" 70)
 
 hide (open) type pred seq
-hide (open) const Pred eval single bind if_pred not_pred
-  Empty Insert Join Seq member pred_of_seq "apply" adjunct eq map
+hide (open) const Pred eval single bind is_empty singleton if_pred not_pred
+  Empty Insert Join Seq member pred_of_seq "apply" adjunct null the_only eq map
 
 end
diff -r e788b33dd2b4 -r db1afe8ee3d7 src/HOL/ex/Predicate_Compile_ex.thy
--- a/src/HOL/ex/Predicate_Compile_ex.thy	Wed Sep 16 12:47:14 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile_ex.thy	Wed Sep 16 13:03:03 2009 +0200
@@ -157,4 +157,13 @@
 values 3 "{(a,q). step (par nil nil) a q}"
 *)
 
+
+inductive divmod_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
+    "k < l \<Longrightarrow> divmod_rel k l 0 k"
+  | "k \<ge> l \<Longrightarrow> divmod_rel (k - l) l q r \<Longrightarrow> divmod_rel k l (Suc q) r"
+
+code_pred divmod_rel ..
+
+value [code] "Predicate.singleton (divmod_rel_1_2 1705 42)"
+
 end
\ No newline at end of file
diff -r e788b33dd2b4 -r db1afe8ee3d7 src/Pure/General/linear_set.scala
--- a/src/Pure/General/linear_set.scala	Wed Sep 16 12:47:14 2009 +0200
+++ b/src/Pure/General/linear_set.scala	Wed Sep 16 13:03:03 2009 +0200
@@ -1,22 +1,22 @@
 /*  Title:      Pure/General/linear_set.scala
     Author:     Makarius
-    Author:     Fabian Immler TU Munich
+    Author:     Fabian Immler, TU Munich
 
 Sets with canonical linear order, or immutable linked-lists.
 */
+
 package isabelle
 
 
 object Linear_Set
 {
   private case class Rep[A](
-    val first_elem: Option[A], val last_elem: Option[A], val body: Map[A, A])
-
-  private def empty_rep[A] = Rep[A](None, None, Map())
+    val first: Option[A], val last: Option[A], val nexts: Map[A, A], prevs: Map[A, A])
 
-  private def make[A](first_elem: Option[A], last_elem: Option[A], body: Map[A, A]): Linear_Set[A] =
-    new Linear_Set[A] { override val rep = Rep(first_elem, last_elem, body) }
+  private def empty_rep[A] = Rep[A](None, None, Map(), Map())
 
+  private def make[A](first: Option[A], last: Option[A], nexts: Map[A, A], prevs: Map[A, A])
+    : Linear_Set[A] = new Linear_Set[A] { override val rep = Rep(first, last, nexts, prevs) }
 
   def empty[A]: Linear_Set[A] = new Linear_Set
   def apply[A](elems: A*): Linear_Set[A] = empty[A] ++ elems
@@ -35,48 +35,74 @@
 
   /* auxiliary operations */
 
-  def next(elem: A) = rep.body.get(elem)
-  def prev(elem: A) = rep.body.find(_._2 == elem).map(_._1)   // slow
+  def next(elem: A): Option[A] = rep.nexts.get(elem)
+  def prev(elem: A): Option[A] = rep.prevs.get(elem)
 
-  private def _insert_after(hook: Option[A], elem: A): Linear_Set[A] =
+  def insert_after(hook: Option[A], elem: A): Linear_Set[A] =
     if (contains(elem)) throw new Linear_Set.Duplicate(elem.toString)
-    else hook match {
-      case Some(hook) =>
-        if (!contains(hook)) throw new Linear_Set.Undefined(hook.toString)
-        else if (rep.body.isDefinedAt(hook))
-          Linear_Set.make(rep.first_elem, rep.last_elem,
-            rep.body - hook + (hook -> elem) + (elem -> rep.body(hook)))
-        else Linear_Set.make(rep.first_elem, Some(elem), rep.body + (hook -> elem))
+    else
+      hook match {
+        case None =>
+          rep.first match {
+            case None => Linear_Set.make(Some(elem), Some(elem), Map(), Map())
+            case Some(elem1) =>
+              Linear_Set.make(Some(elem), rep.last,
+                rep.nexts + (elem -> elem1), rep.prevs + (elem1 -> elem))
+          }
+        case Some(elem1) =>
+          if (!contains(elem1)) throw new Linear_Set.Undefined(elem1.toString)
+          else
+            rep.nexts.get(elem1) match {
+              case None =>
+                Linear_Set.make(rep.first, Some(elem),
+                  rep.nexts + (elem1 -> elem), rep.prevs + (elem -> elem1))
+              case Some(elem2) =>
+                Linear_Set.make(rep.first, rep.last,
+                  rep.nexts + (elem1 -> elem) + (elem -> elem2),
+                  rep.prevs + (elem2 -> elem) + (elem -> elem1))
+            }
+      }
+
+  def delete_after(hook: Option[A]): Linear_Set[A] =
+    hook match {
       case None =>
-        if (isEmpty) Linear_Set.make(Some(elem), Some(elem), Map())
-        else Linear_Set.make(Some(elem), rep.last_elem, rep.body + (elem -> rep.first_elem.get))
+        rep.first match {
+          case None => throw new Linear_Set.Undefined("")
+          case Some(elem1) =>
+            rep.nexts.get(elem1) match {
+              case None => empty
+              case Some(elem2) =>
+                Linear_Set.make(Some(elem2), rep.last, rep.nexts - elem1, rep.prevs - elem2)
+            }
+        }
+      case Some(elem1) =>
+        if (!contains(elem1)) throw new Linear_Set.Undefined(elem1.toString)
+        else
+          rep.nexts.get(elem1) match {
+            case None => throw new Linear_Set.Undefined("")
+            case Some(elem2) =>
+              rep.nexts.get(elem2) match {
+                case None =>
+                  Linear_Set.make(rep.first, Some(elem1), rep.nexts - elem1, rep.prevs - elem2)
+                case Some(elem3) =>
+                  Linear_Set.make(rep.first, rep.last,
+                    rep.nexts - elem2 + (elem1 -> elem3),
+                    rep.prevs - elem2 + (elem3 -> elem1))
+              }
+          }
     }
 
-  def insert_after(hook: Option[A], elems: Seq[A]): Linear_Set[A] =
-    elems.reverse.foldLeft (this) ((ls, elem) => ls._insert_after(hook, elem))
+  def append_after(hook: Option[A], elems: Seq[A]): Linear_Set[A] =
+    (elems :\ this)((elem: A, ls: Linear_Set[A]) => ls.insert_after(hook, elem))
 
-  def delete_after(elem: Option[A]): Linear_Set[A] =
-    elem match {
-      case Some(elem) =>
-        if (!contains(elem)) throw new Linear_Set.Undefined(elem.toString)
-        else if (!rep.body.isDefinedAt(elem)) throw new Linear_Set.Undefined(null)
-        else if (rep.body(elem) == rep.last_elem.get)
-          Linear_Set.make(rep.first_elem, Some(elem), rep.body - elem)
-        else Linear_Set.make(rep.first_elem, rep.last_elem,
-          rep.body - elem - rep.body(elem) + (elem -> rep.body(rep.body(elem))))
-      case None =>
-        if (isEmpty) throw new Linear_Set.Undefined(null)
-        else if (size == 1) empty
-        else Linear_Set.make(Some(rep.body(rep.first_elem.get)), rep.last_elem, rep.body - rep.first_elem.get)
-    }
-
-  def delete_between(from: Option[A], to: Option[A]): Linear_Set[A] = {
-    if(!rep.first_elem.isDefined) this
+  def delete_between(from: Option[A], to: Option[A]): Linear_Set[A] =
+  {
+    if (!rep.first.isDefined) this
     else {
       val next =
-        if (from == rep.last_elem) None
-        else if (from == None) rep.first_elem
-        else from.map(rep.body(_))
+        if (from == rep.last) None
+        else if (from == None) rep.first
+        else from.map(rep.nexts(_))
       if (next == to) this
       else delete_after(from).delete_between(from, to)
     }
@@ -89,23 +115,23 @@
 
   def empty[B]: Linear_Set[B] = Linear_Set.empty
 
-  override def isEmpty: Boolean = !rep.last_elem.isDefined
-  def size: Int = if (isEmpty) 0 else rep.body.size + 1
+  override def isEmpty: Boolean = !rep.first.isDefined
+  def size: Int = if (isEmpty) 0 else rep.nexts.size + 1
 
   def elements = new Iterator[A] {
-    private var next_elem = rep.first_elem
+    private var next_elem = rep.first
     def hasNext = next_elem.isDefined
     def next = {
       val elem = next_elem.get
-      next_elem = if (rep.body.isDefinedAt(elem)) Some(rep.body(elem)) else None
+      next_elem = if (rep.nexts.isDefinedAt(elem)) Some(rep.nexts(elem)) else None
       elem
     }
   }
 
   def contains(elem: A): Boolean =
-    !isEmpty && (rep.last_elem.get == elem || rep.body.isDefinedAt(elem))
+    !isEmpty && (rep.last.get == elem || rep.nexts.isDefinedAt(elem))
 
-  def + (elem: A): Linear_Set[A] = _insert_after(rep.last_elem, elem)
+  def + (elem: A): Linear_Set[A] = insert_after(rep.last, elem)
 
   override def + (elem1: A, elem2: A, elems: A*): Linear_Set[A] =
     this + elem1 + elem2 ++ elems