--- a/Nominal/Ex/Lambda.thy	Fri Jun 10 15:45:49 2011 +0900
+++ b/Nominal/Ex/Lambda.thy	Fri Jun 10 15:52:17 2011 +0900
@@ -605,6 +605,52 @@
 oops (* can this be defined ? *)
   (* Yes, if "sub" is a constant. *)
 
+text {* Working Examples *}
+
+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(rule TrueI)
+  apply (case_tac x, case_tac "eqvt a", case_tac b rule: lam.exhaust)
+  apply auto
+  apply (erule Abs_lst1_fcb)
+  apply (simp_all add: Abs_fresh_iff fresh_fun_eqvt_app)
+  apply (simp add: eqvt_def permute_fun_app_eq)
+  done
+
+termination
+  by (relation "measure (\<lambda>(_,t). size t)") (simp_all add: lam.size)
+
+nominal_primrec
+  trans2 :: "lam \<Rightarrow> atom list \<Rightarrow> db option"
+where
+  "trans2 (Var x) xs = (index xs 0 (atom x) \<guillemotright>= (\<lambda>n. Some (DBVar n)))"
+| "trans2 (App t1 t2) xs = ((trans2 t1 xs) \<guillemotright>= (\<lambda>db1. (trans2 t2 xs) \<guillemotright>= (\<lambda>db2. Some (DBApp db1 db2))))"
+| "trans2 (Lam [x].t) xs = (trans2 t (atom x # xs) \<guillemotright>= (\<lambda>db. Some (DBLam db)))"
+oops
+
+nominal_primrec
+  CPS :: "lam \<Rightarrow> (lam \<Rightarrow> lam) \<Rightarrow> lam"
+where
+  "CPS (Var x) k = Var x"
+| "CPS (App M N) k = CPS M (\<lambda>m. CPS N (\<lambda>n. n))"
+oops
+
+consts b :: name
+nominal_primrec
+  Z :: "lam \<Rightarrow> (lam \<Rightarrow> lam) \<Rightarrow> lam"
+where
+  "Z (App M N) k = Z M (%m. (Z N (%n.(App m n))))"
+| "Z (App M N) k = Z M (%m. (Z N (%n.(App (App m n) (Abs b (k (Var b)))))))"
+unfolding eqvt_def Z_graph_def
+apply (rule, perm_simp, rule)
+oops
 
 text {* tests of functions containing if and case *}
 
@@ -626,26 +672,6 @@
 | "C (App M N) = (if True then M else C N)"
 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(rule TrueI)
-  apply (case_tac x, case_tac "eqvt a", case_tac b rule: lam.exhaust)
-  apply auto
-  apply (erule Abs_lst1_fcb)
-  apply (simp_all add: Abs_fresh_iff fresh_fun_eqvt_app)
-  apply (simp add: eqvt_def permute_fun_app_eq)
-  done
-
-termination
-  by (relation "measure (\<lambda>(_,t). size t)") (simp_all add: lam.size)
-
 nominal_primrec  
   A :: "lam => lam"
 where  
@@ -667,41 +693,6 @@
 apply(rule refl)
 oops
 
-text {* "HO" functions *}
-
-nominal_primrec
-  trans2 :: "lam \<Rightarrow> atom list \<Rightarrow> db option"
-where
-  "trans2 (Var x) xs = (index xs 0 (atom x) \<guillemotright>= (\<lambda>n. Some (DBVar n)))"
-| "trans2 (App t1 t2) xs = ((trans2 t1 xs) \<guillemotright>= (\<lambda>db1. (trans2 t2 xs) \<guillemotright>= (\<lambda>db2. Some (DBApp db1 db2))))"
-| "trans2 (Lam [x].t) xs = (trans2 t (atom x # xs) \<guillemotright>= (\<lambda>db. Some (DBLam db)))"
-oops
-
-nominal_primrec
-  CPS :: "lam \<Rightarrow> (lam \<Rightarrow> lam) \<Rightarrow> lam"
-where
-  "CPS (Var x) k = Var x"
-| "CPS (App M N) k = CPS M (\<lambda>m. CPS N (\<lambda>n. n))"
-oops
-
-(* Problem: nominal_primrec generates non-quantified free variable "x" *)
-consts b :: name
-nominal_primrec
-  Z :: "lam \<Rightarrow> (lam \<Rightarrow> lam) \<Rightarrow> lam"
-where
-  "Z (App M N) k = Z M (%m. (Z N (%n.(App m n))))"
-| "Z (App M N) k = Z M (%m. (Z N (%n.(App (App m n) (Abs b (k (Var b)))))))"
-unfolding eqvt_def Z_graph_def
-apply (rule, perm_simp, rule)
-oops
-
-
-
-
-
-
-
-
 end