*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] remdups_adj crucial lemma*From*: Lars Noschinski <noschinl at in.tum.de>*Date*: Tue, 26 Aug 2014 11:40:45 +0200*In-reply-to*: <8AB4B04F-1094-40B5-95CE-FC5C11211069@uibk.ac.at>*References*: <CALFc0GDzE9KjEFmmQamP8NF7Jt_oW2q8NQX1FhT=YOSrGhMQbA@mail.gmail.com> <53FB4308.9020302@in.tum.de> <CALFc0GBRLHGyVO11PNTn_sB3+A4=fsMd9UYJD3dyOucV+hTcag@mail.gmail.com> <53FB8B1C.8040003@in.tum.de> <8AB4B04F-1094-40B5-95CE-FC5C11211069@uibk.ac.at>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Icedove/24.6.0

On 26.08.2014 10:05, René Thiemann wrote: > Dear all, > >> It seems to me that we need an abstract nonrecursive characterisation of >> remdups_adj from which specific lemmas follow easily. Is the following correct? >> >> remdups_adj xs = ys <-> >> EX f::nat => nat. mono f & f ` {0 ..< size xs} = {0 ..< size ys} >> & (ALL i < size xs. xs!i = ys!(f i) >> & (xs!i = xs!(i+1) <-> f i = f(i+1))) >> It should be sound (-->), but is it complete (<--)? > At least there needs to be one more implication added, since > otherwise the reference to xs!(i+1) is critical. > > remdups_adj xs = ys <-> > EX f::nat => nat. mono f & f ` {0 ..< size xs} = {0 ..< size ys} > & (ALL i < size xs. xs!i = ys!(f i) > & (i + 1 < size xs --> (xs!i = xs!(i+1) <-> f i = f(i+1)))) > > Otherwise, it looks good (soundness and completeness can easily be proven > for lists upto length 1, but the inductive case became quite tedious in my proof attempt) I've got a (lenghty, but otherwise straightforward) proof of completeness for the modified theorem.

theory Scratch imports Main begin lemma "(\<exists>f :: nat \<Rightarrow> nat. mono f \<and> f ` {0 ..< size xs} = {0 ..< size ys} \<and> (\<forall>i < size xs. xs!i = ys! (f i)) \<and> (\<forall>i. i + 1 < size xs \<longrightarrow> (xs!i = xs!(i+1) \<longleftrightarrow> f i = f(i+1)))) \<Longrightarrow> remdups_adj xs = ys" proof (induct xs arbitrary: ys rule: remdups_adj.induct) case 1 then show ?case by auto next case (2 x) then obtain f where f_img: "f ` {0 ..< size [x]} = {0 ..< size ys}" and f_nth: "\<And>i. i < size [x] \<Longrightarrow> [x]!i = ys!(f i)" by metis have "length ys = card (f ` {0 ..< size [x]})" using f_img by auto then have "length ys = 1" by auto moreover then have "f 0 = 0" using f_img by auto ultimately show ?case using f_nth by (cases ys) auto next case (3 x1 x2 xs) from "3.prems" obtain f where f_mono: "mono f" and f_img: "f ` {0..<length (x1 # x2 # xs)} = {0..<length ys}" and f_nth1: "\<And>i. i < length (x1 # x2 # xs) \<Longrightarrow> (x1 # x2 # xs) ! i = ys ! f i" and f_nth2: "\<And>i. i + 1 < length (x1 # x2 #xs) \<Longrightarrow> ((x1 # x2 # xs) ! i = (x1 # x2 # xs) ! (i + 1)) = (f i = f (i + 1))" by metis show ?case proof cases assume "x1 = x2" let ?f' = "f o Suc" have "remdups_adj (x1 # xs) = ys" proof (intro "3.hyps" exI conjI impI allI) show "x1 = x2" by fact next show "mono ?f'" using f_mono by (simp add: mono_iff_le_Suc) next have "?f' ` {0 ..< length (x1 # xs)} = f ` {Suc 0 ..< length (x1 # x2 # xs)}" by safe (fastforce, rename_tac x, case_tac x, auto) also have "\<dots> = f ` {0 ..< length (x1 # x2 # xs)}" proof - have "f 0 = f (Suc 0)" using \<open>x1 = x2\<close> f_nth2[of 0] by simp then show ?thesis by safe (fastforce, rename_tac x, case_tac x, auto) qed also have "\<dots> = {0 ..< length ys}" by fact finally show "?f' ` {0 ..< length (x1 # xs)} = {0 ..< length ys}" . next fix i assume "i < length (x1 # xs)" then show "(x1 # xs) ! i = ys ! ?f' i" using f_nth1[of "Suc i"] \<open>x1 = x2\<close> by simp next fix i assume "i + 1 < length (x1 # xs)" then show "((x1 # xs) ! i = (x1 # xs) ! (i + 1)) = (?f' i = ?f' (i + 1))" using f_nth2[of "Suc i"] \<open>x1 = x2\<close> by simp_all qed then show ?thesis using \<open>x1 = x2\<close> by simp next assume "x1 \<noteq> x2" then have "f 0 \<noteq> f (Suc 0)" using f_nth2[of 0] by auto have "2 \<le> length ys" proof - have "2 = card {f 0, f 1}" using \<open>f 0 \<noteq> _\<close> by simp also have "\<dots> \<le> card (f ` ({0, 1} \<union> {2..< Suc (Suc (length xs))}))" (is "_ \<le> card (f ` ?S)") by (rule card_mono) auto also have "?S = {0..<Suc (Suc (length xs))}" by auto also have "card (f ` \<dots>) = length ys" using f_img by simp finally show "2 \<le> length ys" . qed have "f 0 = 0" proof (rule ccontr) assume "f 0 \<noteq> 0" then have "\<And>i. 0 \<noteq> f i" using f_mono by (metis le0 le_0_eq monoD) then have "0 \<notin> f ` {0 ..< length (x1 # x2 # xs)}" by (auto simp del: neq0_conv) then show False using f_img by auto qed have "f (Suc 0) = Suc 0" proof (rule ccontr) assume "f (Suc 0) \<noteq> Suc 0" then have "Suc 0 < f (Suc 0)" using f_nth2[of 0] \<open>x1 \<noteq> x2\<close> \<open>f 0 = 0\<close> by auto then have "\<And>i. Suc 0 < f (Suc i)" using f_mono by (metis Suc_le_mono le0 less_le_trans monoD) then have "\<And>i. Suc 0 \<noteq> f i" using \<open>f 0 = 0\<close> by (metis less_irrefl_nat not0_implies_Suc) then have "Suc 0 \<notin> f ` {0 ..< length (x1 # x2 # xs)}" by auto then show False using f_img \<open>2 \<le> length ys\<close> by auto qed obtain ys' where "ys = x1 # x2 # ys'" using \<open>2 \<le> length ys\<close> f_nth1[of 0] f_nth1[of 1] apply (cases ys) apply (rename_tac [2] ys', case_tac [2] ys') by (auto simp: \<open>f 0 = 0\<close> \<open>f (Suc 0) = Suc 0\<close>) def f' \<equiv> "\<lambda>x. f (Suc x) - 1" { fix i have "Suc 0 \<le> f (Suc 0)" using f_nth2[of 0] \<open>x1 \<noteq> x2\<close> \<open>f 0 = 0\<close> by auto also have "\<dots> \<le> f (Suc i)" using f_mono by (rule monoD) arith finally have "Suc 0 \<le> f (Suc i)" . } note X = this { fix i have "f (Suc i) = Suc (f' i)" using X[of i] by (auto simp: f'_def) } note f_Suc = this have "remdups_adj (x2 # xs) = (x2 # ys')" proof (intro "3.hyps" exI conjI impI allI) show "x1 \<noteq> x2" by fact next show "mono f'" using X f_mono by (auto simp: f'_def mono_iff_le_Suc le_diff_iff) next have "f' ` {0 ..< length (x2 # xs)} = (\<lambda>x. f x - 1) ` {0 ..< length (x1 # x2 #xs)}" apply safe apply (rename_tac [!] n, case_tac [!] n) apply (auto simp: f'_def \<open>f 0 = 0\<close> \<open>f (Suc 0) = Suc 0\<close> intro: rev_image_eqI) done also have "\<dots> = (\<lambda>x. x - 1) ` f ` {0 ..< length (x1 # x2 #xs)}" by (auto simp: image_comp) also have "\<dots> = (\<lambda>x. x - 1) ` {0 ..< length ys}" by (simp only: f_img) also have "\<dots> = {0 ..< length (x2 # ys')}" using \<open>ys = _\<close> by (fastforce intro: rev_image_eqI) finally show "f' ` {0 ..< length (x2 # xs)} = {0 ..< length (x2 # ys')}" . next fix i assume "i < length (x2 # xs)" then show "(x2 # xs) ! i = (x2 # ys') ! f' i" using f_nth1[of "Suc i"] \<open>x1 \<noteq> x2\<close> f_Suc by (simp add: \<open>ys = _\<close>) next fix i assume "i + 1 < length (x2 # xs)" then show "((x2 # xs) ! i = (x2 # xs) ! (i + 1)) = (f' i = f' (i + 1))" using f_nth2[of "Suc i"] \<open>x1 \<noteq> x2\<close> f_Suc by (auto simp: \<open>ys = _\<close>) qed then show ?case using \<open>ys = _\<close> \<open>x1 \<noteq> x2\<close> by simp qed qed end

**Follow-Ups**:**Re: [isabelle] remdups_adj crucial lemma***From:*René Thiemann

**References**:**[isabelle] remdups_adj crucial lemma***From:*Jakob von Raumer

**Re: [isabelle] remdups_adj crucial lemma***From:*Tobias Nipkow

**Re: [isabelle] remdups_adj crucial lemma***From:*Jakob von Raumer

**Re: [isabelle] remdups_adj crucial lemma***From:*Tobias Nipkow

**Re: [isabelle] remdups_adj crucial lemma***From:*René Thiemann

- Previous by Date: Re: [isabelle] RC4: sledgehammer on Cygwin crashed once; temp file not removed
- Next by Date: Re: [isabelle] Finite product simplification
- Previous by Thread: Re: [isabelle] remdups_adj crucial lemma
- Next by Thread: Re: [isabelle] remdups_adj crucial lemma
- Cl-isabelle-users August 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list