diff -r ca6ca6fc28af -r 25d11b449e92 Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Tue Aug 07 18:53:50 2012 +0100
+++ b/Nominal/Ex/Lambda.thy	Tue Aug 07 18:54:52 2012 +0100
@@ -7,7 +7,6 @@
 
 atom_decl name
 
-
 ML {* trace := true *}
 
 nominal_datatype lam =
@@ -39,7 +38,7 @@
   "is_app (Var x) = False"
 | "is_app (App t1 t2) = True"
 | "is_app (Lam [x]. t) = False"
-apply(simp add: eqvt_def is_app_graph_def)
+apply(simp add: eqvt_def is_app_graph_aux_def)
 apply(rule TrueI)
 apply(rule_tac y="x" in lam.exhaust)
 apply(auto)[3]
@@ -59,7 +58,7 @@
   "rator (Var x) = None"
 | "rator (App t1 t2) = Some t1"
 | "rator (Lam [x]. t) = None"
-apply(simp add: eqvt_def rator_graph_def)
+apply(simp add: eqvt_def rator_graph_aux_def)
 apply(rule TrueI)
 apply(rule_tac y="x" in lam.exhaust)
 apply(auto)[3]
@@ -74,7 +73,7 @@
   "rand (Var x) = None"
 | "rand (App t1 t2) = Some t2"
 | "rand (Lam [x]. t) = None"
-apply(simp add: eqvt_def rand_graph_def)
+apply(simp add: eqvt_def rand_graph_aux_def)
 apply(rule TrueI)
 apply(rule_tac y="x" in lam.exhaust)
 apply(auto)[3]
@@ -90,7 +89,7 @@
 | "is_eta_nf (App t1 t2) = (is_eta_nf t1 \<and> is_eta_nf t2)"
 | "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(simp add: eqvt_def is_eta_nf_graph_aux_def)
 apply(rule TrueI)
 apply(rule_tac y="x" in lam.exhaust)
 apply(auto)[3]
@@ -120,7 +119,7 @@
   "var_pos y (Var x) = (if y = x then {[]} else {})"
 | "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(simp add: eqvt_def var_pos_graph_aux_def)
 apply(rule TrueI)
 apply(case_tac x)
 apply(rule_tac y="b" and c="a" in lam.strong_exhaust)
@@ -166,7 +165,7 @@
   "(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 ::== (App (Var y) s)])"
-  apply(simp add: eqvt_def subst'_graph_def)
+  apply(simp add: eqvt_def subst'_graph_aux_def)
   apply(rule TrueI)
   apply(case_tac x)
   apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust)
@@ -200,9 +199,7 @@
   "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)"
-  unfolding eqvt_def
-  unfolding frees_lst_graph_def
-apply(simp)
+apply(simp add: eqvt_def frees_lst_graph_aux_def)
 apply(rule TrueI)
 apply(rule_tac y="x" in lam.exhaust)
 using [[simproc del: alpha_lst]]
@@ -228,7 +225,7 @@
   "frees_set (Var x) = {atom x}"
 | "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(simp add: eqvt_def frees_set_graph_aux_def)
   apply(erule frees_set_graph.induct)
   apply(auto)[9]
   apply(rule_tac y="x" in lam.exhaust)
@@ -256,7 +253,7 @@
   "height (Var x) = 1"
 | "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(simp add: eqvt_def height_graph_aux_def)
   apply(rule TrueI)
   apply(rule_tac y="x" in lam.exhaust)
   using [[simproc del: alpha_lst]]
@@ -279,8 +276,7 @@
   "(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])"
-  unfolding eqvt_def subst_graph_def
-  apply(simp)
+  apply(simp add: eqvt_def subst_graph_aux_def)
   apply(rule TrueI)
   using [[simproc del: alpha_lst]]
   apply(auto)
@@ -468,7 +464,7 @@
   "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))"
-  apply (simp add: eqvt_def trans_graph_def)
+  apply (simp add: eqvt_def trans_graph_aux_def)
   apply (erule trans_graph.induct)
   apply (auto simp add: ln.fresh)[3]
   apply (simp add: supp_lookup_fresh)
@@ -503,7 +499,7 @@
   "cntlams (Var x) = 0"
 | "cntlams (App t1 t2) = (cntlams t1) + (cntlams t2)"
 | "cntlams (Lam [x]. t) = Suc (cntlams t)"
-  apply(simp add: eqvt_def cntlams_graph_def)
+  apply(simp add: eqvt_def cntlams_graph_aux_def)
   apply(rule TrueI)
   apply(rule_tac y="x" in lam.exhaust)
   apply(auto)[3]
@@ -530,7 +526,7 @@
   "cntbvs (Var x) xs = (if x \<in> set xs then 1 else 0)"
 | "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(simp add: eqvt_def cntbvs_graph_aux_def)
   apply(rule TrueI)
   apply(case_tac x)
   apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
@@ -589,8 +585,7 @@
 | "transdb (App t1 t2) xs = 
       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(simp)
+  apply(simp add: eqvt_def transdb_graph_aux_def)
   apply(rule TrueI)
   apply (case_tac x)
   apply (rule_tac y="a" and c="b" in lam.strong_exhaust)
@@ -651,7 +646,7 @@
 | "apply_subst (Var x) t2 = App (Var x) t2"
 | "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(simp add: eval_apply_subst_graph_aux_def eqvt_def)
   apply(rule TrueI)
   apply (case_tac x)
   apply (case_tac a rule: lam.exhaust)
@@ -703,8 +698,7 @@
   "atom c \<sharp> (x, M) \<Longrightarrow> q (Lam [x]. M) (N :: lam) = Lam [x]. (Lam [c]. (App M (q (Var c) N)))"
 | "q (Var x) N = Var x"
 | "q (App l r) N = App l r"
-unfolding eqvt_def q_graph_def
-apply (simp)
+apply(simp add: eqvt_def q_graph_aux_def)
 apply (rule TrueI)
 apply (case_tac x)
 apply (rule_tac y="a" in lam.exhaust)
@@ -732,7 +726,7 @@
 | "eqvt f \<Longrightarrow> map_term f (App t1 t2) = App (f t1) (f t2)"
 | "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 (simp add: eqvt_def map_term_graph_aux_def)
   apply(rule TrueI)
   apply (case_tac x, case_tac "eqvt a", case_tac b rule: lam.exhaust)
   using [[simproc del: alpha_lst]]
@@ -812,7 +806,7 @@
 where
   "Z (App M N) k = Z M (%m. (Z N (%n.(App m n))))"
 | "Z (App M N) k = Z M (%m. (Z N (%n.(App (App m n) (Abs b (k (Var b)))))))"
-unfolding eqvt_def Z_graph_def
+apply(simp add: eqvt_def Z_graph_aux_def)
 apply (rule, perm_simp, rule)
 oops
 
@@ -852,7 +846,7 @@
 | "aux (Lam [x].t) (App t1 t2) xs = False"
 | "\<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 (simp add: eqvt_def aux_graph_aux_def)
   apply(erule aux_graph.induct)
   apply(simp_all add: fresh_star_def pure_fresh)[9]
   apply(case_tac x)
@@ -899,8 +893,8 @@
 | "aux2 (Lam [x].t) (Var y) = False"
 | "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(simp)
+  apply(simp add: eqvt_def aux2_graph_aux_def)
+  apply(rule TrueI)
   apply(case_tac x)
   apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
   apply(rule_tac y="b" in lam.exhaust)