# HG changeset patch
# User haftmann
# Date 1236522329 -3600
# Node ID e8cc806a3755dcb63f23cfe125407b1ceb3e45c1
# Parent  ad2a9dc516ed61287f1b026fcb30efa3bce315ba
refined enumeration implementation

diff -r ad2a9dc516ed -r e8cc806a3755 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Sun Mar 08 15:25:29 2009 +0100
+++ b/src/HOL/Predicate.thy	Sun Mar 08 15:25:29 2009 +0100
@@ -568,15 +568,24 @@
   "\<bottom> = Seq (\<lambda>u. Empty)"
   unfolding Seq_def by simp
 
+primrec adjunct :: "'a pred \<Rightarrow> 'a seq \<Rightarrow> 'a seq" where
+    "adjunct P Empty = Join P Empty"
+  | "adjunct P (Insert x Q) = Insert x (Q \<squnion> P)"
+  | "adjunct P (Join Q xq) = Join Q (adjunct P xq)"
+
+lemma adjunct_sup:
+  "pred_of_seq (adjunct P xq) = P \<squnion> pred_of_seq xq"
+  by (induct xq) (simp_all add: sup_assoc sup_commute sup_left_commute)
+
 lemma sup_code [code]:
   "Seq f \<squnion> Seq g = Seq (\<lambda>u. case f ()
     of Empty \<Rightarrow> g ()
      | Insert x P \<Rightarrow> Insert x (P \<squnion> Seq g)
-     | Join P xq \<Rightarrow> Join (Seq g) (Join P xq))" (*FIXME order!?*)
+     | Join P xq \<Rightarrow> adjunct (Seq g) (Join P xq))"
 proof (cases "f ()")
   case Empty
   thus ?thesis
-    unfolding Seq_def by (simp add: sup_commute [of "\<bottom>"] sup_bot)
+    unfolding Seq_def by (simp add: sup_commute [of "\<bottom>"]  sup_bot)
 next
   case Insert
   thus ?thesis
@@ -584,10 +593,10 @@
 next
   case Join
   thus ?thesis
-    unfolding Seq_def by (simp add: sup_commute [of "pred_of_seq (g ())"] sup_assoc)
+    unfolding Seq_def
+    by (simp add: adjunct_sup sup_assoc sup_commute sup_left_commute)
 qed
 
-
 declare eq_pred_def [code, code del]
 
 no_notation
@@ -601,6 +610,6 @@
 
 hide (open) type pred seq
 hide (open) const Pred eval single bind if_pred eq_pred not_pred
-  Empty Insert Join Seq member "apply"
+  Empty Insert Join Seq member "apply" adjunct
 
 end