simpler proof
authorblanchet
Wed Sep 24 15:45:55 2014 +0200 (2014-09-24)
changeset 58425246985c6b20b
parent 58424 cbbba613b6ab
child 58426 cac802846ff1
simpler proof
src/HOL/Library/Multiset.thy
     1.1 --- a/src/HOL/Library/Multiset.thy	Wed Sep 24 11:09:05 2014 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Wed Sep 24 15:45:55 2014 +0200
     1.3 @@ -128,7 +128,7 @@
     1.4  
     1.5  lift_definition minus_multiset :: "'a multiset => 'a multiset => 'a multiset" is "\<lambda> M N. \<lambda>a. M a - N a"
     1.6  by (rule diff_preserves_multiset)
     1.7 - 
     1.8 +
     1.9  instance
    1.10  by default (transfer, simp add: fun_eq_iff)+
    1.11  
    1.12 @@ -156,7 +156,7 @@
    1.13  lemma diff_add:
    1.14    "(M::'a multiset) - (N + Q) = M - N - Q"
    1.15    by (rule sym) (fact diff_diff_add)
    1.16 -  
    1.17 +
    1.18  lemma insert_DiffM:
    1.19    "x \<in># M \<Longrightarrow> {#x#} + (M - {#x#}) = M"
    1.20    by (clarsimp simp: multiset_eq_iff)
    1.21 @@ -242,7 +242,7 @@
    1.22    qed
    1.23  qed
    1.24  
    1.25 -lemma insert_noteq_member: 
    1.26 +lemma insert_noteq_member:
    1.27    assumes BC: "B + {#b#} = C + {#c#}"
    1.28     and bnotc: "b \<noteq> c"
    1.29    shows "c \<in># B"
    1.30 @@ -262,14 +262,14 @@
    1.31    "x \<in># M \<Longrightarrow> \<exists>A. M = A + {#x#}"
    1.32    by (rule_tac x = "M - {#x#}" in exI, simp)
    1.33  
    1.34 -lemma multiset_add_sub_el_shuffle: 
    1.35 -  assumes "c \<in># B" and "b \<noteq> c" 
    1.36 +lemma multiset_add_sub_el_shuffle:
    1.37 +  assumes "c \<in># B" and "b \<noteq> c"
    1.38    shows "B - {#c#} + {#b#} = B + {#b#} - {#c#}"
    1.39  proof -
    1.40 -  from `c \<in># B` obtain A where B: "B = A + {#c#}" 
    1.41 +  from `c \<in># B` obtain A where B: "B = A + {#c#}"
    1.42      by (blast dest: multi_member_split)
    1.43    have "A + {#b#} = A + {#b#} + {#c#} - {#c#}" by simp
    1.44 -  then have "A + {#b#} = A + {#c#} + {#b#} - {#c#}" 
    1.45 +  then have "A + {#b#} = A + {#c#} + {#b#} - {#c#}"
    1.46      by (simp add: ac_simps)
    1.47    then show ?thesis using B by simp
    1.48  qed
    1.49 @@ -351,7 +351,7 @@
    1.50  apply (erule_tac x = x in allE)
    1.51  apply auto
    1.52  done
    1.53 -  
    1.54 +
    1.55  lemma mset_less_insertD: "(A + {#x#} < B) \<Longrightarrow> (x \<in># B \<and> A < B)"
    1.56  apply (rule conjI)
    1.57   apply (simp add: mset_lessD)
    1.58 @@ -590,7 +590,7 @@
    1.59  lemma finite_Collect_mem [iff]: "finite {x. x :# M}"
    1.60    unfolding set_of_def[symmetric] by simp
    1.61  
    1.62 -lemma set_of_mono: "A \<le> B \<Longrightarrow> set_of A \<subseteq> set_of B"  
    1.63 +lemma set_of_mono: "A \<le> B \<Longrightarrow> set_of A \<subseteq> set_of B"
    1.64    by (metis mset_leD subsetI mem_set_of_iff)
    1.65  
    1.66  subsubsection {* Size *}
    1.67 @@ -705,7 +705,7 @@
    1.68  proof (induct A arbitrary: B)
    1.69    case (empty M)
    1.70    then have "M \<noteq> {#}" by (simp add: mset_less_empty_nonempty)
    1.71 -  then obtain M' x where "M = M' + {#x#}" 
    1.72 +  then obtain M' x where "M = M' + {#x#}"
    1.73      by (blast dest: multi_nonempty_split)
    1.74    then show ?case by simp
    1.75  next
    1.76 @@ -713,9 +713,9 @@
    1.77    have IH: "\<And>B. S < B \<Longrightarrow> size S < size B" by fact
    1.78    have SxsubT: "S + {#x#} < T" by fact
    1.79    then have "x \<in># T" and "S < T" by (auto dest: mset_less_insertD)
    1.80 -  then obtain T' where T: "T = T' + {#x#}" 
    1.81 +  then obtain T' where T: "T = T' + {#x#}"
    1.82      by (blast dest: multi_member_split)
    1.83 -  then have "S < T'" using SxsubT 
    1.84 +  then have "S < T'" using SxsubT
    1.85      by (blast intro: mset_less_add_bothsides)
    1.86    then have "size S < size T'" using IH by simp
    1.87    then show ?case using T by simp
    1.88 @@ -1047,7 +1047,7 @@
    1.89  next
    1.90    case (Cons x xs)
    1.91    then have *: "set ys = set (x # xs)" by (blast dest: multiset_of_eq_setD)
    1.92 -  have "\<And>x y. x \<in> set ys \<Longrightarrow> y \<in> set ys \<Longrightarrow> f x \<circ> f y = f y \<circ> f x" 
    1.93 +  have "\<And>x y. x \<in> set ys \<Longrightarrow> y \<in> set ys \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
    1.94      by (rule Cons.prems(1)) (simp_all add: *)
    1.95    moreover from * have "x \<in> set ys" by simp
    1.96    ultimately have "List.fold f ys = List.fold f (remove1 x ys) \<circ> f x" by (fact fold_remove1_split)
    1.97 @@ -1211,15 +1211,15 @@
    1.98  end
    1.99  
   1.100  syntax
   1.101 -  "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add" 
   1.102 +  "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"
   1.103        ("(3SUM _:#_. _)" [0, 51, 10] 10)
   1.104  
   1.105  syntax (xsymbols)
   1.106 -  "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add" 
   1.107 +  "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"
   1.108        ("(3\<Sum>_\<in>#_. _)" [0, 51, 10] 10)
   1.109  
   1.110  syntax (HTML output)
   1.111 -  "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add" 
   1.112 +  "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"
   1.113        ("(3\<Sum>_\<in>#_. _)" [0, 51, 10] 10)
   1.114  
   1.115  translations
   1.116 @@ -1249,7 +1249,7 @@
   1.117    by (fact msetprod.singleton)
   1.118  
   1.119  lemma msetprod_Un:
   1.120 -  "msetprod (A + B) = msetprod A * msetprod B" 
   1.121 +  "msetprod (A + B) = msetprod A * msetprod B"
   1.122    by (fact msetprod.union)
   1.123  
   1.124  lemma setprod_unfold_msetprod:
   1.125 @@ -1263,15 +1263,15 @@
   1.126  end
   1.127  
   1.128  syntax
   1.129 -  "_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult" 
   1.130 +  "_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"
   1.131        ("(3PROD _:#_. _)" [0, 51, 10] 10)
   1.132  
   1.133  syntax (xsymbols)
   1.134 -  "_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult" 
   1.135 +  "_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"
   1.136        ("(3\<Prod>_\<in>#_. _)" [0, 51, 10] 10)
   1.137  
   1.138  syntax (HTML output)
   1.139 -  "_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult" 
   1.140 +  "_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"
   1.141        ("(3\<Prod>_\<in>#_. _)" [0, 51, 10] 10)
   1.142  
   1.143  translations
   1.144 @@ -1349,7 +1349,7 @@
   1.145  lemma multiset_of_insort [simp]:
   1.146    "multiset_of (insort_key k x xs) = {#x#} + multiset_of xs"
   1.147    by (induct xs) (simp_all add: ac_simps)
   1.148 - 
   1.149 +
   1.150  lemma multiset_of_sort [simp]:
   1.151    "multiset_of (sort_key k xs) = multiset_of xs"
   1.152    by (induct xs) (simp_all add: ac_simps)
   1.153 @@ -1469,7 +1469,7 @@
   1.154      proof (cases zs)
   1.155        case Nil with hyps show ?thesis by auto
   1.156      next
   1.157 -      case Cons 
   1.158 +      case Cons
   1.159        from sort_key_by_quicksort [of f xs]
   1.160        have "sort_key f xs = (let (lts, eqs, gts) = part f (f (xs ! (length xs div 2))) xs
   1.161          in sort_key f lts @ eqs @ sort_key f gts)"
   1.162 @@ -1833,16 +1833,16 @@
   1.163  next
   1.164    case (pw_leq_step x y X Y)
   1.165    then obtain A B Z where
   1.166 -    [simp]: "X = A + Z" "Y = B + Z" 
   1.167 -      and 1[simp]: "(set_of A, set_of B) \<in> max_strict \<or> (B = {#} \<and> A = {#})" 
   1.168 +    [simp]: "X = A + Z" "Y = B + Z"
   1.169 +      and 1[simp]: "(set_of A, set_of B) \<in> max_strict \<or> (B = {#} \<and> A = {#})"
   1.170      by auto
   1.171 -  from pw_leq_step have "x = y \<or> (x, y) \<in> pair_less" 
   1.172 +  from pw_leq_step have "x = y \<or> (x, y) \<in> pair_less"
   1.173      unfolding pair_leq_def by auto
   1.174    thus ?case
   1.175    proof
   1.176      assume [simp]: "x = y"
   1.177      have
   1.178 -      "{#x#} + X = A + ({#y#}+Z) 
   1.179 +      "{#x#} + X = A + ({#y#}+Z)
   1.180        \<and> {#y#} + Y = B + ({#y#}+Z)
   1.181        \<and> ((set_of A, set_of B) \<in> max_strict \<or> (B = {#} \<and> A = {#}))"
   1.182        by (auto simp: ac_simps)
   1.183 @@ -1853,21 +1853,21 @@
   1.184      have "{#x#} + X = ?A' + Z"
   1.185        "{#y#} + Y = ?B' + Z"
   1.186        by (auto simp add: ac_simps)
   1.187 -    moreover have 
   1.188 +    moreover have
   1.189        "(set_of ?A', set_of ?B') \<in> max_strict"
   1.190 -      using 1 A unfolding max_strict_def 
   1.191 +      using 1 A unfolding max_strict_def
   1.192        by (auto elim!: max_ext.cases)
   1.193      ultimately show ?thesis by blast
   1.194    qed
   1.195  qed
   1.196  
   1.197 -lemma 
   1.198 +lemma
   1.199    assumes pwleq: "pw_leq Z Z'"
   1.200    shows ms_strictI: "(set_of A, set_of B) \<in> max_strict \<Longrightarrow> (Z + A, Z' + B) \<in> ms_strict"
   1.201    and   ms_weakI1:  "(set_of A, set_of B) \<in> max_strict \<Longrightarrow> (Z + A, Z' + B) \<in> ms_weak"
   1.202    and   ms_weakI2:  "(Z + {#}, Z' + {#}) \<in> ms_weak"
   1.203  proof -
   1.204 -  from pw_leq_split[OF pwleq] 
   1.205 +  from pw_leq_split[OF pwleq]
   1.206    obtain A' B' Z''
   1.207      where [simp]: "Z = A' + Z''" "Z' = B' + Z''"
   1.208      and mx_or_empty: "(set_of A', set_of B') \<in> max_strict \<or> (A' = {#} \<and> B' = {#})"
   1.209 @@ -1880,7 +1880,7 @@
   1.210        assume max': "(set_of A', set_of B') \<in> max_strict"
   1.211        with max have "(set_of (A + A'), set_of (B + B')) \<in> max_strict"
   1.212          by (auto simp: max_strict_def intro: max_ext_additive)
   1.213 -      thus ?thesis by (rule smsI) 
   1.214 +      thus ?thesis by (rule smsI)
   1.215      next
   1.216        assume [simp]: "A' = {#} \<and> B' = {#}"
   1.217        show ?thesis by (rule smsI) (auto intro: max)
   1.218 @@ -1929,7 +1929,7 @@
   1.219    val set_of_simps = [@{thm set_of_empty}, @{thm set_of_single}, @{thm set_of_union},
   1.220                        @{thm Un_insert_left}, @{thm Un_empty_left}]
   1.221  in
   1.222 -  ScnpReconstruct.multiset_setup (ScnpReconstruct.Multiset 
   1.223 +  ScnpReconstruct.multiset_setup (ScnpReconstruct.Multiset
   1.224    {
   1.225      msetT=msetT, mk_mset=mk_mset, mset_regroup_conv=regroup_munion_conv,
   1.226      mset_member_tac=mset_member_tac, mset_nonempty_tac=mset_nonempty_tac,
   1.227 @@ -1989,7 +1989,7 @@
   1.228  lemma mult_less_trans:
   1.229    "K \<subset># M ==> M \<subset># N ==> K \<subset># (N::'a::order multiset)"
   1.230    by (fact multiset_order.less_trans)
   1.231 -    
   1.232 +
   1.233  lemma mult_less_not_sym:
   1.234    "M \<subset># N ==> \<not> N \<subset># (M::'a::order multiset)"
   1.235    by (fact multiset_order.less_not_sym)
   1.236 @@ -2114,9 +2114,9 @@
   1.237    "mcard (multiset_of xs) = length xs"
   1.238    by (simp add: mcard_multiset_of)
   1.239  
   1.240 -fun ms_lesseq_impl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool option" where 
   1.241 +fun ms_lesseq_impl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool option" where
   1.242    "ms_lesseq_impl [] ys = Some (ys \<noteq> [])"
   1.243 -| "ms_lesseq_impl (Cons x xs) ys = (case List.extract (op = x) ys of 
   1.244 +| "ms_lesseq_impl (Cons x xs) ys = (case List.extract (op = x) ys of
   1.245       None \<Rightarrow> None
   1.246     | Some (ys1,_,ys2) \<Rightarrow> ms_lesseq_impl xs (ys1 @ ys2))"
   1.247  
   1.248 @@ -2148,7 +2148,7 @@
   1.249      obtain ys1 y ys2 where res: "res = (ys1,y,ys2)" by (cases res, auto)
   1.250      note Some = Some[unfolded res]
   1.251      from extract_SomeE[OF Some] have "ys = ys1 @ x # ys2" by simp
   1.252 -    hence id: "multiset_of ys = multiset_of (ys1 @ ys2) + {#x#}" 
   1.253 +    hence id: "multiset_of ys = multiset_of (ys1 @ ys2) + {#x#}"
   1.254        by (auto simp: ac_simps)
   1.255      show ?thesis unfolding ms_lesseq_impl.simps
   1.256        unfolding Some option.simps split
   1.257 @@ -2267,13 +2267,13 @@
   1.258        by (rule Cons.hyps(2))
   1.259      thus ?thesis
   1.260        unfolding k by (auto simp: add.commute union_lcomm)
   1.261 -  qed      
   1.262 +  qed
   1.263  qed
   1.264  
   1.265  lemma ex_multiset_of_zip_left:
   1.266    assumes "length xs = length ys" "multiset_of xs' = multiset_of xs"
   1.267    shows "\<exists>ys'. length ys' = length xs' \<and> multiset_of (zip xs' ys') = multiset_of (zip xs ys)"
   1.268 -using assms 
   1.269 +using assms
   1.270  proof (induct xs ys arbitrary: xs' rule: list_induct2)
   1.271    case Nil
   1.272    thus ?case
   1.273 @@ -2281,19 +2281,9 @@
   1.274  next
   1.275    case (Cons x xs y ys xs')
   1.276    obtain j where j_len: "j < length xs'" and nth_j: "xs' ! j = x"
   1.277 -  proof -
   1.278 -    assume "\<And>j. \<lbrakk>j < length xs'; xs' ! j = x\<rbrakk> \<Longrightarrow> ?thesis"
   1.279 -    moreover have "\<And>k m n. (m\<Colon>nat) + n < m + k \<or> \<not> n < k" by linarith
   1.280 -    moreover have "\<And>n a as. n - n < length (a # as) \<or> n < n"
   1.281 -      by (metis Nat.add_diff_inverse diff_add_inverse2 impossible_Cons le_add1
   1.282 -        less_diff_conv not_add_less2)
   1.283 -    moreover have "\<not> length xs' < length xs'" by blast
   1.284 -    ultimately show ?thesis
   1.285 -      by (metis (no_types) Cons.prems Nat.add_diff_inverse diff_add_inverse2 length_append
   1.286 -        less_diff_conv list.set_intros(1) multiset_of_eq_setD nth_append_length split_list)
   1.287 -  qed
   1.288 -
   1.289 -  def xsa \<equiv> "take j xs' @ drop (Suc j) xs'" 
   1.290 +    by (metis Cons.prems in_set_conv_nth list.set_intros(1) multiset_of_eq_setD)
   1.291 +
   1.292 +  def xsa \<equiv> "take j xs' @ drop (Suc j) xs'"
   1.293    have "multiset_of xs' = {#x#} + multiset_of xsa"
   1.294      unfolding xsa_def using j_len nth_j
   1.295      by (metis (no_types) ab_semigroup_add_class.add_ac(1) append_take_drop_id Cons_nth_drop_Suc
   1.296 @@ -2345,7 +2335,7 @@
   1.297  
   1.298  bnf "'a multiset"
   1.299    map: image_mset
   1.300 -  sets: set_of 
   1.301 +  sets: set_of
   1.302    bd: natLeq
   1.303    wits: "{#}"
   1.304    rel: rel_mset