diff -r ca6ca6fc28af -r 25d11b449e92 Nominal/Ex/TypeSchemes2.thy
--- a/Nominal/Ex/TypeSchemes2.thy	Tue Aug 07 18:53:50 2012 +0100
+++ b/Nominal/Ex/TypeSchemes2.thy	Tue Aug 07 18:54:52 2012 +0100
@@ -80,117 +80,7 @@
   "subst \<theta> (Var X) = lookup \<theta> X"
 | "subst \<theta> (Fun T1 T2) = Fun (subst \<theta> T1) (subst \<theta> T2)"
 | "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs T) = All xs (subst \<theta> T)"
-(*unfolding subst_substs_graph_def eqvt_def
-apply rule
-apply perm_simp
-apply (subst test3)
-defer
-apply (subst test3)
-defer
-apply (subst test3)
-defer
-apply rule*)
-thm subst_substs_graph.intros
-apply(subgoal_tac "\<And>p x r. subst_substs_graph x r \<Longrightarrow> subst_substs_graph (p \<bullet> x) (p \<bullet> r)")
-apply(simp add: eqvt_def)
-apply(rule allI)
-apply(simp add: permute_fun_def permute_bool_def)
-apply(rule ext)
-apply(rule ext)
-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)
---"Eqvt One way"
-apply(erule subst_substs_graph.induct)
-apply(perm_simp)
-apply(rule subst_substs_graph.intros)
-apply(erule subst_substs_graph.cases)
-apply(simp (no_asm_use) only: eqvts)
-apply(subst test)
-back
-apply (rule exI)
-apply(assumption)
-apply(rotate_tac 1)
-apply(erule subst_substs_graph.cases)
-apply(subst test)
-back
-apply (rule exI)
-apply(assumption)
-apply(perm_simp)
-apply(rule subst_substs_graph.intros)
-apply(assumption)
-apply(assumption)
-apply(subst test)
-back
-apply (rule exI)
-apply(assumption)
-apply(perm_simp)
-apply(rule subst_substs_graph.intros)
-apply(assumption)
-apply(assumption)
-apply(simp)
---"A"
-apply(simp (no_asm_use) only: eqvts)
-apply(subst test)
-back
-apply (rule exI)
-apply(assumption)
-apply(rotate_tac 1)
-apply(erule subst_substs_graph.cases)
-apply(subst test)
-back
-apply (rule exI)
-apply(assumption)
-apply(perm_simp)
-apply(rule subst_substs_graph.intros)
-apply(assumption)
-apply(assumption)
-apply(subst test)
-back
-apply (rule exI)
-apply(assumption)
-apply(perm_simp)
-apply(rule subst_substs_graph.intros)
-apply(assumption)
-apply(assumption)
-apply(simp)
---"A"
-apply(simp)
-apply(erule subst_substs_graph.cases)
-apply(simp (no_asm_use) only: eqvts)
-apply(subst test)
-back
-back
-apply (rule exI)
-apply(assumption)
-apply(rule subst_substs_graph.intros)
-apply (simp add: eqvts)
-apply (subgoal_tac "(p \<bullet> (atom ` fset xs)) \<sharp>* (p \<bullet> \<theta>)")
-apply (simp add: image_eqvt eqvts_raw eqvts)
-apply (simp only: fresh_star_permute_iff)
-apply(perm_simp)
-apply(assumption)
-apply(simp (no_asm_use) only: eqvts)
-apply(subst test)
-back
-back
-apply (rule exI)
-apply(assumption)
-apply(rule subst_substs_graph.intros)
-apply (simp add: eqvts)
-apply (subgoal_tac "(p \<bullet> (atom ` fset xs)) \<sharp>* (p \<bullet> \<theta>)")
-apply (simp add: image_eqvt eqvts_raw eqvts)
-apply (simp only: fresh_star_permute_iff)
-apply(perm_simp)
-apply(assumption)
-apply(simp)
---"Eqvt done"
+apply(simp add: subst_substs_graph_aux_def eqvt_def)
 apply(rule TrueI)
 apply (case_tac x)
 apply simp apply clarify