408 by (cases x) simp |
408 by (cases x) simp |
409 |
409 |
410 lemma pred_eqI: |
410 lemma pred_eqI: |
411 "(\<And>w. eval P w \<longleftrightarrow> eval Q w) \<Longrightarrow> P = Q" |
411 "(\<And>w. eval P w \<longleftrightarrow> eval Q w) \<Longrightarrow> P = Q" |
412 by (cases P, cases Q) (auto simp add: fun_eq_iff) |
412 by (cases P, cases Q) (auto simp add: fun_eq_iff) |
|
413 |
|
414 lemma pred_eq_iff: |
|
415 "P = Q \<Longrightarrow> (\<And>w. eval P w \<longleftrightarrow> eval Q w)" |
|
416 by (simp add: pred_eqI) |
413 |
417 |
414 instantiation pred :: (type) complete_lattice |
418 instantiation pred :: (type) complete_lattice |
415 begin |
419 begin |
416 |
420 |
417 definition |
421 definition |
814 next |
818 next |
815 case Join then show ?case |
819 case Join then show ?case |
816 by (auto simp add: fun_eq_iff elim: supE intro: supI1 supI2) |
820 by (auto simp add: fun_eq_iff elim: supE intro: supI1 supI2) |
817 qed |
821 qed |
818 |
822 |
819 lemma eval_code [code]: "eval (Seq f) = member (f ())" |
823 lemma eval_code [(* FIXME declare simp *)code]: "eval (Seq f) = member (f ())" |
820 unfolding Seq_def by (rule sym, rule eval_member) |
824 unfolding Seq_def by (rule sym, rule eval_member) |
821 |
825 |
822 lemma single_code [code]: |
826 lemma single_code [code]: |
823 "single x = Seq (\<lambda>u. Insert x \<bottom>)" |
827 "single x = Seq (\<lambda>u. Insert x \<bottom>)" |
824 unfolding Seq_def by simp |
828 unfolding Seq_def by simp |
1015 fun yieldn P = anamorph yield P; |
1019 fun yieldn P = anamorph yield P; |
1016 |
1020 |
1017 end; |
1021 end; |
1018 *} |
1022 *} |
1019 |
1023 |
|
1024 text {* Conversion from and to sets *} |
|
1025 |
|
1026 definition pred_of_set :: "'a set \<Rightarrow> 'a pred" where |
|
1027 "pred_of_set = Pred \<circ> (\<lambda>A x. x \<in> A)" |
|
1028 |
|
1029 lemma eval_pred_of_set [simp]: |
|
1030 "eval (pred_of_set A) x \<longleftrightarrow> x \<in>A" |
|
1031 by (simp add: pred_of_set_def) |
|
1032 |
|
1033 definition set_of_pred :: "'a pred \<Rightarrow> 'a set" where |
|
1034 "set_of_pred = Collect \<circ> eval" |
|
1035 |
|
1036 lemma member_set_of_pred [simp]: |
|
1037 "x \<in> set_of_pred P \<longleftrightarrow> Predicate.eval P x" |
|
1038 by (simp add: set_of_pred_def) |
|
1039 |
|
1040 definition set_of_seq :: "'a seq \<Rightarrow> 'a set" where |
|
1041 "set_of_seq = set_of_pred \<circ> pred_of_seq" |
|
1042 |
|
1043 lemma member_set_of_seq [simp]: |
|
1044 "x \<in> set_of_seq xq = Predicate.member xq x" |
|
1045 by (simp add: set_of_seq_def eval_member) |
|
1046 |
|
1047 lemma of_pred_code [code]: |
|
1048 "set_of_pred (Predicate.Seq f) = (case f () of |
|
1049 Predicate.Empty \<Rightarrow> {} |
|
1050 | Predicate.Insert x P \<Rightarrow> insert x (set_of_pred P) |
|
1051 | Predicate.Join P xq \<Rightarrow> set_of_pred P \<union> set_of_seq xq)" |
|
1052 by (auto split: seq.split simp add: eval_code) |
|
1053 |
|
1054 lemma of_seq_code [code]: |
|
1055 "set_of_seq Predicate.Empty = {}" |
|
1056 "set_of_seq (Predicate.Insert x P) = insert x (set_of_pred P)" |
|
1057 "set_of_seq (Predicate.Join P xq) = set_of_pred P \<union> set_of_seq xq" |
|
1058 by auto |
|
1059 |
1020 no_notation |
1060 no_notation |
1021 bot ("\<bottom>") and |
1061 bot ("\<bottom>") and |
1022 top ("\<top>") and |
1062 top ("\<top>") and |
1023 inf (infixl "\<sqinter>" 70) and |
1063 inf (infixl "\<sqinter>" 70) and |
1024 sup (infixl "\<squnion>" 65) and |
1064 sup (infixl "\<squnion>" 65) and |