--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Lambda_add.thy	Thu Feb 17 12:01:08 2011 +0900
@@ -0,0 +1,79 @@
+theory Lambda_add
+imports "Lambda"
+begin
+
+nominal_primrec
+  addlam_pre :: "lam \<Rightarrow> lam \<Rightarrow> lam"
+where
+  "fv \<noteq> x \<Longrightarrow> addlam_pre (Var x) (Lam [fv].it) = Lam [fv]. App (Var fv) (Var x)"
+| "addlam_pre (Var x) (App t1 t2) = Var x"
+| "addlam_pre (Var x) (Var v) = Var x"
+| "addlam_pre (App t1 t2) it = App t1 t2"
+| "addlam_pre (Lam [x]. t) it = Lam [x].t"
+apply (subgoal_tac "\<And>p a x. addlam_pre_graph a x \<Longrightarrow> addlam_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 addlam_pre_graph.induct)
+apply (simp_all add: addlam_pre_graph.intros)
+apply (simp_all add:lam.distinct)
+apply clarify
+apply simp
+apply (rule_tac y="a" in lam.exhaust)
+apply(auto simp add: lam.distinct lam.eq_iff)
+prefer 2 apply blast
+prefer 2 apply blast
+apply (rule_tac y="b" and c="name" in lam.strong_exhaust)
+apply(auto simp add: lam.distinct lam.eq_iff)[3]
+apply blast
+apply(drule_tac x="namea" in meta_spec)
+apply(drule_tac x="name" in meta_spec)
+apply(drule_tac x="lam" in meta_spec)
+apply (auto simp add: fresh_star_def atom_name_def fresh_at_base)[1]
+apply (auto simp add: lam.eq_iff Abs1_eq_iff fresh_def lam.supp supp_at_base)
+done
+
+termination
+  by (relation "measure (\<lambda>(t,_). size t)")
+     (simp_all add: lam.size)
+
+function
+  addlam :: "lam \<Rightarrow> lam"
+where
+  "addlam (Var x) = addlam_pre (Var x) (Lam [x]. (Var x))"
+| "addlam (App t1 t2) = App t1 t2"
+| "addlam (Lam [x]. t) = Lam [x].t"
+apply (simp_all add:lam.distinct)
+apply (rule_tac y="x" in lam.exhaust)
+apply auto
+apply (simp add:lam.eq_iff)
+done
+
+termination
+  by (relation "measure (\<lambda>(t). size t)")
+     (simp_all add: lam.size)
+
+lemma addlam':
+  "fv \<noteq> x \<Longrightarrow> addlam (Var x) = Lam [fv]. App (Var fv) (Var x)"
+  apply simp
+  apply (subgoal_tac "Lam [x]. Var x = Lam [fv]. Var fv")
+  apply simp
+  apply (simp add: lam.eq_iff Abs1_eq_iff lam.supp fresh_def supp_at_base)
+  done
+
+end
+
+
+