698 |
698 |
699 end |
699 end |
700 |
700 |
701 instance "fun" :: (type, boolean_algebra) boolean_algebra proof |
701 instance "fun" :: (type, boolean_algebra) boolean_algebra proof |
702 qed (rule ext, simp_all add: inf_apply sup_apply bot_apply top_apply uminus_apply minus_apply inf_compl_bot sup_compl_top diff_eq)+ |
702 qed (rule ext, simp_all add: inf_apply sup_apply bot_apply top_apply uminus_apply minus_apply inf_compl_bot sup_compl_top diff_eq)+ |
|
703 |
|
704 |
|
705 subsection {* Lattice on unary and binary predicates *} |
|
706 |
|
707 lemma inf1I: "A x \<Longrightarrow> B x \<Longrightarrow> (A \<sqinter> B) x" |
|
708 by (simp add: inf_fun_def) |
|
709 |
|
710 lemma inf2I: "A x y \<Longrightarrow> B x y \<Longrightarrow> (A \<sqinter> B) x y" |
|
711 by (simp add: inf_fun_def) |
|
712 |
|
713 lemma inf1E: "(A \<sqinter> B) x \<Longrightarrow> (A x \<Longrightarrow> B x \<Longrightarrow> P) \<Longrightarrow> P" |
|
714 by (simp add: inf_fun_def) |
|
715 |
|
716 lemma inf2E: "(A \<sqinter> B) x y \<Longrightarrow> (A x y \<Longrightarrow> B x y \<Longrightarrow> P) \<Longrightarrow> P" |
|
717 by (simp add: inf_fun_def) |
|
718 |
|
719 lemma inf1D1: "(A \<sqinter> B) x \<Longrightarrow> A x" |
|
720 by (simp add: inf_fun_def) |
|
721 |
|
722 lemma inf2D1: "(A \<sqinter> B) x y \<Longrightarrow> A x y" |
|
723 by (simp add: inf_fun_def) |
|
724 |
|
725 lemma inf1D2: "(A \<sqinter> B) x \<Longrightarrow> B x" |
|
726 by (simp add: inf_fun_def) |
|
727 |
|
728 lemma inf2D2: "(A \<sqinter> B) x y \<Longrightarrow> B x y" |
|
729 by (simp add: inf_fun_def) |
|
730 |
|
731 lemma sup1I1: "A x \<Longrightarrow> (A \<squnion> B) x" |
|
732 by (simp add: sup_fun_def) |
|
733 |
|
734 lemma sup2I1: "A x y \<Longrightarrow> (A \<squnion> B) x y" |
|
735 by (simp add: sup_fun_def) |
|
736 |
|
737 lemma sup1I2: "B x \<Longrightarrow> (A \<squnion> B) x" |
|
738 by (simp add: sup_fun_def) |
|
739 |
|
740 lemma sup2I2: "B x y \<Longrightarrow> (A \<squnion> B) x y" |
|
741 by (simp add: sup_fun_def) |
|
742 |
|
743 lemma sup1E: "(A \<squnion> B) x \<Longrightarrow> (A x \<Longrightarrow> P) \<Longrightarrow> (B x \<Longrightarrow> P) \<Longrightarrow> P" |
|
744 by (simp add: sup_fun_def) iprover |
|
745 |
|
746 lemma sup2E: "(A \<squnion> B) x y \<Longrightarrow> (A x y \<Longrightarrow> P) \<Longrightarrow> (B x y \<Longrightarrow> P) \<Longrightarrow> P" |
|
747 by (simp add: sup_fun_def) iprover |
|
748 |
|
749 text {* |
|
750 \medskip Classical introduction rule: no commitment to @{text A} vs |
|
751 @{text B}. |
|
752 *} |
|
753 |
|
754 lemma sup1CI: "(\<not> B x \<Longrightarrow> A x) \<Longrightarrow> (A \<squnion> B) x" |
|
755 by (auto simp add: sup_fun_def) |
|
756 |
|
757 lemma sup2CI: "(\<not> B x y \<Longrightarrow> A x y) \<Longrightarrow> (A \<squnion> B) x y" |
|
758 by (auto simp add: sup_fun_def) |
|
759 |
703 |
760 |
704 no_notation |
761 no_notation |
705 less_eq (infix "\<sqsubseteq>" 50) and |
762 less_eq (infix "\<sqsubseteq>" 50) and |
706 less (infix "\<sqsubset>" 50) and |
763 less (infix "\<sqsubset>" 50) and |
707 inf (infixl "\<sqinter>" 70) and |
764 inf (infixl "\<sqinter>" 70) and |
708 sup (infixl "\<squnion>" 65) and |
765 sup (infixl "\<squnion>" 65) and |
709 top ("\<top>") and |
766 top ("\<top>") and |
710 bot ("\<bottom>") |
767 bot ("\<bottom>") |
711 |
768 |
712 end |
769 end |
|
770 |