# HG changeset patch
# User boehmes
# Date 1251807038 -7200
# Node ID 8ca2f3500dbcc9f5902ed79b30cc94ab84ca2c1d
# Parent  1ad7d4fc0954fd86d6500a4e832b6567406d2484# Parent  87f0e1b2d3f2bf08a8b208524827b89c07f9881a
merged

diff -r 1ad7d4fc0954 -r 8ca2f3500dbc NEWS
--- a/NEWS	Tue Sep 01 14:09:59 2009 +0200
+++ b/NEWS	Tue Sep 01 14:10:38 2009 +0200
@@ -112,6 +112,9 @@
 Suc_eq_add_numeral_1_left -> Suc_eq_plus1_left
 Suc_plus1 -> Suc_eq_plus1
 
+* Moved theorems:
+Wellfounded.in_inv_image -> Relation.in_inv_image
+
 * New sledgehammer option "Full Types" in Proof General settings menu.
 Causes full type information to be output to the ATPs.  This slows
 ATPs down considerably but eliminates a source of unsound "proofs"
diff -r 1ad7d4fc0954 -r 8ca2f3500dbc src/HOL/MicroJava/J/TypeRel.thy
--- a/src/HOL/MicroJava/J/TypeRel.thy	Tue Sep 01 14:09:59 2009 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.thy	Tue Sep 01 14:10:38 2009 +0200
@@ -97,6 +97,14 @@
   qed
 qed
 
+text {* Code generator setup (FIXME!) *}
+
+consts_code
+  "wfrec"   ("\<module>wfrec?")
+attach {*
+fun wfrec f x = f (wfrec f) x;
+*}
+
 consts
 
   method :: "'c prog \<times> cname => ( sig   \<rightharpoonup> cname \<times> ty \<times> 'c)" (* ###curry *)
diff -r 1ad7d4fc0954 -r 8ca2f3500dbc src/HOL/Recdef.thy
--- a/src/HOL/Recdef.thy	Tue Sep 01 14:09:59 2009 +0200
+++ b/src/HOL/Recdef.thy	Tue Sep 01 14:10:38 2009 +0200
@@ -19,6 +19,65 @@
   ("Tools/recdef.ML")
 begin
 
+inductive
+  wfrec_rel :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b => bool"
+  for R :: "('a * 'a) set"
+  and F :: "('a => 'b) => 'a => 'b"
+where
+  wfrecI: "ALL z. (z, x) : R --> wfrec_rel R F z (g z) ==>
+            wfrec_rel R F x (F g x)"
+
+constdefs
+  cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b"
+  "cut f r x == (%y. if (y,x):r then f y else undefined)"
+
+  adm_wf :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => bool"
+  "adm_wf R F == ALL f g x.
+     (ALL z. (z, x) : R --> f z = g z) --> F f x = F g x"
+
+  wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b"
+  [code del]: "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
+
+subsection{*Well-Founded Recursion*}
+
+text{*cut*}
+
+lemma cuts_eq: "(cut f r x = cut g r x) = (ALL y. (y,x):r --> f(y)=g(y))"
+by (simp add: expand_fun_eq cut_def)
+
+lemma cut_apply: "(x,a):r ==> (cut f r a)(x) = f(x)"
+by (simp add: cut_def)
+
+text{*Inductive characterization of wfrec combinator; for details see:
+John Harrison, "Inductive definitions: automation and application"*}
+
+lemma wfrec_unique: "[| adm_wf R F; wf R |] ==> EX! y. wfrec_rel R F x y"
+apply (simp add: adm_wf_def)
+apply (erule_tac a=x in wf_induct)
+apply (rule ex1I)
+apply (rule_tac g = "%x. THE y. wfrec_rel R F x y" in wfrec_rel.wfrecI)
+apply (fast dest!: theI')
+apply (erule wfrec_rel.cases, simp)
+apply (erule allE, erule allE, erule allE, erule mp)
+apply (fast intro: the_equality [symmetric])
+done
+
+lemma adm_lemma: "adm_wf R (%f x. F (cut f R x) x)"
+apply (simp add: adm_wf_def)
+apply (intro strip)
+apply (rule cuts_eq [THEN iffD2, THEN subst], assumption)
+apply (rule refl)
+done
+
+lemma wfrec: "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a"
+apply (simp add: wfrec_def)
+apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality], assumption)
+apply (rule wfrec_rel.wfrecI)
+apply (intro strip)
+apply (erule adm_lemma [THEN wfrec_unique, THEN theI'])
+done
+
+
 text{** This form avoids giant explosions in proofs.  NOTE USE OF ==*}
 lemma def_wfrec: "[| f==wfrec r H;  wf(r) |] ==> f(a) = H (cut f r a) a"
 apply auto
diff -r 1ad7d4fc0954 -r 8ca2f3500dbc src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Tue Sep 01 14:09:59 2009 +0200
+++ b/src/HOL/Relation.thy	Tue Sep 01 14:10:38 2009 +0200
@@ -599,6 +599,9 @@
   apply blast
   done
 
+lemma in_inv_image[simp]: "((x,y) : inv_image r f) = ((f x, f y) : r)"
+  by (auto simp:inv_image_def)
+
 
 subsection {* Finiteness *}
 
diff -r 1ad7d4fc0954 -r 8ca2f3500dbc src/HOL/Tools/TFL/rules.ML
--- a/src/HOL/Tools/TFL/rules.ML	Tue Sep 01 14:09:59 2009 +0200
+++ b/src/HOL/Tools/TFL/rules.ML	Tue Sep 01 14:10:38 2009 +0200
@@ -456,7 +456,7 @@
 fun is_cong thm =
   case (Thm.prop_of thm)
      of (Const("==>",_)$(Const("Trueprop",_)$ _) $
-         (Const("==",_) $ (Const (@{const_name "Wellfounded.cut"},_) $ f $ R $ a $ x) $ _)) => false
+         (Const("==",_) $ (Const (@{const_name "Recdef.cut"},_) $ f $ R $ a $ x) $ _)) => false
       | _ => true;
 
 
@@ -659,7 +659,7 @@
   end;
 
 fun restricted t = isSome (S.find_term
-                            (fn (Const(@{const_name "Wellfounded.cut"},_)) =>true | _ => false)
+                            (fn (Const(@{const_name "Recdef.cut"},_)) =>true | _ => false)
                             t)
 
 fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =
diff -r 1ad7d4fc0954 -r 8ca2f3500dbc src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Tue Sep 01 14:09:59 2009 +0200
+++ b/src/HOL/Wellfounded.thy	Tue Sep 01 14:10:38 2009 +0200
@@ -13,14 +13,6 @@
 
 subsection {* Basic Definitions *}
 
-inductive
-  wfrec_rel :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b => bool"
-  for R :: "('a * 'a) set"
-  and F :: "('a => 'b) => 'a => 'b"
-where
-  wfrecI: "ALL z. (z, x) : R --> wfrec_rel R F z (g z) ==>
-            wfrec_rel R F x (F g x)"
-
 constdefs
   wf         :: "('a * 'a)set => bool"
   "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))"
@@ -31,16 +23,6 @@
   acyclic :: "('a*'a)set => bool"
   "acyclic r == !x. (x,x) ~: r^+"
 
-  cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b"
-  "cut f r x == (%y. if (y,x):r then f y else undefined)"
-
-  adm_wf :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => bool"
-  "adm_wf R F == ALL f g x.
-     (ALL z. (z, x) : R --> f z = g z) --> F f x = F g x"
-
-  wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b"
-  [code del]: "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
-
 abbreviation acyclicP :: "('a => 'a => bool) => bool" where
   "acyclicP r == acyclic {(x, y). r x y}"
 
@@ -425,54 +407,6 @@
 by (blast intro: finite_acyclic_wf wf_acyclic)
 
 
-subsection{*Well-Founded Recursion*}
-
-text{*cut*}
-
-lemma cuts_eq: "(cut f r x = cut g r x) = (ALL y. (y,x):r --> f(y)=g(y))"
-by (simp add: expand_fun_eq cut_def)
-
-lemma cut_apply: "(x,a):r ==> (cut f r a)(x) = f(x)"
-by (simp add: cut_def)
-
-text{*Inductive characterization of wfrec combinator; for details see:  
-John Harrison, "Inductive definitions: automation and application"*}
-
-lemma wfrec_unique: "[| adm_wf R F; wf R |] ==> EX! y. wfrec_rel R F x y"
-apply (simp add: adm_wf_def)
-apply (erule_tac a=x in wf_induct) 
-apply (rule ex1I)
-apply (rule_tac g = "%x. THE y. wfrec_rel R F x y" in wfrec_rel.wfrecI)
-apply (fast dest!: theI')
-apply (erule wfrec_rel.cases, simp)
-apply (erule allE, erule allE, erule allE, erule mp)
-apply (fast intro: the_equality [symmetric])
-done
-
-lemma adm_lemma: "adm_wf R (%f x. F (cut f R x) x)"
-apply (simp add: adm_wf_def)
-apply (intro strip)
-apply (rule cuts_eq [THEN iffD2, THEN subst], assumption)
-apply (rule refl)
-done
-
-lemma wfrec: "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a"
-apply (simp add: wfrec_def)
-apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality], assumption)
-apply (rule wfrec_rel.wfrecI)
-apply (intro strip)
-apply (erule adm_lemma [THEN wfrec_unique, THEN theI'])
-done
-
-subsection {* Code generator setup *}
-
-consts_code
-  "wfrec"   ("\<module>wfrec?")
-attach {*
-fun wfrec f x = f (wfrec f) x;
-*}
-
-
 subsection {* @{typ nat} is well-founded *}
 
 lemma less_nat_rel: "op < = (\<lambda>m n. n = Suc m)^++"
@@ -696,9 +630,6 @@
 apply blast
 done
 
-lemma in_inv_image[simp]: "((x,y) : inv_image r f) = ((f x, f y) : r)"
-  by (auto simp:inv_image_def)
-
 text {* Measure Datatypes into @{typ nat} *}
 
 definition measure :: "('a => nat) => ('a * 'a)set"
diff -r 1ad7d4fc0954 -r 8ca2f3500dbc src/Pure/General/linear_set.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/linear_set.scala	Tue Sep 01 14:10:38 2009 +0200
@@ -0,0 +1,118 @@
+/*  Title:      Pure/General/linear_set.scala
+    Author:     Makarius
+    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())
+
+  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) }
+
+
+  def empty[A]: Linear_Set[A] = new Linear_Set
+  def apply[A](elems: A*): Linear_Set[A] = empty[A] ++ elems
+
+  class Duplicate(s: String) extends Exception(s)
+  class Undefined(s: String) extends Exception(s)
+}
+
+
+class Linear_Set[A] extends scala.collection.immutable.Set[A]
+{
+  /* representation */
+
+  protected val rep = Linear_Set.empty_rep[A]
+
+
+  /* auxiliary operations */
+
+  def next(elem: A) = rep.body.get(elem)
+  def prev(elem: A) = rep.body.find(_._2 == elem).map(_._1)   // slow
+
+  private 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))
+      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))
+    }
+
+  def insert_after(hook: Option[A], elems: Seq[A]): Linear_Set[A] =
+    elems.reverse.foldLeft (this) ((ls, elem) => 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
+    else {
+      val next =
+        if (from == rep.last_elem) None
+        else if (from == None) rep.first_elem
+        else from.map(rep.body(_))
+      if (next == to) this
+      else delete_after(from).delete_between(from, to)
+    }
+  }
+
+
+  /* Set methods */
+
+  override def stringPrefix = "Linear_Set"
+
+  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
+
+  def elements = new Iterator[A] {
+    private var next_elem = rep.first_elem
+    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
+      elem
+    }
+  }
+
+  def contains(elem: A): Boolean =
+    !isEmpty && (rep.last_elem.get == elem || rep.body.isDefinedAt(elem))
+
+  def + (elem: A): Linear_Set[A] = _insert_after(rep.last_elem, elem)
+
+  override def + (elem1: A, elem2: A, elems: A*): Linear_Set[A] =
+    this + elem1 + elem2 ++ elems
+  override def ++ (elems: Iterable[A]): Linear_Set[A] = (this /: elems) ((s, elem) => s + elem)
+  override def ++ (elems: Iterator[A]): Linear_Set[A] = (this /: elems) ((s, elem) => s + elem)
+
+  def - (elem: A): Linear_Set[A] =
+    if (!contains(elem)) throw new Linear_Set.Undefined(elem.toString)
+    else delete_after(prev(elem))
+}
\ No newline at end of file
diff -r 1ad7d4fc0954 -r 8ca2f3500dbc src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Tue Sep 01 14:09:59 2009 +0200
+++ b/src/Pure/IsaMakefile	Tue Sep 01 14:10:38 2009 +0200
@@ -117,14 +117,14 @@
 
 ## Scala material
 
-SCALA_FILES = General/event_bus.scala General/markup.scala		\
-  General/position.scala General/scan.scala General/swing_thread.scala	\
-  General/symbol.scala General/xml.scala General/yxml.scala		\
-  Isar/isar.scala Isar/isar_document.scala Isar/outer_keyword.scala	\
-  System/cygwin.scala System/gui_setup.scala				\
+SCALA_FILES = General/event_bus.scala General/linear_set.scala		\
+  General/markup.scala General/position.scala General/scan.scala	\
+  General/swing_thread.scala General/symbol.scala General/xml.scala	\
+  General/yxml.scala Isar/isar.scala Isar/isar_document.scala		\
+  Isar/outer_keyword.scala System/cygwin.scala System/gui_setup.scala	\
   System/isabelle_process.scala System/isabelle_syntax.scala		\
   System/isabelle_system.scala System/platform.scala			\
-  Thy/completion.scala Thy/thy_header.scala \
+  Thy/completion.scala Thy/thy_header.scala
 
 JAR_DIR = $(ISABELLE_HOME)/lib/classes
 PURE_JAR = $(JAR_DIR)/Pure.jar