# HG changeset patch
# User Cezary Kaliszyk <cezarykaliszyk@gmail.com>
# Date 1333084524 -7200
# Node ID 1da802bd2ab189f7085dd4145c77e79005484bef
# Parent  4d01d1056e2262605883b2121e396d41ad8ff7c9
Correct Aux and proof sketch that it's same as alpha-equality, following Dan Synek's proof.

diff -r 4d01d1056e22 -r 1da802bd2ab1 Nominal/Ex/AuxNoFCB.thy
--- a/Nominal/Ex/AuxNoFCB.thy	Thu Mar 29 10:37:41 2012 +0200
+++ b/Nominal/Ex/AuxNoFCB.thy	Fri Mar 30 07:15:24 2012 +0200
@@ -7,8 +7,18 @@
 | App "lam" "lam"
 | Lam x::"name" l::"lam"  binds x in l ("Lam [_]. _" [100, 100] 100)
 
+nominal_primrec lookup where
+  "lookup (n :: name) m [] \<longleftrightarrow> (n = m)"
+| "lookup n m ((hn, hm) # t) \<longleftrightarrow>
+     (n, m) = (hn, hm) \<or> (n \<noteq> hn \<and> m \<noteq> hm \<and> lookup n m t)"
+  apply (simp add: eqvt_def lookup_graph_def)
+  apply (rule, perm_simp, rule, rule)
+  by pat_completeness auto
+
+termination (eqvt) by lexicographic_order
+
 nominal_primrec lam2_rec where
-  "lam2_rec faa fll xs (Var n) (Var m) = (n = m \<or> (n, m) \<in> set xs)"
+  "lam2_rec faa fll xs (Var n) (Var m) = lookup n m xs"
 | "lam2_rec faa fll xs (Var n) (App l r) = False"
 | "lam2_rec faa fll xs (Var n) (Lam [x]. t) = False"
 | "lam2_rec faa fll xs (App l r) (Var n) = False"
@@ -118,7 +128,7 @@
   by (relation "measure (\<lambda>(l, r, xs). size l + size r)") simp_all
 
 lemma aux_simps[simp]:
-  "aux (Var x) (Var y) xs = (x = y \<or> (x, y) \<in> set xs)"
+  "aux (Var x) (Var y) xs = lookup x y xs"
   "aux (App t1 t2) (App s1 s2) xs = (aux t1 s1 xs \<and> aux t2 s2 xs)"
   "aux (Var x) (App t1 t2) xs = False"
   "aux (Var x) (Lam [y].t) xs = False"
@@ -212,6 +222,211 @@
   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>
+    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 (case_tac x)
+  apply (case_tac c)
+  apply metis
+  apply (case_tac aa)
+  apply (rename_tac l r lst h t hl hr)
+  apply (rule_tac x="(l, r, hl, hr, t)" and ?'a="name" in obtain_fresh)
+  apply simp
+  apply simp
+  apply simp
+  sorry
+
+termination (eqvt) by lexicographic_order
+
+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 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
+  defer
+  apply (case_tac "n = aa")
+  apply (simp add: fresh_Pair_elim fresh_at_base)
+  defer
+  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
+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
+
+
+    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: "
+  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:
+  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
+  apply (induct xs arbitrary: t s x y)
+  apply (rule_tac x="(x, y, t, s)" and ?'a="name" in obtain_fresh)
+  apply (simp add: fresh_Pair_elim fresh_Nil)
+  apply (subst swapequal.simps)
+  apply (simp add: fresh_Pair fresh_Nil)
+  apply auto[1]
+  apply simp
+  apply (subgoal_tac "[[atom x]]lst. t = [[atom a]]lst. ((x \<leftrightarrow> a) \<bullet> t)")
+  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 (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 reord)
+  apply auto[4]
+  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 (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)
+  done
+
+lemma aux_alphaish:
+  assumes "distinct (map fst xs @ map snd xs)"
+  shows "aux x y xs \<longleftrightarrow> swapequal x y xs"
+  using assms
+  apply (induct xs x y rule: aux_induct)
+  apply (simp add: lookup_swapequal)
+  prefer 8
+  apply (simp add: fresh_Pair_elim lam.fresh fresh_at_base)
+  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 need)
+  apply auto[1]
+  sorry
+
+lemma
+  "aux x y [] \<longleftrightarrow> (x = y)"
+  by (simp_all add: supp_Nil aux_alphaish)
+
 end
 
 
diff -r 4d01d1056e22 -r 1da802bd2ab1 Nominal/Ex/SubstNoFcb.thy
--- a/Nominal/Ex/SubstNoFcb.thy	Thu Mar 29 10:37:41 2012 +0200
+++ b/Nominal/Ex/SubstNoFcb.thy	Fri Mar 30 07:15:24 2012 +0200
@@ -65,7 +65,7 @@
   shows "\<lbrakk>a \<sharp> x; a \<sharp> y; a \<sharp> z\<rbrakk> \<Longrightarrow> a \<sharp> f x y z"
   using fresh_fun_eqvt_app[OF e] fresh_fun_app by (metis (lifting, full_types))
 
-lemma
+lemma substr_simps:
   "substr (Var x) y s = (if x = y then s else (Var x))"
   "substr (App t1 t2) y s = App (substr t1 y s) (substr t2 y s)"
   "atom x \<sharp> (y, s) \<Longrightarrow> substr (Lam [x]. t) y s = Lam [x]. (substr t y s)"