--- a/Nominal/Ex/Lambda.thy	Tue Jan 25 02:51:44 2011 +0900
+++ b/Nominal/Ex/Lambda.thy	Tue Jan 25 18:58:26 2011 +0100
@@ -17,6 +17,7 @@
   "height (Var x) = 1"
 | "height (App t1 t2) = max (height t1) (height t2) + 1"
 | "height (Lam [x].t) = height t + 1"
+defer
 apply(rule_tac y="x" in lam.exhaust)
 apply(auto simp add: lam.distinct lam.eq_iff)
 apply(simp add: Abs_eq_iff alphas)
@@ -24,11 +25,39 @@
 apply(subst (4) supp_perm_eq[where p="p", symmetric])
 apply(simp add: pure_supp fresh_star_def)
 apply(simp add: eqvt_at_def)
+apply(subgoal_tac "\<And>p x r. height_graph x r \<Longrightarrow> height_graph (p \<bullet> x) (p \<bullet> r)") 
+unfolding eqvt_def
+apply(rule allI)
+apply(simp add: permute_fun_def)
+apply(rule ext)
+apply(rule ext)
+apply(simp add: permute_bool_def)
+apply(rule iffI)
+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 height_graph.induct)
+apply(perm_simp)
+apply(rule height_graph.intros)
+apply(perm_simp)
+apply(rule height_graph.intros)
+apply(assumption)
+apply(assumption)
+apply(perm_simp)
+apply(rule height_graph.intros)
+apply(assumption)
 done
 
 termination
   by (relation "measure size") (simp_all add: lam.size)
   
+thm height.simps
+
   
 text {* free name function - returns atom lists *}
 
@@ -38,6 +67,7 @@
   "frees_lst (Var x) = [atom x]"
 | "frees_lst (App t1 t2) = frees_lst t1 @ frees_lst t2"
 | "frees_lst (Lam [x]. t) = removeAll (atom x) (frees_lst t)"
+defer
 apply(rule_tac y="x" in lam.exhaust)
 apply(simp_all)[3]
 apply(simp_all only: lam.distinct)
@@ -57,6 +87,32 @@
 apply(auto simp add: fresh_star_def)[1]
 unfolding eqvt_at_def
 apply(simp only: removeAll_eqvt atom_eqvt)
+apply(subgoal_tac "\<And>p x r. frees_lst_graph x r \<Longrightarrow> frees_lst_graph (p \<bullet> x) (p \<bullet> r)") 
+unfolding eqvt_def
+apply(rule allI)
+apply(simp add: permute_fun_def)
+apply(rule ext)
+apply(rule ext)
+apply(simp add: permute_bool_def)
+apply(rule iffI)
+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 frees_lst_graph.induct)
+apply(perm_simp)
+apply(rule frees_lst_graph.intros)
+apply(perm_simp)
+apply(rule frees_lst_graph.intros)
+apply(assumption)
+apply(assumption)
+apply(perm_simp)
+apply(rule frees_lst_graph.intros)
+apply(assumption)
 done
 
 termination
@@ -79,6 +135,7 @@
   "(Var x)[y ::= s] = (if x = y then s else (Var x))"
 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])"
 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])"
+defer
 apply(auto simp add: lam.distinct lam.eq_iff)
 apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)
 apply(blast)+
@@ -115,6 +172,33 @@
 apply(simp add: Abs_fresh_iff)
 apply(drule sym)
 apply(simp add: Abs_fresh_iff)
+apply(subgoal_tac "\<And>p x r. subst_graph x r \<Longrightarrow> subst_graph (p \<bullet> x) (p \<bullet> r)") 
+unfolding eqvt_def
+apply(rule allI)
+apply(simp add: permute_fun_def)
+apply(rule ext)
+apply(rule ext)
+apply(simp add: permute_bool_def)
+apply(rule iffI)
+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 subst_graph.induct)
+apply(perm_simp)
+apply(rule subst_graph.intros)
+apply(perm_simp)
+apply(rule subst_graph.intros)
+apply(assumption)
+apply(assumption)
+apply(perm_simp)
+apply(rule subst_graph.intros)
+apply(simp add: fresh_Pair)
+apply(assumption)
 done
 
 termination
@@ -249,6 +333,7 @@
   "trans (Var x) xs = lookup xs 0 x"
 | "trans (App t1 t2) xs = LNApp (trans t1 xs) (trans t2 xs)"
 | "atom x \<sharp> xs \<Longrightarrow> trans (Lam [x]. t) xs = LNLam (trans t (x # xs))"
+defer
 apply(case_tac x)
 apply(simp)
 apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
@@ -335,53 +420,13 @@
 apply(simp_all add: permute_pure)
 done
 
-ML {*
-Nominal_Function_Core.trace := true
-*}
-
 (*
-inductive
-  trans_graph
-where
-  "trans_graph (Var x, xs) (index xs 0 (atom x) \<guillemotright>= (\<lambda>v. Some (DBVar v)))" 
-| "\<lbrakk>trans_graph (t1, xs) (trans_sum (t1, xs)); 
-    \<And>a. trans_sum (t1, xs) = Some a \<Longrightarrow> trans_graph (t2, xs) (trans_sum (t2, xs))\<rbrakk>
-    \<Longrightarrow> trans_graph (App t1 t2, xs) 
-       (trans_sum (t1, xs) \<guillemotright>= (\<lambda>v. trans_sum (t2, xs) \<guillemotright>= (\<lambda>va. Some (DBApp v va))))"
-| "trans_graph (t, atom x # xs) (trans_sum (t, atom x # xs)) \<Longrightarrow>
-    trans_graph (Lam x t, xs) (trans_sum (t, atom x # xs) \<guillemotright>= (\<lambda>v. Some (DBLam v)))"
-
-lemma
-  assumes a: "trans_graph x t"
-  shows "trans_graph (p \<bullet> x) (p \<bullet> t)"
-using a
-apply(induct)
-apply(perm_simp)
-apply(rule trans_graph.intros)
-apply(perm_simp)
-apply(rule trans_graph.intros)
-apply(simp)
-apply(simp)
-defer
-apply(perm_simp)
-apply(rule trans_graph.intros)
-apply(simp)
-apply(rotate_tac 3)
-apply(drule_tac x="FOO" in meta_spec)
-apply(drule meta_mp)
-prefer 2
-apply(simp)
-
-equivariance trans_graph
-*)
-
-(* equivariance fails at the moment
 nominal_primrec
   trans :: "lam \<Rightarrow> atom list \<Rightarrow> db option"
 where
   "trans (Var x) xs = (index xs 0 (atom x) \<guillemotright>= (\<lambda>n. Some (DBVar n)))"
-| "trans (App t1 t2) xs = (trans t1 xs \<guillemotright>= (\<lambda>db1. trans t2 xs \<guillemotright>= (\<lambda>db2. Some (DBApp db1 db2))))"
-| "trans (Lam x t) xs = (trans t (atom x # xs) \<guillemotright>= (\<lambda>db. Some (DBLam db)))"
+| "trans (App t1 t2) xs = ((trans t1 xs) \<guillemotright>= (\<lambda>db1. (trans t2 xs) \<guillemotright>= (\<lambda>db2. Some (DBApp db1 db2))))"
+| "trans (Lam [x].t) xs = (trans t (atom x # xs) \<guillemotright>= (\<lambda>db. Some (DBLam db)))"
 *)