--- a/Nominal/Ex/LetSimple2.thy	Wed Jul 06 23:11:30 2011 +0200
+++ b/Nominal/Ex/LetSimple2.thy	Mon Jul 11 12:23:24 2011 +0100
@@ -123,7 +123,6 @@
   apply(simp_all)[5]
   apply(simp)
   apply(erule conjE)+
-  thm alpha_bn_cases
   apply(erule alpha_bn_cases)
   apply(simp)
   apply (subgoal_tac "height_trm_sumC b = height_trm_sumC ba")
@@ -153,7 +152,6 @@
   apply(simp_all)[5]
   apply(simp)
   apply(erule conjE)+
-  thm alpha_bn_cases
   apply(erule alpha_bn_cases)
   apply(simp)
   apply(simp add: trm_assn.bn_defs)
@@ -166,17 +164,29 @@
 
 section {* direct definitions --- problems *}
 
+lemma cheat: "P" sorry
 
-nominal_primrec
-    height_trm :: "trm \<Rightarrow> nat"
-and height_assn :: "assn \<Rightarrow> nat"
+nominal_primrec (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")
+    height_trm2 :: "trm \<Rightarrow> nat"
+and height_assn2 :: "assn \<Rightarrow> nat"
 where
-  "height_trm (Var x) = 1"
-| "height_trm (App l r) = max (height_trm l) (height_trm r)"
-| "height_trm (Let as b) = max (height_assn as) (height_trm b)"
-| "height_assn (Assn x t) = (height_trm t)"
-  apply (simp only: eqvt_def height_trm_height_assn_graph_def)
-  apply (rule, perm_simp, rule, rule TrueI)
+  "height_trm2 (Var x) = 1"
+| "height_trm2 (App l r) = max (height_trm2 l) (height_trm2 r)"
+| "height_trm2 (Let as b) = max (height_assn2 as) (height_trm2 b)"
+| "height_assn2 (Assn x t) = (height_trm2 t)"
+  thm height_trm2_height_assn2_graph.intros
+  thm height_trm2_height_assn2_graph_def
+  apply (simp only: eqvt_def height_trm2_height_assn2_graph_def)
+  apply (rule, perm_simp, rule)
+  apply(erule height_trm2_height_assn2_graph.induct)
+  -- "invariant"
+  apply(simp)
+  apply(simp)
+  apply(simp)
+  apply(simp)
+  apply(rule cheat)
+  apply -
+  --"completeness"
   apply (case_tac x)
   apply(simp)
   apply (case_tac a rule: trm_assn.exhaust(1))
@@ -190,47 +200,45 @@
   apply(simp_all)[7]
   prefer 2
   apply(simp)
+  prefer 2
+  apply(simp)
   --"let case"
-  apply (simp only: meta_eq_to_obj_eq[OF height_trm_def, symmetric, unfolded fun_eq_iff])
-  apply (simp only: meta_eq_to_obj_eq[OF height_assn_def, symmetric, unfolded fun_eq_iff])
-  apply (subgoal_tac "eqvt_at height_assn as")
-  apply (subgoal_tac "eqvt_at height_assn asa")
-  apply (subgoal_tac "eqvt_at height_trm b")
-  apply (subgoal_tac "eqvt_at height_trm ba")
-  apply (thin_tac "eqvt_at height_trm_height_assn_sumC (Inr as)")
-  apply (thin_tac "eqvt_at height_trm_height_assn_sumC (Inr asa)")
-  apply (thin_tac "eqvt_at height_trm_height_assn_sumC (Inl b)")
-  apply (thin_tac "eqvt_at height_trm_height_assn_sumC (Inl ba)")
+  apply (simp only: meta_eq_to_obj_eq[OF height_trm2_def, symmetric, unfolded fun_eq_iff])
+  apply (simp only: meta_eq_to_obj_eq[OF height_assn2_def, symmetric, unfolded fun_eq_iff])
+  apply (subgoal_tac "eqvt_at height_assn2 as")
+  apply (subgoal_tac "eqvt_at height_assn2 asa")
+  apply (subgoal_tac "eqvt_at height_trm2 b")
+  apply (subgoal_tac "eqvt_at height_trm2 ba")
+  apply (thin_tac "eqvt_at height_trm2_height_assn2_sumC (Inr as)")
+  apply (thin_tac "eqvt_at height_trm2_height_assn2_sumC (Inr asa)")
+  apply (thin_tac "eqvt_at height_trm2_height_assn2_sumC (Inl b)")
+  apply (thin_tac "eqvt_at height_trm2_height_assn2_sumC (Inl ba)")
   defer
-  apply (simp add: eqvt_at_def height_trm_def)
-  apply (simp add: eqvt_at_def height_trm_def)
-  apply (simp add: eqvt_at_def height_assn_def)
-  apply (simp add: eqvt_at_def height_assn_def)
-  prefer 2
-  apply (subgoal_tac "height_assn as = height_assn asa")
-  apply (subgoal_tac "height_trm b = height_trm ba")
+  apply (simp add: eqvt_at_def height_trm2_def)
+  apply (simp add: eqvt_at_def height_trm2_def)
+  apply (simp add: eqvt_at_def height_assn2_def)
+  apply (simp add: eqvt_at_def height_assn2_def)
+  apply (subgoal_tac "height_assn2 as = height_assn2 asa")
+  apply (subgoal_tac "height_trm2 b = height_trm2 ba")
   apply simp
   apply(simp)
   apply(erule conjE)+
   apply(erule alpha_bn_cases)
   apply(simp)
   apply(simp add: trm_assn.bn_defs)
-  thm Abs_lst_fcb2
   apply(erule_tac c="()" in Abs_lst_fcb2)
   apply(simp_all add: fresh_star_def pure_fresh)[3]
   apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def)
-  defer
-  apply(simp)
-  apply(frule Inl_inject)
-  apply(subst (asm) trm_assn.eq_iff)
   apply(drule Inl_inject)
+  apply(simp (no_asm_use))
   apply(clarify)
   apply(erule alpha_bn_cases)
   apply(simp del: trm_assn.eq_iff)
-  apply(rename_tac as s as' s' t' t x x')
   apply(simp only: trm_assn.bn_defs)
-  (* HERE *)
+  apply(erule_tac c="()" in Abs_lst1_fcb2')
+  apply(simp_all add: fresh_star_def pure_fresh)[3]
+
   oops