885   apply (simp_all add: pure_fresh fresh_star_def eqvt_at_def)

   885   apply (simp_all add: pure_fresh fresh_star_def eqvt_at_def)

   886   done

   886   done

   887 

   887 

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

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

   889 

   889 

   891 

   891 

   892 nominal_primrec  

   892 nominal_primrec  

   893   A :: "lam => lam"

   893   A :: "lam => lam"

   894 where  

   894 where  

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

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

   922 unfolding eqvt_def

   922 unfolding eqvt_def

   923 unfolding B_graph_def

   923 unfolding B_graph_def

   924 apply(perm_simp)

   924 apply(perm_simp)

   925 apply(rule allI)

   925 apply(rule allI)

   926 apply(rule refl)

   926 apply(rule refl)

   928 

   928 

   929 end

   929 end

   930 

   930 

   931 

   931 

   932 

   932