refined enumeration implementation
authorhaftmann
Sun Mar 08 15:25:29 2009 +0100 (2009-03-08)
changeset 30376e8cc806a3755
parent 30375 ad2a9dc516ed
child 30377 26a05c2fd577
refined enumeration implementation
src/HOL/Predicate.thy
     1.1 --- a/src/HOL/Predicate.thy	Sun Mar 08 15:25:29 2009 +0100
     1.2 +++ b/src/HOL/Predicate.thy	Sun Mar 08 15:25:29 2009 +0100
     1.3 @@ -568,15 +568,24 @@
     1.4    "\<bottom> = Seq (\<lambda>u. Empty)"
     1.5    unfolding Seq_def by simp
     1.6  
     1.7 +primrec adjunct :: "'a pred \<Rightarrow> 'a seq \<Rightarrow> 'a seq" where
     1.8 +    "adjunct P Empty = Join P Empty"
     1.9 +  | "adjunct P (Insert x Q) = Insert x (Q \<squnion> P)"
    1.10 +  | "adjunct P (Join Q xq) = Join Q (adjunct P xq)"
    1.11 +
    1.12 +lemma adjunct_sup:
    1.13 +  "pred_of_seq (adjunct P xq) = P \<squnion> pred_of_seq xq"
    1.14 +  by (induct xq) (simp_all add: sup_assoc sup_commute sup_left_commute)
    1.15 +
    1.16  lemma sup_code [code]:
    1.17    "Seq f \<squnion> Seq g = Seq (\<lambda>u. case f ()
    1.18      of Empty \<Rightarrow> g ()
    1.19       | Insert x P \<Rightarrow> Insert x (P \<squnion> Seq g)
    1.20 -     | Join P xq \<Rightarrow> Join (Seq g) (Join P xq))" (*FIXME order!?*)
    1.21 +     | Join P xq \<Rightarrow> adjunct (Seq g) (Join P xq))"
    1.22  proof (cases "f ()")
    1.23    case Empty
    1.24    thus ?thesis
    1.25 -    unfolding Seq_def by (simp add: sup_commute [of "\<bottom>"] sup_bot)
    1.26 +    unfolding Seq_def by (simp add: sup_commute [of "\<bottom>"]  sup_bot)
    1.27  next
    1.28    case Insert
    1.29    thus ?thesis
    1.30 @@ -584,10 +593,10 @@
    1.31  next
    1.32    case Join
    1.33    thus ?thesis
    1.34 -    unfolding Seq_def by (simp add: sup_commute [of "pred_of_seq (g ())"] sup_assoc)
    1.35 +    unfolding Seq_def
    1.36 +    by (simp add: adjunct_sup sup_assoc sup_commute sup_left_commute)
    1.37  qed
    1.38  
    1.39 -
    1.40  declare eq_pred_def [code, code del]
    1.41  
    1.42  no_notation
    1.43 @@ -601,6 +610,6 @@
    1.44  
    1.45  hide (open) type pred seq
    1.46  hide (open) const Pred eval single bind if_pred eq_pred not_pred
    1.47 -  Empty Insert Join Seq member "apply"
    1.48 +  Empty Insert Join Seq member "apply" adjunct
    1.49  
    1.50  end