# HG changeset patch # User Cezary Kaliszyk # 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 \ xs \ 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 \ xs \ ab \ m \ \ 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 \ (b \ aba) \ m") + apply simp + by (metis (lifting) permute_flip_at) +lemma var_neq_swapequal2: "atom ab \ xs \ ab \ m \ \ 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 \ (aa \ aba) \ 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 \ 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 \ m = b") + apply (simp add: var_neq_swapequal2 fresh_at_base) apply simp -proof - - have "lookup n m xs = (fold (\(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) \ - lookup n m xs = (fold (\(x\name, y\name) t\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 (\(x\name, y\name) t\name. if n = t then y else t) xs n = m)" - using d by simp - then show "lookup n m (a # xs) = - (fold (\(x\name, y\name) t\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 (\(x\name, y\name) t\name. if n = t then y else t) xs n = m)" "a = (b, c)" - then show "lookup n m (a # xs) = (fold (\(x\name, y\name) t\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 (\(x, y) t. if n = t then y else t) xs n) = Var m)" by simp - also have "... = (foldr (\(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 \ x \ a \ y \ b \ x \ b \ y \ 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 \ atom x \ xs \ atom y \ 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 \ fst ` set xs \ x \ snd ` set xs \ y \ snd ` set xs \ y \ fst ` set xs") apply (simp) - apply (subst need) + apply (subst swapequal_lambda) apply auto[1] sorry