--- a/Nominal/Ex/Lambda_add.thy	Tue Mar 08 09:07:27 2011 +0000
+++ b/Nominal/Ex/Lambda_add.thy	Tue Mar 08 09:07:49 2011 +0000
@@ -73,6 +73,80 @@
   apply (simp add: lam.eq_iff Abs1_eq_iff lam.supp fresh_def supp_at_base)
   done
 
+nominal_primrec
+  Pair_pre
+where
+  "atom z \<sharp> (M, N) \<Longrightarrow> (Pair_pre M N) (Lam [z]. _) = (Lam [z]. App (App (Var z) M) N)"
+| "(Pair_pre M N) (App l r) = (App l r)"
+| "(Pair_pre M N) (Var v) = (Var v)"
+apply (subgoal_tac "\<And>p a x. Pair_pre_graph a x \<Longrightarrow> Pair_pre_graph (p \<bullet> a) (p \<bullet> x)")
+apply (simp add: eqvt_def)
+apply (intro allI)
+apply(simp add: permute_fun_def)
+apply(rule ext)
+apply(rule ext)
+apply(simp add: permute_bool_def)
+apply rule
+apply(drule_tac x="p" in meta_spec)
+apply(drule_tac x="- p \<bullet> x" in meta_spec)
+apply(drule_tac x="- p \<bullet> xa" in meta_spec)
+apply simp
+apply(drule_tac x="-p" in meta_spec)
+apply(drule_tac x="x" in meta_spec)
+apply(drule_tac x="xa" in meta_spec)
+apply simp
+apply (erule Pair_pre_graph.induct)
+apply (simp_all add: Pair_pre_graph.intros)[3]
+  apply (case_tac x)
+  apply clarify
+  apply (simp add: symmetric[OF atomize_conjL])
+  apply (rule_tac y="c" and c="(ab, ba)" in lam.strong_exhaust)
+  apply (simp_all add: lam.distinct symmetric[OF atomize_conjL] lam.eq_iff Abs1_eq_iff fresh_star_def)
+  apply auto[1]
+  apply (simp_all add: fresh_Pair lam.fresh fresh_at_base)
+  apply (rule swap_fresh_fresh[symmetric])
+  prefer 3
+  apply (rule swap_fresh_fresh[symmetric])
+  apply simp_all
+  done
+
+termination
+  by (relation "measure (\<lambda>(t,_). size t)")
+     (simp_all add: lam.size)
+
+consts cx :: name
+
+fun
+  Pair where
+  "(Pair M N) = (Pair_pre M N (Lam [cx]. Var cx))"
+
+lemma Pair : "atom z \<sharp> (M, N) \<Longrightarrow> Pair M N = (Lam [z]. App (App (Var z) M) N)"
+  apply simp
+  apply (subgoal_tac "Lam [cx]. Var cx = Lam[z]. Var z")
+  apply simp
+  apply (auto simp add: lam.eq_iff Abs1_eq_iff)
+  by (metis Rep_name_inject atom_name_def fresh_at_base lam.fresh(1))
+
+
+definition Lam_I_pre : "\<II> \<equiv> Lam[cx]. Var cx"
+
+lemma Lam_I : "\<II> = Lam[x]. Var x"
+  by (simp add: Lam_I_pre lam.eq_iff Abs1_eq_iff lam.fresh supp_at_base)
+     (metis Rep_name_inverse atom_name_def fresh_at_base)
+
+definition c1 :: name where "c1 \<equiv> Abs_name (Atom (Sort ''Lambda.name'' []) 1)"
+definition c2 :: name where "c2 \<equiv> Abs_name (Atom (Sort ''Lambda.name'' []) 2)"
+
+lemma c1_c2[simp]:
+  "c1 \<noteq> c2"
+  unfolding c1_def c2_def
+  by (simp add: Abs_name_inject)
+
+definition Lam_F_pre : "\<FF> \<equiv> Lam[c1]. Lam[c2]. Var c2"
+lemma Lam_F : "\<FF> = Lam[x]. Lam[y]. Var y"
+  by (simp add: Lam_F_pre lam.eq_iff Abs1_eq_iff lam.fresh supp_at_base)
+     (metis Rep_name_inverse atom_name_def fresh_at_base)
+
 end