--- a/Nominal/Ex/LetSimple2.thy	Tue Jul 19 02:30:05 2011 +0100
+++ b/Nominal/Ex/LetSimple2.thy	Tue Jul 19 08:34:54 2011 +0100
@@ -175,7 +175,35 @@
 
 lemma cheat: "P" sorry
 
+definition
+  "eqvt_at_bn f as \<equiv> \<forall>p. (p \<bullet> (f as)) = f (permute_bn p as)"
+
+definition
+  "alpha_bn_preserve f as \<equiv> \<forall>p. f as = f (permute_bn p as)"
+
+lemma
+  fixes as::"assn"
+  assumes "eqvt_at f as"
+  shows "eqvt_at_bn f as"
+using assms
+unfolding eqvt_at_bn_def
+apply(rule_tac allI)
+apply(drule k)
+apply(erule conjE)
+apply(subst (asm) eqvt_at_def)
+apply(simp)
+
+oops
+
+
+
 nominal_primrec 
+<<<<<<< variant A
+ (invariant "\<lambda>x y. case x of Inl x1 \<Rightarrow> True | Inr x2 \<Rightarrow> alpha_bn_preserve (height_assn2::assn \<Rightarrow> nat) x2")
+>>>>>>> variant B
+####### Ancestor
+ (invariant "\<lambda>x y. case x of Inl x1 \<Rightarrow> True | Inr x2 \<Rightarrow> \<forall>p. (permute_bn p x2) = x2 \<longrightarrow> (p \<bullet> y) = y")
+======= end
     height_trm2 :: "trm \<Rightarrow> nat"
 and height_assn2 :: "assn \<Rightarrow> nat"
 where
@@ -189,6 +217,26 @@
   apply (rule, perm_simp, rule)
   -- "invariant"
   apply(simp)
+<<<<<<< variant A
+  apply(simp)
+  apply(simp)
+  apply(simp)
+  apply(simp add: alpha_bn_preserve_def)
+  apply(simp add: height_assn2_def)
+  apply(simp add: trm_assn.perm_bn_simps)
+  apply(rule allI)
+  thm height_trm2_height_assn2_graph.intros[no_vars]
+  thm height_trm2_height_assn2_sumC_def
+  apply(rule cheat)
+  apply -
+>>>>>>> variant B
+####### Ancestor
+  apply(simp)
+  apply(simp)
+  apply(simp)
+  apply(rule cheat)
+  apply -
+======= end
   --"completeness"
   apply (case_tac x)
   apply(simp)
@@ -246,6 +294,16 @@
   apply(erule alpha_bn_cases)
   apply(simp del: trm_assn.eq_iff)
   apply(simp only: trm_assn.bn_defs)
+<<<<<<< variant A
+  apply(erule_tac c="()" in Abs_lst1_fcb2')
+  apply(simp_all add: fresh_star_def pure_fresh)[3]
+  apply(simp add: eqvt_at_bn_def)
+  apply(simp add: trm_assn.perm_bn_simps)
+  apply(simp add: eqvt_at_bn_def)
+  apply(simp add: trm_assn.perm_bn_simps)
+  done
+ 
+>>>>>>> variant B
   apply(erule_tac c="(trm_rawa)" in Abs_lst1_fcb2')
   apply(simp_all add: fresh_star_def pure_fresh)[2]
   apply(simp add: trm_assn.supp)
@@ -258,6 +316,12 @@
   apply(simp add: eqvt_at_def perm_supp_eq)
   apply(simp add: eqvt_at_def perm_supp_eq)
   done
+####### Ancestor
+  apply(erule_tac c="()" in Abs_lst1_fcb2')
+  apply(simp_all add: fresh_star_def pure_fresh)[3]
+
+  oops
+======= end
 
 termination by lexicographic_order