# HG changeset patch
# User Cezary Kaliszyk <cezarykaliszyk@gmail.com>
# Date 1333116480 -7200
# Node ID 8a3352cff8d0a27f78903df1ca2336c3359517f2
# Parent  d24e704830516576c668beb2b67305b8976d7a11
More cleaning

diff -r d24e70483051 -r 8a3352cff8d0 Nominal/Ex/AuxNoFCB.thy
--- a/Nominal/Ex/AuxNoFCB.thy	Fri Mar 30 13:56:36 2012 +0200
+++ b/Nominal/Ex/AuxNoFCB.thy	Fri Mar 30 16:08:00 2012 +0200
@@ -44,6 +44,7 @@
   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)
+  unfolding fresh_star_def
   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")
@@ -60,26 +61,13 @@
   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>
-             atom y' \<sharp> (x', c, Lam [x']. t') \<longrightarrow>
-             Lam [name]. lam = Lam [x']. t' \<longrightarrow>
-             Lam [namea]. lama = Lam [y']. s' \<longrightarrow> b name lam namea lama = b x' t' y' s')
-  ")
+  apply (case_tac "(\<forall>x' y' t' s'. atom x' \<sharp> (c, Lam [y']. s') \<longrightarrow>
+             atom y' \<sharp> (x', c, Lam [x']. t') \<longrightarrow> Lam [name]. lam = Lam [x']. t' \<longrightarrow>
+             Lam [namea]. lama = Lam [y']. s' \<longrightarrow> b name lam namea lama = b x' t' y' s')")
   apply clarify
   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'.
-             atom x' \<sharp> (c, Lam [y']. s') \<longrightarrow>
-             atom y' \<sharp> (x', c, Lam [x']. t') \<longrightarrow>
-             Lam [name]. lam = Lam [x']. t' \<longrightarrow>
-             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)
+  apply (simp only: fresh_Pair_elim)
+  apply blast
   apply (simp_all)[53]
   apply clarify
   apply metis
@@ -98,18 +86,15 @@
   apply (rule_tac y="l2" and c="(name, xs, l)" in lam.strong_exhaust)
   apply auto[2]
   apply clarify
-  apply (case_tac "(\<forall>x' y' t' s'.
-              atom x' \<sharp> (xs, Lam [y']. s') \<longrightarrow>
-              atom y' \<sharp> (x', xs, Lam [x']. t') \<longrightarrow>
-              Lam [name]. lam = Lam [x']. t' \<longrightarrow>
-              Lam [namea]. lama = Lam [y']. s' \<longrightarrow>
-              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)
+  apply (case_tac "(\<forall>x' y' t' s'. atom x' \<sharp> (xs, Lam [y']. s') \<longrightarrow>
+    atom y' \<sharp> (x', xs, Lam [x']. t') \<longrightarrow> Lam [name]. lam = Lam [x']. t' \<longrightarrow>
+    Lam [namea]. lama = Lam [y']. s' \<longrightarrow> fll name lam namea lama = fll x' t' y' s')")
+  unfolding fresh_star_def
+  apply (subst lam2_rec.simps) apply simp
+  apply (subst lam2_rec.simps) apply simp
   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
+  apply (subst lam2_rec.simps(10)) apply (simp_all add: fresh_star_def)
   done
 
 nominal_primrec aux :: "lam \<Rightarrow> lam \<Rightarrow> (name \<times> name) list \<Rightarrow> bool"
@@ -144,7 +129,6 @@
   apply (subst aux.simps, simp)
   apply (subst aux.simps)
   apply (subst lam2_rec.simps)
-  prefer 2 apply rule
   apply (rule, simp add: lam.fresh)
   apply (rule, simp add: lam.fresh)
   apply (intro allI impI)
@@ -193,6 +177,7 @@
   apply (simp add: Abs1_eq_iff fresh_Pair_elim fresh_at_base swap_commute)
   apply (rule sym)
   apply (simp add: Abs1_eq_iff fresh_Pair_elim fresh_at_base swap_commute)
+  apply (rule refl)
   done
 
 lemma aux_induct:  "\<lbrakk>\<And>xs n m. P xs (Var n) (Var m); \<And>xs n l r. P xs (Var n) (App l r);
@@ -224,8 +209,7 @@
 | "atom x \<sharp> (l, r, hl, hr, t) \<Longrightarrow>
     swapequal l r ((hl, hr) # t) \<longleftrightarrow> swapequal ((hl \<leftrightarrow> x) \<bullet> l) ((hr \<leftrightarrow> x) \<bullet> r) t"
   unfolding eqvt_def swapequal_graph_def
-  apply (rule, perm_simp, rule)
-  apply(rule TrueI)
+  apply (rule, perm_simp, rule, rule TrueI)
   apply (case_tac x)
   apply (case_tac c)
   apply metis
@@ -262,58 +246,33 @@
   apply (simp add: fresh_Pair_elim)
   by (metis flip_at_base_simps(3) fresh_Pair fresh_at_base(2))
 
-lemma var_neq_swapequal: "atom ab \<sharp> xs \<Longrightarrow> ab \<noteq> m \<Longrightarrow> \<not> swapequal (Var ab) (Var m) xs"
+lemma var_neq_swapequal:
+  "atom ab \<sharp> xs \<Longrightarrow> ab \<noteq> m \<Longrightarrow> \<not> swapequal (Var ab) (Var m) xs"
+  "atom ab \<sharp> xs \<Longrightarrow> ab \<noteq> m \<Longrightarrow> \<not> swapequal (Var m) (Var ab) xs"
   apply (induct xs arbitrary: m)
-  apply simp
-  apply (case_tac a)
-  apply (simp add: fresh_Cons)
-  apply (rule_tac x="(ab, aa, b, m, xs)" and ?'a="name" in obtain_fresh)
+  apply simp_all[2]
+  apply (case_tac [!] a)
+  apply (simp_all add: fresh_Cons)
+  apply (rule_tac [!] x="(ab, aa, b, m, xs)" and ?'a="name" in obtain_fresh)
   apply (subst swapequal.simps)
-  apply (simp add: fresh_Pair lam.fresh)
-  apply auto[1]
+  apply (auto simp add: fresh_Pair lam.fresh)[1]
   apply (elim conjE)
-  apply (simp add: fresh_Pair_elim)
-  apply (simp add: flip_at_base_simps(3) fresh_Pair fresh_at_base(2))
-  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
-  apply (case_tac a)
-  apply (simp add: fresh_Cons)
-  apply (rule_tac x="(ab, aa, b, m, xs)" and ?'a="name" in obtain_fresh)
+  apply (simp add: fresh_Pair_elim fresh_at_base permute_flip_at)
   apply (subst swapequal.simps)
-  apply (simp add: fresh_Pair lam.fresh)
-  apply auto[1]
+  apply (auto simp add: fresh_Pair lam.fresh)[1]
   apply (elim conjE)
-  apply (simp add: fresh_Pair_elim)
-  apply (simp add: flip_at_base_simps(3) fresh_Pair fresh_at_base(2))
-  apply (subgoal_tac "ab \<noteq> (aa \<leftrightarrow> aba) \<bullet> m")
-  apply simp
-  by (metis (lifting) permute_flip_at)
+  apply (simp add: fresh_Pair_elim fresh_at_base permute_flip_at)
+  done
 
 lemma lookup_swapequal: "lookup n m xs = swapequal (Var n) (Var m) xs"
   apply (induct xs arbitrary: m n)
   apply simp
   apply (case_tac a)
+  apply (rule_tac x="(n, m, aa, b, xs)" and ?'a="name" in obtain_fresh)
   apply simp
-  apply (rule_tac x="(n, m, aa, b, xs)" and ?'a="name" in obtain_fresh)
   apply (subst swapequal.simps)
   apply (simp add: fresh_Pair lam.fresh fresh_Nil)
-  apply (case_tac "n = aa \<and> m = b")
-  apply simp
-  apply (simp add: var_eq_swapequal fresh_Pair_elim)
-  apply (case_tac "n = aa")
-  apply (simp add: fresh_Pair_elim fresh_at_base)
-  apply (simp add: var_neq_swapequal fresh_Pair_elim)
-  apply (simp add: fresh_Pair_elim fresh_at_base flip_def)
-  apply (case_tac "m = b")
-  apply simp
-  apply (simp add: var_neq_swapequal2 fresh_at_base)
-  apply simp
-  done
+  by (metis (hide_lams, mono_tags) flip_at_base_simps(3) flip_at_simps(1) fresh_Pair fresh_at_base(2) lam.perm_simps(1) var_eq_swapequal var_neq_swapequal(1) var_neq_swapequal(2))
 
 lemma swapequal_reorder: "
   a \<noteq> x \<Longrightarrow> a \<noteq> y \<Longrightarrow> b \<noteq> x \<Longrightarrow> b \<noteq> y \<Longrightarrow>
@@ -363,33 +322,25 @@
   apply (subgoal_tac "[[atom y]]lst. s = [[atom a]]lst. ((y \<leftrightarrow> a) \<bullet> s)")
   apply simp
   apply (simp add: Abs1_eq_iff)
-  apply (auto simp add: Abs1_eq_iff flip_def fresh_at_base)[1]
+  apply (auto simp add: Abs1_eq_iff flip_def fresh_at_base)[2]
   apply (smt atom_eqvt eq_eqvt flip_at_simps(2) flip_def fresh_eqvt)
-  apply (simp add: Abs1_eq_iff)
-  apply (auto simp add: Abs1_eq_iff flip_def fresh_at_base)[1]
   apply (smt atom_eqvt eq_eqvt flip_at_simps(2) flip_def fresh_eqvt)
   apply clarify
   apply (simp add: fresh_Cons fresh_Pair fresh_at_base)
   apply clarify
-  apply (subst swapequal_reorder)
-  apply auto[4]
+  apply (simp add: swapequal_reorder)
   apply (rule_tac x="(x, y, t, s, a, b, xs)" and ?'a="name" in obtain_fresh)
   apply (rename_tac f)
   apply (subst (2) swapequal.simps)
-  apply (simp add: lam.fresh fresh_Pair fresh_at_base fresh_Cons)
-  apply auto[1]
+  apply (auto simp add: lam.fresh fresh_Pair fresh_at_base fresh_Cons)[1]
   apply (subst swapequal.simps)
-  apply (simp add: lam.fresh fresh_Pair fresh_at_base fresh_Cons)
-  apply auto[1]
-  apply simp
-  apply (simp add: flip_def)
-  apply (simp add: fresh_Pair_elim fresh_at_base)
+  apply (auto simp add: lam.fresh fresh_Pair fresh_at_base fresh_Cons)[1]
+  apply (simp add: flip_def fresh_Pair_elim fresh_at_base)
   done
 
 lemma distinct_swapequal: "\<forall>p q. p \<bullet> l \<noteq> q \<bullet> r \<Longrightarrow> \<not>swapequal l r xs"
   apply (induct xs rule:swapequal.induct)
-  apply simp
-  apply metis
+  apply auto[1]
   apply (simp add: fresh_Pair_elim)
   apply (subgoal_tac "\<forall>(p\<Colon>perm) q\<Colon>perm. p \<bullet> (hl \<leftrightarrow> x) \<bullet> l \<noteq> q \<bullet> (hr \<leftrightarrow> x) \<bullet> r")
   apply simp
@@ -406,9 +357,8 @@
   apply simp
   apply (rule_tac x="(l1, l2, r1, r2, aa, b, xs)" and ?'a="name" in obtain_fresh)
   apply (simp add: fresh_Pair_elim)
-  apply (subst swapequal.simps) apply (simp add: fresh_Pair) apply auto[1]
-  apply (subst swapequal.simps) apply (simp add: fresh_Pair lam.fresh) apply auto[1]
-  apply simp
+  apply (subst swapequal.simps) apply (auto simp add: fresh_Pair)[1]
+  apply (subst swapequal.simps) apply (auto simp add: fresh_Pair lam.fresh)
   done
 
 lemma [simp]: "distinct (map fst xs) \<Longrightarrow> distinct xs"
@@ -429,19 +379,14 @@
   using assms
   apply (induct xs x y rule: aux_induct)
   apply (simp add: lookup_swapequal)
-  apply (simp, rule distinct_swapequal, simp)
-  apply (simp, rule distinct_swapequal, simp)
-  apply (simp, rule distinct_swapequal, simp)
+  apply (simp, rule distinct_swapequal, simp)+
   apply (simp add: swapequal_app)
-  apply (simp, rule distinct_swapequal, simp)
-  apply (simp, rule distinct_swapequal, simp)
-  apply (simp, rule distinct_swapequal, simp)
-  apply (simp add: fresh_Pair_elim lam.fresh fresh_at_base)
+  apply (simp, rule distinct_swapequal, simp)+
+  apply (simp add: fresh_Pair_elim lam.fresh fresh_at_base conjE)
   apply (elim conjE)
   apply (simp add: fresh_Pair_elim lam.fresh fresh_at_base)
   apply (subgoal_tac "x \<notin> fst ` set xs \<and>
         x \<notin> snd ` set xs \<and> y \<notin> snd ` set xs \<and> y \<notin> fst ` set xs")
-  apply (simp)
   apply (subst swapequal_lambda)
   apply auto[2]
   apply simp