586 thus ?thesis |
586 thus ?thesis |
587 unfolding Seq_def |
587 unfolding Seq_def |
588 by (simp add: adjunct_sup sup_assoc sup_commute sup_left_commute) |
588 by (simp add: adjunct_sup sup_assoc sup_commute sup_left_commute) |
589 qed |
589 qed |
590 |
590 |
591 declare eq_pred_def [code, code del] |
591 primrec contained :: "'a seq \<Rightarrow> 'a pred \<Rightarrow> bool" where |
|
592 "contained Empty Q \<longleftrightarrow> True" |
|
593 | "contained (Insert x P) Q \<longleftrightarrow> eval Q x \<and> P \<le> Q" |
|
594 | "contained (Join P xq) Q \<longleftrightarrow> P \<le> Q \<and> contained xq Q" |
|
595 |
|
596 lemma single_less_eq_eval: |
|
597 "single x \<le> P \<longleftrightarrow> eval P x" |
|
598 by (auto simp add: single_def less_eq_pred_def mem_def) |
|
599 |
|
600 lemma contained_less_eq: |
|
601 "contained xq Q \<longleftrightarrow> pred_of_seq xq \<le> Q" |
|
602 by (induct xq) (simp_all add: single_less_eq_eval) |
|
603 |
|
604 lemma less_eq_pred_code [code]: |
|
605 "Seq f \<le> Q = (case f () |
|
606 of Empty \<Rightarrow> True |
|
607 | Insert x P \<Rightarrow> eval Q x \<and> P \<le> Q |
|
608 | Join P xq \<Rightarrow> P \<le> Q \<and> contained xq Q)" |
|
609 by (cases "f ()") |
|
610 (simp_all add: Seq_def single_less_eq_eval contained_less_eq) |
|
611 |
|
612 lemma eq_pred_code [code]: |
|
613 fixes P Q :: "'a::eq pred" |
|
614 shows "eq_class.eq P Q \<longleftrightarrow> P \<le> Q \<and> Q \<le> P" |
|
615 unfolding eq by auto |
|
616 |
|
617 lemma [code]: |
|
618 "pred_case f P = f (eval P)" |
|
619 by (cases P) simp |
|
620 |
|
621 lemma [code]: |
|
622 "pred_rec f P = f (eval P)" |
|
623 by (cases P) simp |
592 |
624 |
593 no_notation |
625 no_notation |
594 inf (infixl "\<sqinter>" 70) and |
626 inf (infixl "\<sqinter>" 70) and |
595 sup (infixl "\<squnion>" 65) and |
627 sup (infixl "\<squnion>" 65) and |
596 Inf ("\<Sqinter>_" [900] 900) and |
628 Inf ("\<Sqinter>_" [900] 900) and |
599 bot ("\<bottom>") and |
631 bot ("\<bottom>") and |
600 bind (infixl "\<guillemotright>=" 70) |
632 bind (infixl "\<guillemotright>=" 70) |
601 |
633 |
602 hide (open) type pred seq |
634 hide (open) type pred seq |
603 hide (open) const Pred eval single bind if_pred not_pred |
635 hide (open) const Pred eval single bind if_pred not_pred |
604 Empty Insert Join Seq member "apply" adjunct |
636 Empty Insert Join Seq member pred_of_seq "apply" adjunct |
605 |
637 |
606 end |
638 end |