# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1311064893 -3600
# Node ID 1dde421e380b5e7be1621cace5d53649b6b82e70
# Parent  967c55907ce1345959aae2887067b421cc84db2a# Parent  d5ecc2f7f299266abd2d9a1e575d096391da5743
merged

diff -r d5ecc2f7f299 -r 1dde421e380b Nominal/Ex/LetSimple2.thy
--- a/Nominal/Ex/LetSimple2.thy	Tue Jul 19 09:35:24 2011 +0100
+++ b/Nominal/Ex/LetSimple2.thy	Tue Jul 19 09:41:33 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
 
diff -r d5ecc2f7f299 -r 1dde421e380b Nominal/nominal_mutual.ML
--- a/Nominal/nominal_mutual.ML	Tue Jul 19 09:35:24 2011 +0100
+++ b/Nominal/nominal_mutual.ML	Tue Jul 19 09:41:33 2011 +0100
@@ -300,7 +300,7 @@
     val minducts = mutual_induct_rules lthy simple_pinduct all_f_defs m
     val mtermination = full_simplify rew_ss termination
     val mdomintros = Option.map (map (full_simplify rew_ss)) domintros
-    val meqvts = mk_meqvts lthy eqvt all_f_defs
+    val meqvts = [eqvt] (*mk_meqvts lthy eqvt all_f_defs*)
  in
     NominalFunctionResult { fs=fs, G=G, R=R,
       psimps=mpsimps, simple_pinducts=minducts,