equal
deleted
inserted
replaced
902 Non-dependent versions are needed to avoid the need for higher-order |
902 Non-dependent versions are needed to avoid the need for higher-order |
903 matching, especially when the rules are re-oriented. |
903 matching, especially when the rules are re-oriented. |
904 *} |
904 *} |
905 |
905 |
906 lemma Times_Un_distrib1: "(A Un B) <*> C = (A <*> C) Un (B <*> C)" |
906 lemma Times_Un_distrib1: "(A Un B) <*> C = (A <*> C) Un (B <*> C)" |
907 by blast |
907 by blast |
908 |
908 |
909 lemma Times_Int_distrib1: "(A Int B) <*> C = (A <*> C) Int (B <*> C)" |
909 lemma Times_Int_distrib1: "(A Int B) <*> C = (A <*> C) Int (B <*> C)" |
910 by blast |
910 by blast |
911 |
911 |
912 lemma Times_Diff_distrib1: "(A - B) <*> C = (A <*> C) - (B <*> C)" |
912 lemma Times_Diff_distrib1: "(A - B) <*> C = (A <*> C) - (B <*> C)" |
913 by blast |
913 by blast |
914 |
914 |
|
915 lemma insert_times_insert[simp]: |
|
916 "insert a A \<times> insert b B = |
|
917 insert (a,b) (A \<times> insert b B \<union> insert a A \<times> B)" |
|
918 by blast |
915 |
919 |
916 subsubsection {* Code generator setup *} |
920 subsubsection {* Code generator setup *} |
917 |
921 |
918 instance * :: (eq, eq) eq .. |
922 instance * :: (eq, eq) eq .. |
919 |
923 |