884   apply (simp_all add: pure_fresh fresh_star_def eqvt_at_def)

   884   apply (simp_all add: pure_fresh fresh_star_def eqvt_at_def)

   885   done

   885   done

   886 

   886 

   887 text {* tests of functions containing if and case *}

   887 text {* tests of functions containing if and case *}

   888 

   888 

   890 

   890 

   891 nominal_primrec  

   891 nominal_primrec  

   892   A :: "lam => lam"

   892   A :: "lam => lam"

   893 where  

   893 where  

   894   "A (App M N) = (if (True \<or> P M) then (A M) else (A N))"

   894   "A (App M N) = (if (True \<or> P M) then (A M) else (A N))"

   921 unfolding eqvt_def

   921 unfolding eqvt_def

   922 unfolding B_graph_def

   922 unfolding B_graph_def

   923 apply(perm_simp)

   923 apply(perm_simp)

   924 apply(rule allI)

   924 apply(rule allI)

   925 apply(rule refl)

   925 apply(rule refl)

   927 

   927 

   928 end

   928 end

   929 

   929 

   930 

   930 

   931 

   931