equal
deleted
inserted
replaced
620 |
620 |
621 lemma [code]: |
621 lemma [code]: |
622 "pred_rec f P = f (eval P)" |
622 "pred_rec f P = f (eval P)" |
623 by (cases P) simp |
623 by (cases P) simp |
624 |
624 |
|
625 inductive eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where "eq x x" |
|
626 |
|
627 lemma eq_is_eq: "eq x y \<equiv> (x = y)" |
|
628 by (rule eq_reflection) (auto intro: eq.intros elim: eq.cases) |
|
629 |
625 no_notation |
630 no_notation |
626 inf (infixl "\<sqinter>" 70) and |
631 inf (infixl "\<sqinter>" 70) and |
627 sup (infixl "\<squnion>" 65) and |
632 sup (infixl "\<squnion>" 65) and |
628 Inf ("\<Sqinter>_" [900] 900) and |
633 Inf ("\<Sqinter>_" [900] 900) and |
629 Sup ("\<Squnion>_" [900] 900) and |
634 Sup ("\<Squnion>_" [900] 900) and |
631 bot ("\<bottom>") and |
636 bot ("\<bottom>") and |
632 bind (infixl "\<guillemotright>=" 70) |
637 bind (infixl "\<guillemotright>=" 70) |
633 |
638 |
634 hide (open) type pred seq |
639 hide (open) type pred seq |
635 hide (open) const Pred eval single bind if_pred not_pred |
640 hide (open) const Pred eval single bind if_pred not_pred |
636 Empty Insert Join Seq member pred_of_seq "apply" adjunct |
641 Empty Insert Join Seq member pred_of_seq "apply" adjunct eq |
637 |
642 |
638 end |
643 end |