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