516 nominal_primrec

   517   map_term :: "(lam \<Rightarrow> lam) \<Rightarrow> lam \<Rightarrow> lam"

   518 where

   519   "eqvt f \<Longrightarrow> map_term f (Var x) = f (Var x)"

   520 | "eqvt f \<Longrightarrow> map_term f (App t1 t2) = App (f t1) (f t2)"

   521 | "eqvt f \<Longrightarrow> map_term f (Lam [x].t) = Lam [x].(f t)"

   522 | "\<not>eqvt f \<Longrightarrow> map_term f t = t"

   523   apply (simp add: eqvt_def map_term_graph_def)

   524   apply (rule, perm_simp, rule)

   525   apply (case_tac x, case_tac "eqvt a", case_tac b rule: lam.exhaust)

   526   apply auto

   527   apply (simp add: Abs1_eq_iff)

   528   apply (auto)

   529   apply (simp add: eqvt_def permute_fun_app_eq)

   530   apply (drule supp_fun_app_eqvt)

   531   apply (simp add: fresh_def )

   532   apply blast

   533   apply (simp add: eqvt_def permute_fun_app_eq)

   534   apply (drule supp_fun_app_eqvt)

   535   apply (simp add: fresh_def )

   536   apply blast

   537   done

   538 

   539 termination

   540   by (relation "measure (\<lambda>(_,t). size t)") (simp_all add: lam.size)

   541