487 end

   487 end

   488 

   488 

   489 

   489 

   490 subsection {* Permutations for products *}

   490 subsection {* Permutations for products *}

   491 

   491 

   493 begin

   493 begin

   494 

   494 

   495 primrec 

   495 primrec 

   496   permute_prod 

   496   permute_prod 

   497 where

   497 where

   502 

   502 

   503 end

   503 end

   504 

   504 

   505 subsection {* Permutations for sums *}

   505 subsection {* Permutations for sums *}

   506 

   506 

   508 begin

   508 begin

   509 

   509 

   510 primrec 

   510 primrec 

   511   permute_sum 

   511   permute_sum 

   512 where

   512 where

   601 text {* Other type constructors preserve purity. *}

   601 text {* Other type constructors preserve purity. *}

   602 

   602 

   603 instance "fun" :: (pure, pure) pure

   603 instance "fun" :: (pure, pure) pure

   604 by default (simp add: permute_fun_def permute_pure)

   604 by default (simp add: permute_fun_def permute_pure)

   605 

   605 

   607 by default (induct_tac x, simp add: permute_pure)

   607 by default (induct_tac x, simp add: permute_pure)

   608 

   608 

   610 by default (induct_tac x, simp_all add: permute_pure)

   610 by default (induct_tac x, simp_all add: permute_pure)

   611 

   611 

   612 instance list :: (pure) pure

   612 instance list :: (pure) pure

   613 by default (induct_tac x, simp_all add: permute_pure)

   613 by default (induct_tac x, simp_all add: permute_pure)

   614 

   614 

   985 

   985 

   986 lemma fresh_Pair: 

   986 lemma fresh_Pair: 

   987   shows "a \<sharp> (x, y) \<longleftrightarrow> a \<sharp> x \<and> a \<sharp> y"

   987   shows "a \<sharp> (x, y) \<longleftrightarrow> a \<sharp> x \<and> a \<sharp> y"

   988   by (simp add: fresh_def supp_Pair)

   988   by (simp add: fresh_def supp_Pair)

   989 

   989 

   991 apply default

   991 apply default

   992 apply (induct_tac x)

   992 apply (induct_tac x)

   993 apply (simp add: supp_Pair finite_supp)

   993 apply (simp add: supp_Pair finite_supp)

   994 done

   994 done

   995 

   995 

  1009 

  1009 

  1010 lemma fresh_Inr: 

  1010 lemma fresh_Inr: 

  1011   shows "a \<sharp> Inr y \<longleftrightarrow> a \<sharp> y"

  1011   shows "a \<sharp> Inr y \<longleftrightarrow> a \<sharp> y"

  1012   by (simp add: fresh_def supp_Inr)

  1012   by (simp add: fresh_def supp_Inr)

  1013 

  1013 

  1015 apply default

  1015 apply default

  1016 apply (induct_tac x)

  1016 apply (induct_tac x)

  1017 apply (simp_all add: supp_Inl supp_Inr finite_supp)

  1017 apply (simp_all add: supp_Inl supp_Inr finite_supp)

  1018 done

  1018 done

  1019 

  1019