--- 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