src/HOL/IMP/Astate.thy

--- a/src/HOL/IMP/Astate.thy	Wed Sep 14 06:49:24 2011 +0200
+++ b/src/HOL/IMP/Astate.thy	Thu Sep 15 09:44:08 2011 +0200
@@ -2,6 +2,8 @@
 
 theory Astate
 imports AbsInt0_fun
+  "~~/src/HOL/Library/Char_ord" "~~/src/HOL/Library/List_lexord"
+  (* Library import merely to allow string lists to be sorted for output *)
 begin
 
 subsection "Abstract State with Computable Ordering"
@@ -13,12 +15,14 @@
 fun "fun" where "fun (FunDom f _) = f"
 fun dom where "dom (FunDom _ A) = A"
 
-definition "list S = [(x,fun S x). x \<leftarrow> dom S]"
+definition [simp]: "inter_list xs ys = [x\<leftarrow>xs. x \<in> set ys]"
+
+definition "list S = [(x,fun S x). x \<leftarrow> sort(dom S)]"
 
 definition "lookup F x = (if x : set(dom F) then fun F x else Top)"
 
 definition "update F x y =
-  FunDom ((fun F)(x:=y)) (if x : set(dom F) then dom F else x # dom F)"
+  FunDom ((fun F)(x:=y)) (if x \<in> set(dom F) then dom F else x # dom F)"
 
 lemma lookup_update: "lookup (update S x y) = (lookup S)(x:=y)"
 by(rule ext)(auto simp: lookup_def update_def)
@@ -30,7 +34,7 @@
 
 definition
 "join_astate F G =
- FunDom (\<lambda>x. fun F x \<squnion> fun G x) ([x\<leftarrow>dom F. x : set(dom G)])"
+ FunDom (\<lambda>x. fun F x \<squnion> fun G x) (inter_list (dom F) (dom G))"
 
 definition "Top = FunDom (\<lambda>x. Top) []"