src/HOL/Product_Type.thy
changeset 28719 01e04e41cc7b
parent 28562 4e74209f113e
child 30604 2a9911f4b0a3
equal deleted inserted replaced
28718:ef16499edaab 28719:01e04e41cc7b
   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