# HG changeset patch
# User Cezary Kaliszyk <cezarykaliszyk@gmail.com>
# Date 1333085803 -7200
# Node ID 57dcb5c0d5db73fe080ac67f4b27835980d1db29
# Parent  1da802bd2ab189f7085dd4145c77e79005484bef
Close some of the obvious subgoals in Aux

diff -r 1da802bd2ab1 -r 57dcb5c0d5db Nominal/Ex/AuxNoFCB.thy
--- a/Nominal/Ex/AuxNoFCB.thy	Fri Mar 30 07:15:24 2012 +0200
+++ b/Nominal/Ex/AuxNoFCB.thy	Fri Mar 30 07:36:43 2012 +0200
@@ -268,10 +268,55 @@
   apply simp
   apply simp
   apply simp
+  (* The last subgoal would be obvious if we'd define it with a recusor
+     and have eqvt for the function *)
   sorry
 
 termination (eqvt) by lexicographic_order
 
+lemma var_eq_swapequal: "atom ab \<sharp> xs \<Longrightarrow> swapequal (Var ab) (Var ab) xs"
+  apply (induct xs)
+  apply simp
+  apply (case_tac a)
+  apply (simp add: fresh_Cons)
+  apply (rule_tac x="(ab, aa, b, xs)" and ?'a="name" in obtain_fresh)
+  apply (subst swapequal.simps)
+  apply (simp add: fresh_Pair lam.fresh)
+  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"
+  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 (subst swapequal.simps)
+  apply (simp add: fresh_Pair lam.fresh)
+  apply auto[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 (subst swapequal.simps)
+  apply (simp add: fresh_Pair lam.fresh)
+  apply auto[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)
+
+
 lemma lookup_swapequal: "lookup n m xs = swapequal (Var n) (Var m) xs"
   apply (induct xs arbitrary: m n)
   apply simp
@@ -282,93 +327,23 @@
   apply (simp add: fresh_Pair lam.fresh fresh_Nil)
   apply (case_tac "n = aa \<and> m = b")
   apply simp
-  defer
+  apply (simp add: var_eq_swapequal fresh_Pair_elim)
   apply (case_tac "n = aa")
   apply (simp add: fresh_Pair_elim fresh_at_base)
-  defer
+  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
-  defer
-  apply simp
-  sorry
-
-(*
-lemma lookup_property:
-  assumes "distinct (map fst xs @ map snd xs)"
-  shows "aux (Var n) (Var m) xs = swapequal (Var n) (Var m) xs"
-  using assms
-  apply (induct xs arbitrary: n m)
-  apply simp
-  apply simp
-  apply (case_tac a)
-  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_Cons)
-  apply auto[1]
-
-  apply (case_tac "n = aa \<and> m = b")
+  apply (simp add: var_neq_swapequal2 fresh_at_base)
   apply simp
-proof -
-  have "lookup n m xs = (fold (\<lambda>(x, y) t. if n = t then y else t) xs n = m)"
-    using assms
-    proof (induct xs, simp)
-      fix a b xs
-      assume d: "distinct (map fst xs @ map snd xs) \<Longrightarrow>
-        lookup n m xs = (fold (\<lambda>(x\<Colon>name, y\<Colon>name) t\<Colon>name. if n = t then y else t) xs n = m)"
-      assume "distinct (map fst (a # xs) @ map snd (a # xs))"
-      then have "lookup n m xs = (fold (\<lambda>(x\<Colon>name, y\<Colon>name) t\<Colon>name. if n = t then y else t) xs n = m)"
-        using d by simp
-      then show "lookup n m (a # xs) =
-          (fold (\<lambda>(x\<Colon>name, y\<Colon>name) t\<Colon>name. if n = t then y else t) (a # xs) n = m)"
-        proof (cases a)
-          case (Pair b c)
-          assume "lookup n m xs = (fold (\<lambda>(x\<Colon>name, y\<Colon>name) t\<Colon>name. if n = t then y else t) xs n = m)" "a = (b, c)"
-          then show "lookup n m (a # xs) = (fold (\<lambda>(x\<Colon>name, y\<Colon>name) t\<Colon>name. if n = t then y else t) (a # xs) n = m)"
-            apply simp
-            apply auto
-            sledgehammer
-
-        apply -
-        apply (case_tac a)
-        apply auto
-
+  done
 
-    apply simp
-    apply (case_tac a)
-    apply simp
-    apply metis
-  also have "... = (Var (foldr (\<lambda>(x, y) t. if n = t then y else t) xs n) = Var m)" by simp
-  also have "... = (foldr (\<lambda>(x, y) t. subst t x (Var y)) xs (Var n) = Var m)"
-    apply (rule arg_cong) back
-    apply (induct xs)
-    apply simp
-    apply (case_tac a)
-    apply simp
-    apply auto
-    find_theorems "fold _ _ _ = fold _ _ _"
-    apply (induct xs) apply simp
-    apply simp
-  apply (case_tac a)
-  apply simp
-  apply (simp only: lookup.simps)
-  apply simp
-  apply clarify
-  apply (case_tac "n = aa")
-  apply (case_tac "m = ba")
-  apply simp
-  apply (induct_tac xs)
-  apply simp
-  apply simp
-  sorry*)
-
-lemma reord: "
+lemma swapequal_reorder: "
   a \<noteq> x \<Longrightarrow> a \<noteq> y \<Longrightarrow> b \<noteq> x \<Longrightarrow> b \<noteq> y \<Longrightarrow>
   swapequal t s ((x, y) # (a, b) # xs) = swapequal t s ((a, b) # (x, y) # xs)"
   sorry
 
-lemma need:
+lemma swapequal_lambda:
   assumes "distinct xs \<and> atom x \<sharp> xs \<and> atom y \<sharp> xs"
   shows "swapequal (Lam [x]. t) (Lam [y]. s) xs = swapequal t s ((x, y) # xs)"
   using assms
@@ -391,7 +366,7 @@
   apply clarify
   apply (simp add: fresh_Cons fresh_Pair fresh_at_base)
   apply clarify
-  apply (subst reord)
+  apply (subst swapequal_reorder)
   apply auto[4]
   apply (rule_tac x="(x, y, t, s, a, b, xs)" and ?'a="name" in obtain_fresh)
   apply (rename_tac f)
@@ -419,7 +394,7 @@
   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 need)
+  apply (subst swapequal_lambda)
   apply auto[1]
   sorry