832 sorted_spmat.simps |
832 sorted_spmat.simps |
833 sorted_sparse_matrix_def |
833 sorted_sparse_matrix_def |
834 |
834 |
835 lemma bool1: "(\<not> True) = False" by blast |
835 lemma bool1: "(\<not> True) = False" by blast |
836 lemma bool2: "(\<not> False) = True" by blast |
836 lemma bool2: "(\<not> False) = True" by blast |
837 lemma bool3: "((P\<Colon>bool) \<and> True) = P" by blast |
837 lemma bool3: "((P::bool) \<and> True) = P" by blast |
838 lemma bool4: "(True \<and> (P\<Colon>bool)) = P" by blast |
838 lemma bool4: "(True \<and> (P::bool)) = P" by blast |
839 lemma bool5: "((P\<Colon>bool) \<and> False) = False" by blast |
839 lemma bool5: "((P::bool) \<and> False) = False" by blast |
840 lemma bool6: "(False \<and> (P\<Colon>bool)) = False" by blast |
840 lemma bool6: "(False \<and> (P::bool)) = False" by blast |
841 lemma bool7: "((P\<Colon>bool) \<or> True) = True" by blast |
841 lemma bool7: "((P::bool) \<or> True) = True" by blast |
842 lemma bool8: "(True \<or> (P\<Colon>bool)) = True" by blast |
842 lemma bool8: "(True \<or> (P::bool)) = True" by blast |
843 lemma bool9: "((P\<Colon>bool) \<or> False) = P" by blast |
843 lemma bool9: "((P::bool) \<or> False) = P" by blast |
844 lemma bool10: "(False \<or> (P\<Colon>bool)) = P" by blast |
844 lemma bool10: "(False \<or> (P::bool)) = P" by blast |
845 lemmas boolarith = bool1 bool2 bool3 bool4 bool5 bool6 bool7 bool8 bool9 bool10 |
845 lemmas boolarith = bool1 bool2 bool3 bool4 bool5 bool6 bool7 bool8 bool9 bool10 |
846 |
846 |
847 lemma if_case_eq: "(if b then x else y) = (case b of True => x | False => y)" by simp |
847 lemma if_case_eq: "(if b then x else y) = (case b of True => x | False => y)" by simp |
848 |
848 |
849 primrec pprt_spvec :: "('a::{lattice_ab_group_add}) spvec \<Rightarrow> 'a spvec" |
849 primrec pprt_spvec :: "('a::{lattice_ab_group_add}) spvec \<Rightarrow> 'a spvec" |