# HG changeset patch
# User Cezary Kaliszyk <cezarykaliszyk@gmail.com>
# Date 1333108596 -7200
# Node ID d24e704830516576c668beb2b67305b8976d7a11
# Parent  556fcd0e5fcb724046bd0c5ab6db41152e6be8fe
Clean the proof of Aux

diff -r 556fcd0e5fcb -r d24e70483051 Nominal/Ex/AuxNoFCB.thy
--- a/Nominal/Ex/AuxNoFCB.thy	Fri Mar 30 13:39:15 2012 +0200
+++ b/Nominal/Ex/AuxNoFCB.thy	Fri Mar 30 13:56:36 2012 +0200
@@ -36,22 +36,14 @@
      lam2_rec faa fll xs (Lam [x]. t) (Lam [y]. s) = False"
   apply (simp add: eqvt_def lam2_rec_graph_def)
   apply (rule, perm_simp, rule, rule)
-  defer
-  apply (simp_all)[53]
-  apply clarify
-  apply metis
-  apply simp
   apply (case_tac x)
   apply (rule_tac y="d" and c="(c, e)" in lam.strong_exhaust)
   apply (rule_tac y="e" and c="(c, d)" in lam.strong_exhaust)
-  apply simp_all[3]
-  apply (metis, metis, metis)
+  apply simp_all[3]  apply (metis, metis, metis)
   apply (rule_tac y="e" and c="(c, d)" in lam.strong_exhaust)
-  apply simp_all[3]
-  apply (metis, metis, metis)
+  apply simp_all[3]  apply (metis, metis, metis)
   apply (rule_tac y="e" and c="(name, c, d)" in lam.strong_exhaust)
-  apply simp_all[2]
-  apply (metis, metis)
+  apply simp_all[2]  apply (metis, metis)
   apply (thin_tac "\<And>faa fll xs n m. x = (faa, fll, xs, Var n, Var m) \<Longrightarrow> P")
   apply (thin_tac "\<And>faa fll xs n l r. x = (faa, fll, xs, Var n, App l r) \<Longrightarrow> P")
   apply (thin_tac "\<And>faa fll xs n xa t. x = (faa, fll, xs, Var n, Lam [xa]. t) \<Longrightarrow> P")
@@ -68,6 +60,7 @@
   apply (drule_tac x="lam" in meta_spec)+
   apply (drule_tac x="b" in meta_spec)+
   apply (drule_tac x="a" in meta_spec)+
+  unfolding fresh_star_def
   apply (case_tac "
 (\<forall>x' y' t' s'.
              atom x' \<sharp> (c, Lam [y']. s') \<longrightarrow>
@@ -76,7 +69,7 @@
              Lam [namea]. lama = Lam [y']. s' \<longrightarrow> b name lam namea lama = b x' t' y' s')
   ")
   apply clarify
-  apply (simp add: fresh_star_def)
+  apply (simp)
   apply (thin_tac "\<lbrakk>atom name \<sharp> (c, Lam [namea]. lama) \<and>
          atom namea \<sharp> (name, c, Lam [name]. lam) \<and>
          (\<forall>x' y' t' s'.
@@ -86,7 +79,11 @@
              Lam [namea]. lama = Lam [y']. s' \<longrightarrow> b name lam namea lama = b x' t' y' s');
          x = (a, b, c, Lam [name]. lam, Lam [namea]. lama)\<rbrakk>
         \<Longrightarrow> P")
-  apply (simp add: fresh_star_def)
+  apply (simp)
+  apply (simp_all)[53]
+  apply clarify
+  apply metis
+  apply simp
   done
 
 termination (eqvt) by lexicographic_order
@@ -109,7 +106,7 @@
               fll name lam namea lama = fll x' t' y' s')")
   apply (subst lam2_rec.simps) apply (simp add: fresh_star_def)
   apply (subst lam2_rec.simps) apply (simp add: fresh_star_def)
-  using Abs1_eq_iff lam.eq_iff apply metis
+  apply metis
   apply (subst lam2_rec.simps(10)) apply (simp add: fresh_star_def)
   apply (subst lam2_rec.simps(10)) apply (simp add: fresh_star_def)
   apply rule
@@ -222,36 +219,6 @@
   apply lexicographic_order
   done
 
-lemma foldr_eqvt[eqvt]:
-  "p \<bullet> foldr a b c = foldr (p \<bullet> a) (p \<bullet> b) (p \<bullet> c)"
-  apply (induct b)
-  apply simp_all
-  apply (perm_simp)
-  apply simp
-  done
-
-nominal_primrec
-  subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::= _]" [90, 90, 90] 90)
-where
-  "(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 (rule, perm_simp, rule)
-  apply(rule TrueI)
-  apply(auto)
-  apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)
-  apply(blast)+
-  apply(simp_all add: fresh_star_def fresh_Pair_elim)
-  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)
-done
-
-termination (eqvt) by lexicographic_order
-
 nominal_primrec swapequal :: "lam \<Rightarrow> lam \<Rightarrow> (name \<times> name) list \<Rightarrow> bool" where
   "swapequal l r [] \<longleftrightarrow> l = r"
 | "atom x \<sharp> (l, r, hl, hr, t) \<Longrightarrow>
@@ -310,6 +277,7 @@
   apply (subgoal_tac "ab \<noteq> (b \<leftrightarrow> aba) \<bullet> m")
   apply simp
   by (metis (lifting) permute_flip_at)
+
 lemma var_neq_swapequal2: "atom ab \<sharp> xs \<Longrightarrow> ab \<noteq> m \<Longrightarrow> \<not> swapequal (Var m) (Var ab) xs"
   apply (induct xs arbitrary: m)
   apply simp
@@ -326,7 +294,6 @@
   apply simp
   by (metis (lifting) permute_flip_at)
 
-
 lemma lookup_swapequal: "lookup n m xs = swapequal (Var n) (Var m) xs"
   apply (induct xs arbitrary: m n)
   apply simp
@@ -358,8 +325,6 @@
   apply (subst swapequal.simps)
   apply (auto simp add: fresh_Pair fresh_Cons fresh_at_base)[1]
   apply (subgoal_tac "(x \<leftrightarrow> f) \<bullet> atom g \<sharp> t")
-  prefer 2
-  apply (simp add: flip_at_base_simps fresh_at_base flip_def)
   apply (subst swapequal.simps)
   apply (simp add: fresh_Pair fresh_Cons fresh_permute_left)
   apply rule apply assumption
@@ -372,15 +337,15 @@
   apply (subst swapequal.simps)
   apply (simp add: fresh_Pair fresh_Cons fresh_at_base fresh_permute_left)
   apply (subgoal_tac "(a \<leftrightarrow> g) \<bullet> atom f \<sharp> t")
-  prefer 2
+  apply rule apply assumption
   apply (simp add: flip_at_base_simps fresh_at_base flip_def)
-  apply rule apply assumption
   apply (simp add: flip_at_base_simps fresh_at_base flip_def)
   apply (subgoal_tac "(a \<leftrightarrow> g) \<bullet> (x \<leftrightarrow> f) \<bullet> t = (x \<leftrightarrow> f) \<bullet> (a \<leftrightarrow> g) \<bullet> t")
   apply (subgoal_tac "(b \<leftrightarrow> g) \<bullet> (y \<leftrightarrow> f) \<bullet> s = (y \<leftrightarrow> f) \<bullet> (b \<leftrightarrow> g) \<bullet> s")
   apply simp
   apply (smt flip_at_base_simps(3) flip_at_simps(1) flip_eqvt permute_eqvt)
   apply (smt flip_at_base_simps(3) flip_at_simps(1) flip_eqvt permute_eqvt)
+  apply (simp add: flip_at_base_simps fresh_at_base flip_def)
   done
 
 lemma swapequal_lambda:
@@ -482,7 +447,7 @@
   apply simp
   done
 
-lemma
+lemma aux_is_alpha:
   "aux x y [] \<longleftrightarrow> (x = y)"
   by (simp_all add: supp_Nil aux_alphaish)
 
diff -r 556fcd0e5fcb -r d24e70483051 Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Fri Mar 30 13:39:15 2012 +0200
+++ b/Nominal/Nominal2_Base.thy	Fri Mar 30 13:56:36 2012 +0200
@@ -1002,6 +1002,14 @@
   unfolding Inter_eq 
   by (perm_simp) (rule refl)
 
+lemma foldr_eqvt[eqvt]:
+  "p \<bullet> foldr a b c = foldr (p \<bullet> a) (p \<bullet> b) (p \<bullet> c)"
+  apply (induct b)
+  apply simp_all
+  apply (perm_simp)
+  apply simp
+  done
+
 (* FIXME: eqvt attribute *)
 lemma Sigma_eqvt:
   shows "(p \<bullet> (X \<times> Y)) = (p \<bullet> X) \<times> (p \<bullet> Y)"
diff -r 556fcd0e5fcb -r d24e70483051 Nominal/Nominal2_Base_Exec.thy
--- a/Nominal/Nominal2_Base_Exec.thy	Fri Mar 30 13:39:15 2012 +0200
+++ b/Nominal/Nominal2_Base_Exec.thy	Fri Mar 30 13:56:36 2012 +0200
@@ -929,6 +929,14 @@
   unfolding Inter_eq 
   by (perm_simp) (rule refl)
 
+lemma foldr_eqvt[eqvt]:
+  "p \<bullet> foldr a b c = foldr (p \<bullet> a) (p \<bullet> b) (p \<bullet> c)"
+  apply (induct b)
+  apply simp_all
+  apply (perm_simp)
+  apply simp
+  done
+
 (* FIXME: eqvt attribute *)
 lemma Sigma_eqvt:
   shows "(p \<bullet> (X \<times> Y)) = (p \<bullet> X) \<times> (p \<bullet> Y)"