diff -r 5335c0ea743a -r 313e6f2cdd89 Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Thu May 31 12:01:13 2012 +0100
+++ b/Nominal/Ex/Lambda.thy	Mon Jun 04 21:39:51 2012 +0100
@@ -40,7 +40,6 @@
 | "is_app (App t1 t2) = True"
 | "is_app (Lam [x]. t) = False"
 apply(simp add: eqvt_def is_app_graph_def)
-apply (rule, perm_simp, rule)
 apply(rule TrueI)
 apply(rule_tac y="x" in lam.exhaust)
 apply(auto)[3]
@@ -61,7 +60,6 @@
 | "rator (App t1 t2) = Some t1"
 | "rator (Lam [x]. t) = None"
 apply(simp add: eqvt_def rator_graph_def)
-apply (rule, perm_simp, rule)
 apply(rule TrueI)
 apply(rule_tac y="x" in lam.exhaust)
 apply(auto)[3]
@@ -77,7 +75,6 @@
 | "rand (App t1 t2) = Some t2"
 | "rand (Lam [x]. t) = None"
 apply(simp add: eqvt_def rand_graph_def)
-apply (rule, perm_simp, rule)
 apply(rule TrueI)
 apply(rule_tac y="x" in lam.exhaust)
 apply(auto)[3]
@@ -94,7 +91,6 @@
 | "is_eta_nf (Lam [x]. t) = (is_eta_nf t \<and> 
                              ((is_app t \<and> rand t = Some (Var x)) \<longrightarrow> atom x \<in> supp (rator t)))"
 apply(simp add: eqvt_def is_eta_nf_graph_def)
-apply (rule, perm_simp, rule)
 apply(rule TrueI)
 apply(rule_tac y="x" in lam.exhaust)
 apply(auto)[3]
@@ -102,11 +98,7 @@
 apply(erule_tac c="()" in Abs_lst1_fcb2')
 apply(simp_all add: pure_fresh fresh_star_def)[3]
 apply(simp add: eqvt_at_def conj_eqvt)
-apply(perm_simp)
-apply(rule refl)
 apply(simp add: eqvt_at_def conj_eqvt)
-apply(perm_simp)
-apply(rule refl)
 done
 
 termination (eqvt) by lexicographic_order
@@ -128,7 +120,6 @@
 | "var_pos y (App t1 t2) = (Cons Left ` (var_pos y t1)) \<union> (Cons Right ` (var_pos y t2))"
 | "atom x \<sharp> y \<Longrightarrow> var_pos y (Lam [x]. t) = (Cons In ` (var_pos y t))"
 apply(simp add: eqvt_def var_pos_graph_def)
-apply (rule, perm_simp, rule)
 apply(rule TrueI)
 apply(case_tac x)
 apply(rule_tac y="b" and c="a" in lam.strong_exhaust)
@@ -138,12 +129,14 @@
 apply(erule_tac Abs_lst1_fcb2)
 apply(simp add: pure_fresh)
 apply(simp add: fresh_star_def)
-apply(simp add: eqvt_at_def image_eqvt perm_supp_eq)
+apply(simp only: eqvt_at_def)
 apply(perm_simp)
-apply(rule refl)
-apply(simp add: eqvt_at_def image_eqvt perm_supp_eq)
+apply(simp)
+apply(simp add: perm_supp_eq)
+apply(simp only: eqvt_at_def)
 apply(perm_simp)
-apply(rule refl)
+apply(simp)
+apply(simp add: perm_supp_eq)
 done
 
 termination (eqvt) by lexicographic_order
@@ -172,7 +165,6 @@
 | "(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 ::== (App (Var y) s)])"
   apply(simp add: eqvt_def subst'_graph_def)
-  apply(perm_simp, simp)
   apply(rule TrueI)
   apply(case_tac x)
   apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust)
@@ -182,8 +174,14 @@
   apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2)
   apply(simp_all add: Abs_fresh_iff)
   apply(simp add: fresh_star_def fresh_Pair)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp only: eqvt_at_def)
+  apply(perm_simp)
+  apply(simp)
+  apply(simp add: fresh_star_Pair perm_supp_eq)
+  apply(simp only: eqvt_at_def)
+  apply(perm_simp)
+  apply(simp)
+  apply(simp add: fresh_star_Pair perm_supp_eq)
 done
 
 termination (eqvt) by lexicographic_order
@@ -201,7 +199,7 @@
 | "frees_lst (Lam [x]. t) = removeAll (atom x) (frees_lst t)"
   unfolding eqvt_def
   unfolding frees_lst_graph_def
-  apply (rule, perm_simp, rule)
+apply(simp)
 apply(rule TrueI)
 apply(rule_tac y="x" in lam.exhaust)
 apply(auto)
@@ -227,7 +225,6 @@
 | "frees_set (App t1 t2) = frees_set t1 \<union> frees_set t2"
 | "frees_set (Lam [x]. t) = (frees_set t) - {atom x}"
   apply(simp add: eqvt_def frees_set_graph_def)
-  apply(rule, perm_simp, rule)
   apply(erule frees_set_graph.induct)
   apply(auto)[9]
   apply(rule_tac y="x" in lam.exhaust)
@@ -236,8 +233,8 @@
   apply(erule_tac c="()" in Abs_lst1_fcb2)
   apply(simp add: fresh_minus_atom_set)
   apply(simp add: fresh_star_def fresh_Unit)
-  apply(simp add: Diff_eqvt eqvt_at_def, perm_simp, rule refl)
-  apply(simp add: Diff_eqvt eqvt_at_def, perm_simp, rule refl)
+  apply(simp add: Diff_eqvt eqvt_at_def)
+  apply(simp add: Diff_eqvt eqvt_at_def)
   done
 
 termination (eqvt) 
@@ -255,7 +252,6 @@
 | "height (App t1 t2) = max (height t1) (height t2) + 1"
 | "height (Lam [x].t) = height t + 1"
   apply(simp add: eqvt_def height_graph_def)
-  apply (rule, perm_simp, rule)
   apply(rule TrueI)
   apply(rule_tac y="x" in lam.exhaust)
   apply(auto)
@@ -278,7 +274,7 @@
 | "(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])"
   unfolding eqvt_def subst_graph_def
-  apply (rule, perm_simp, rule)
+  apply(simp)
   apply(rule TrueI)
   apply(auto)
   apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)
@@ -287,8 +283,14 @@
   apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2)
   apply(simp_all add: Abs_fresh_iff)
   apply(simp add: fresh_star_def fresh_Pair)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp only: eqvt_at_def)
+  apply(perm_simp)
+  apply(simp)
+  apply(simp add: fresh_star_Pair perm_supp_eq)
+  apply(simp only: eqvt_at_def)
+  apply(perm_simp)
+  apply(simp)
+  apply(simp add: fresh_star_Pair perm_supp_eq)
 done
 
 termination (eqvt)
@@ -457,7 +459,6 @@
 | "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))"
   apply (simp add: eqvt_def trans_graph_def)
-  apply (rule, perm_simp, rule)
   apply (erule trans_graph.induct)
   apply (auto simp add: ln.fresh)[3]
   apply (simp add: supp_lookup_fresh)
@@ -471,8 +472,12 @@
   apply (erule_tac c="xsa" in Abs_lst1_fcb2')
   apply (simp add: fresh_star_def)
   apply (simp add: fresh_star_def)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp only: eqvt_at_def)
+  apply(perm_simp)
+  apply(simp add: fresh_star_Pair perm_supp_eq)
+  apply(simp only: eqvt_at_def)
+  apply(perm_simp)
+  apply(simp add: fresh_star_Pair perm_supp_eq)
   done
 
 termination (eqvt)
@@ -488,7 +493,6 @@
 | "cntlams (App t1 t2) = (cntlams t1) + (cntlams t2)"
 | "cntlams (Lam [x]. t) = Suc (cntlams t)"
   apply(simp add: eqvt_def cntlams_graph_def)
-  apply(rule, perm_simp, rule)
   apply(rule TrueI)
   apply(rule_tac y="x" in lam.exhaust)
   apply(auto)[3]
@@ -515,7 +519,6 @@
 | "cntbvs (App t1 t2) xs = (cntbvs t1 xs) + (cntbvs t2 xs)"
 | "atom x \<sharp> xs \<Longrightarrow> cntbvs (Lam [x]. t) xs = cntbvs t (x # xs)"
   apply(simp add: eqvt_def cntbvs_graph_def)
-  apply(rule, perm_simp, rule)
   apply(rule TrueI)
   apply(case_tac x)
   apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
@@ -528,8 +531,12 @@
   apply(erule Abs_lst1_fcb2')
   apply(simp add: pure_fresh fresh_star_def)
   apply(simp add: fresh_star_def)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp only: eqvt_at_def)
+  apply(perm_simp)
+  apply(simp add: fresh_star_Pair perm_supp_eq)
+  apply(simp only: eqvt_at_def)
+  apply(perm_simp)
+  apply(simp add: fresh_star_Pair perm_supp_eq)
   done
 
 termination (eqvt)
@@ -570,7 +577,7 @@
       Option.bind (transdb t1 xs) (\<lambda>d1. Option.bind (transdb t2 xs) (\<lambda>d2. Some (DBApp d1 d2)))"
 | "x \<notin> set xs \<Longrightarrow> transdb (Lam [x].t) xs = Option.map DBLam (transdb t (x # xs))"
   unfolding eqvt_def transdb_graph_def
-  apply (rule, perm_simp, rule)
+  apply(simp)
   apply(rule TrueI)
   apply (case_tac x)
   apply (rule_tac y="a" and c="b" in lam.strong_exhaust)
@@ -580,7 +587,14 @@
   apply (erule_tac c="xsa" in Abs_lst1_fcb2')
   apply (simp add: pure_fresh)
   apply(simp add: fresh_star_def fresh_at_list)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq eqvts eqvts_raw)+
+  apply(simp only: eqvt_at_def)
+  apply(perm_simp)
+  apply(simp)
+  apply(simp add: fresh_star_Pair perm_supp_eq)
+  apply(simp only: eqvt_at_def)
+  apply(perm_simp)
+  apply(simp)
+  apply(simp add: fresh_star_Pair perm_supp_eq)
   done
 
 termination (eqvt)
@@ -624,7 +638,6 @@
 | "apply_subst (App t0 t1) t2 = App (App t0 t1) t2"
 | "atom x \<sharp> t2 \<Longrightarrow> apply_subst (Lam [x].t1) t2 = eval (t1[x::= t2])"
   apply(simp add: eval_apply_subst_graph_def eqvt_def)
-  apply(rule, perm_simp, rule)
   apply(rule TrueI)
   apply (case_tac x)
   apply (case_tac a rule: lam.exhaust)
@@ -648,8 +661,12 @@
   apply (simp add: finite_supp)
   apply (simp add: fresh_Inl var_fresh_subst)
   apply(simp add: fresh_star_def)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq subst.eqvt)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq subst.eqvt)
+  apply(simp only: eqvt_at_def)
+  apply(perm_simp)
+  apply(simp add: fresh_star_Pair perm_supp_eq)
+  apply(simp only: eqvt_at_def)
+  apply(perm_simp)
+  apply(simp add: fresh_star_Pair perm_supp_eq)
 done
 
 
@@ -671,7 +688,7 @@
 | "q (Var x) N = Var x"
 | "q (App l r) N = App l r"
 unfolding eqvt_def q_graph_def
-apply (rule, perm_simp, rule)
+apply (simp)
 apply (rule TrueI)
 apply (case_tac x)
 apply (rule_tac y="a" in lam.exhaust)
@@ -699,7 +716,6 @@
 | "eqvt f \<Longrightarrow> map_term f (Lam [x].t) = Lam [x].(f t)"
 | "\<not>eqvt f \<Longrightarrow> map_term f t = t"
   apply (simp add: eqvt_def map_term_graph_def)
-  apply (rule, perm_simp, rule)
   apply(rule TrueI)
   apply (case_tac x, case_tac "eqvt a", case_tac b rule: lam.exhaust)
   apply auto
@@ -819,7 +835,6 @@
 | "\<lbrakk>{atom x} \<sharp>* (s, xs); {atom y} \<sharp>* (t, xs); x \<noteq> y\<rbrakk> \<Longrightarrow> 
        aux (Lam [x].t) (Lam [y].s) xs = aux t s ((x, y) # xs)"
   apply (simp add: eqvt_def aux_graph_def)
-  apply (rule, perm_simp, rule)
   apply(erule aux_graph.induct)
   apply(simp_all add: fresh_star_def pure_fresh)[9]
   apply(case_tac x)
@@ -867,7 +882,7 @@
 | "aux2 (Lam [x].t) (App t1 t2) = False"
 | "x = y \<Longrightarrow> aux2 (Lam [x].t) (Lam [y].s) = aux2 t s"
   apply(simp add: eqvt_def aux2_graph_def)
-  apply(rule, perm_simp, rule, rule)
+  apply(simp)
   apply(case_tac x)
   apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
   apply(rule_tac y="b" in lam.exhaust)