equal
deleted
inserted
replaced
648 begin |
648 begin |
649 |
649 |
650 definition |
650 definition |
651 "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)" |
651 "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)" |
652 |
652 |
653 lemma inf_apply (* CANDIDATE [simp, code] *): |
653 lemma inf_apply [simp] (* CANDIDATE [code] *): |
654 "(f \<sqinter> g) x = f x \<sqinter> g x" |
654 "(f \<sqinter> g) x = f x \<sqinter> g x" |
655 by (simp add: inf_fun_def) |
655 by (simp add: inf_fun_def) |
656 |
656 |
657 definition |
657 definition |
658 "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)" |
658 "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)" |
659 |
659 |
660 lemma sup_apply (* CANDIDATE [simp, code] *): |
660 lemma sup_apply [simp] (* CANDIDATE [code] *): |
661 "(f \<squnion> g) x = f x \<squnion> g x" |
661 "(f \<squnion> g) x = f x \<squnion> g x" |
662 by (simp add: sup_fun_def) |
662 by (simp add: sup_fun_def) |
663 |
663 |
664 instance proof |
664 instance proof |
665 qed (simp_all add: le_fun_def inf_apply sup_apply) |
665 qed (simp_all add: le_fun_def inf_apply sup_apply) |
675 begin |
675 begin |
676 |
676 |
677 definition |
677 definition |
678 fun_Compl_def: "- A = (\<lambda>x. - A x)" |
678 fun_Compl_def: "- A = (\<lambda>x. - A x)" |
679 |
679 |
680 lemma uminus_apply (* CANDIDATE [simp, code] *): |
680 lemma uminus_apply [simp] (* CANDIDATE [code] *): |
681 "(- A) x = - (A x)" |
681 "(- A) x = - (A x)" |
682 by (simp add: fun_Compl_def) |
682 by (simp add: fun_Compl_def) |
683 |
683 |
684 instance .. |
684 instance .. |
685 |
685 |
689 begin |
689 begin |
690 |
690 |
691 definition |
691 definition |
692 fun_diff_def: "A - B = (\<lambda>x. A x - B x)" |
692 fun_diff_def: "A - B = (\<lambda>x. A x - B x)" |
693 |
693 |
694 lemma minus_apply (* CANDIDATE [simp, code] *): |
694 lemma minus_apply [simp] (* CANDIDATE [code] *): |
695 "(A - B) x = A x - B x" |
695 "(A - B) x = A x - B x" |
696 by (simp add: fun_diff_def) |
696 by (simp add: fun_diff_def) |
697 |
697 |
698 instance .. |
698 instance .. |
699 |
699 |