# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1306814061 -32400
# Node ID 5d0875b7ed3e188ba32a1a1b88e694b676f7e5ee
# Parent  d2154b4217073aac70f7cec5d4aa34b8c25a8901
Simple eqvt proofs with perm_simps for clarity

diff -r d2154b421707 -r 5d0875b7ed3e Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Tue May 31 00:36:16 2011 +0100
+++ b/Nominal/Ex/Lambda.thy	Tue May 31 12:54:21 2011 +0900
@@ -75,37 +75,12 @@
   "height (Var x) = 1"
 | "height (App t1 t2) = max (height t1) (height t2) + 1"
 | "height (Lam [x].t) = height t + 1"
-defer
+  unfolding eqvt_def height_graph_def
+  apply (rule, perm_simp, rule)
 apply(rule_tac y="x" in lam.exhaust)
 apply(auto simp add: lam.distinct lam.eq_iff)
 apply (erule Abs1_eq_fdest)
 apply(simp_all add: fresh_def pure_supp 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
@@ -122,7 +97,8 @@
   "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
+  unfolding eqvt_def frees_lst_graph_def
+  apply (rule, perm_simp, rule)
 apply(rule_tac y="x" in lam.exhaust)
 apply(simp_all)[3]
 apply(auto)[1]
@@ -132,32 +108,6 @@
 apply(drule supp_eqvt_at)
 apply(simp add: finite_supp)
 apply(auto simp add: fresh_def supp_removeAll eqvts eqvt_at_def)
-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
@@ -180,7 +130,8 @@
   "(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
+  unfolding eqvt_def subst_graph_def
+  apply (rule, perm_simp, rule)
 apply(auto simp add: lam.distinct lam.eq_iff)
 apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)
 apply(blast)+
@@ -193,33 +144,6 @@
 apply(subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> ya = ya")
 apply(simp add: eqvt_at_def)
 apply(rule perm_supp_eq,simp add: fresh_star_def fresh_Pair supp_swap)+
-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
@@ -374,7 +298,8 @@
   "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
+  unfolding eqvt_def trans_graph_def
+  apply (rule, perm_simp, rule)
 apply(case_tac x)
 apply(simp)
 apply(rule_tac y="a" and c="b" in lam.strong_exhaust)