# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1306815935 -32400
# Node ID 9bc46d04fb2cd3af846d39de76919eb8d005026e
# Parent  8042bf23af1ce6301e4343ba0de2ad4f65a39336
map_term can be defined when equivariance is assumed

diff -r 8042bf23af1c -r 9bc46d04fb2c Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Tue May 31 13:21:00 2011 +0900
+++ b/Nominal/Ex/Lambda.thy	Tue May 31 13:25:35 2011 +0900
@@ -513,6 +513,32 @@
 (*apply (erule Abs1_eq_fdest)*)
 oops
 
+nominal_primrec
+  map_term :: "(lam \<Rightarrow> lam) \<Rightarrow> lam \<Rightarrow> lam"
+where
+  "eqvt f \<Longrightarrow> map_term f (Var x) = f (Var x)"
+| "eqvt f \<Longrightarrow> map_term f (App t1 t2) = App (f t1) (f t2)"
+| "eqvt f \<Longrightarrow> map_term f (Lam [x].t) = Lam [x].(f t)"
+| "\<not>eqvt f \<Longrightarrow> map_term f t = t"
+  apply (simp add: eqvt_def map_term_graph_def)
+  apply (rule, perm_simp, rule)
+  apply (case_tac x, case_tac "eqvt a", case_tac b rule: lam.exhaust)
+  apply auto
+  apply (simp add: Abs1_eq_iff)
+  apply (auto)
+  apply (simp add: eqvt_def permute_fun_app_eq)
+  apply (drule supp_fun_app_eqvt)
+  apply (simp add: fresh_def )
+  apply blast
+  apply (simp add: eqvt_def permute_fun_app_eq)
+  apply (drule supp_fun_app_eqvt)
+  apply (simp add: fresh_def )
+  apply blast
+  done
+
+termination
+  by (relation "measure (\<lambda>(_,t). size t)") (simp_all add: lam.size)
+
 nominal_primrec  
   A :: "lam => lam"
 where