--- 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
--- 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
--- 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
--- 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
--- 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