equal
deleted
inserted
replaced
8 |
8 |
9 subsection "Abstract State with Computable Ordering" |
9 subsection "Abstract State with Computable Ordering" |
10 |
10 |
11 text{* A concrete type of state with computable @{text"\<sqsubseteq>"}: *} |
11 text{* A concrete type of state with computable @{text"\<sqsubseteq>"}: *} |
12 |
12 |
13 datatype 'a astate = FunDom "string \<Rightarrow> 'a" "string list" |
13 datatype_new 'a astate = FunDom "string \<Rightarrow> 'a" "string list" |
14 |
14 |
15 fun "fun" where "fun (FunDom f _) = f" |
15 fun "fun" where "fun (FunDom f _) = f" |
16 fun dom where "dom (FunDom _ A) = A" |
16 fun dom where "dom (FunDom _ A) = A" |
17 |
17 |
18 definition [simp]: "inter_list xs ys = [x\<leftarrow>xs. x \<in> set ys]" |
18 definition [simp]: "inter_list xs ys = [x\<leftarrow>xs. x \<in> set ys]" |