equal
deleted
inserted
replaced
983 have a: "\<lbrakk>xs = [] \<Longrightarrow> thesis; \<And>x ys. \<lbrakk>\<not> List.member ys x; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis" |
983 have a: "\<lbrakk>xs = [] \<Longrightarrow> thesis; \<And>x ys. \<lbrakk>\<not> List.member ys x; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis" |
984 by (rule Cons(1)) |
984 by (rule Cons(1)) |
985 have b: "\<And>x' ys'. \<lbrakk>\<not> List.member ys' x'; a # xs \<approx> x' # ys'\<rbrakk> \<Longrightarrow> thesis" by fact |
985 have b: "\<And>x' ys'. \<lbrakk>\<not> List.member ys' x'; a # xs \<approx> x' # ys'\<rbrakk> \<Longrightarrow> thesis" by fact |
986 have c: "xs = [] \<Longrightarrow> thesis" using b |
986 have c: "xs = [] \<Longrightarrow> thesis" using b |
987 apply(simp) |
987 apply(simp) |
988 by (metis List.set_simps(1) emptyE empty_subsetI) |
988 by (metis list.set(1) emptyE empty_subsetI) |
989 have "\<And>x ys. \<lbrakk>\<not> List.member ys x; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis" |
989 have "\<And>x ys. \<lbrakk>\<not> List.member ys x; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis" |
990 proof - |
990 proof - |
991 fix x :: 'a |
991 fix x :: 'a |
992 fix ys :: "'a list" |
992 fix ys :: "'a list" |
993 assume d:"\<not> List.member ys x" |
993 assume d:"\<not> List.member ys x" |