moved lemmas and locales around (with minor incompatibilities)
authorblanchet
Thu Jul 07 09:24:03 2016 +0200 (2016-07-07)
changeset 634093f3223b90239
parent 63408 74c609115df0
child 63410 9789ccc2a477
child 63411 e051eea34990
child 63419 f473b6b16c63
moved lemmas and locales around (with minor incompatibilities)
src/HOL/Library/Multiset.thy
src/HOL/Library/Multiset_Order.thy
src/HOL/UNITY/Comp/AllocBase.thy
     1.1 --- a/src/HOL/Library/Multiset.thy	Thu Jul 07 00:43:27 2016 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Thu Jul 07 09:24:03 2016 +0200
     1.3 @@ -426,8 +426,6 @@
     1.4  qed
     1.5  
     1.6  
     1.7 -
     1.8 -
     1.9  subsubsection \<open>Pointwise ordering induced by count\<close>
    1.10  
    1.11  definition subseteq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<subseteq>#" 50)
    1.12 @@ -779,6 +777,7 @@
    1.13  
    1.14  interpretation subset_mset: order "op \<le>#" "op <#" by unfold_locales auto
    1.15  
    1.16 +
    1.17  subsubsection \<open>Conditionally complete lattice\<close>
    1.18  
    1.19  instantiation multiset :: (type) Inf
    1.20 @@ -2577,6 +2576,7 @@
    1.21    by standard (auto simp add: less_eq_multiset_def intro: union_le_mono2)
    1.22  end
    1.23  
    1.24 +
    1.25  subsubsection \<open>Termination proofs with multiset orders\<close>
    1.26  
    1.27  lemma multi_member_skip: "x \<in># XS \<Longrightarrow> x \<in># {# y #} + XS"
     2.1 --- a/src/HOL/Library/Multiset_Order.thy	Thu Jul 07 00:43:27 2016 +0200
     2.2 +++ b/src/HOL/Library/Multiset_Order.thy	Thu Jul 07 09:24:03 2016 +0200
     2.3 @@ -9,7 +9,7 @@
     2.4  imports Multiset
     2.5  begin
     2.6  
     2.7 -subsubsection \<open>Alternative characterizations\<close>
     2.8 +subsection \<open>Alternative characterizations\<close>
     2.9  
    2.10  context order
    2.11  begin
    2.12 @@ -215,96 +215,91 @@
    2.13  lemmas less_multiset\<^sub>D\<^sub>M = mult\<^sub>D\<^sub>M[folded less_multiset_def]
    2.14  lemmas less_multiset\<^sub>H\<^sub>O = mult\<^sub>H\<^sub>O[folded less_multiset_def]
    2.15  
    2.16 -lemma less_eq_multiset\<^sub>H\<^sub>O:
    2.17 -  fixes M N :: "('a :: linorder) multiset"
    2.18 -  shows "M \<le> N \<longleftrightarrow> (\<forall>y. count N y < count M y \<longrightarrow> (\<exists>x. y < x \<and> count M x < count N x))"
    2.19 -  by (auto simp: less_eq_multiset_def less_multiset\<^sub>H\<^sub>O)
    2.20 -
    2.21 -lemma wf_less_multiset: "wf {(M :: ('a :: wellorder) multiset, N). M < N}"
    2.22 -  unfolding less_multiset_def by (auto intro: wf_mult wf)
    2.23 -
    2.24 -instantiation multiset :: (linorder) linorder
    2.25 -begin
    2.26 -  instance by standard (metis less_eq_multiset\<^sub>H\<^sub>O not_less_iff_gr_or_eq)
    2.27 -end
    2.28 -
    2.29 -instantiation multiset :: (wellorder) wellorder
    2.30 -begin
    2.31 -  instance by standard (metis less_multiset_def wf wf_def wf_mult)
    2.32 -end
    2.33 -
    2.34 -lemma less_eq_multiset_total:
    2.35 -  fixes M N :: "('a :: linorder) multiset"
    2.36 -  shows "\<not> M \<le> N \<Longrightarrow> N \<le> M"
    2.37 -  by simp
    2.38 -
    2.39  lemma subset_eq_imp_le_multiset:
    2.40 -  fixes M N :: "('a :: linorder) multiset"
    2.41    shows "M \<le># N \<Longrightarrow> M \<le> N"
    2.42    unfolding less_eq_multiset_def less_multiset\<^sub>H\<^sub>O
    2.43    by (simp add: less_le_not_le subseteq_mset_def)
    2.44  
    2.45  lemma le_multiset_right_total:
    2.46 -  fixes M :: "('a :: linorder) multiset"
    2.47    shows "M < M + {#x#}"
    2.48    unfolding less_eq_multiset_def less_multiset\<^sub>H\<^sub>O by simp
    2.49  
    2.50  lemma less_eq_multiset_empty_left[simp]:
    2.51 -  fixes M :: "('a :: linorder) multiset"
    2.52    shows "{#} \<le> M"
    2.53    by (simp add: subset_eq_imp_le_multiset)
    2.54  
    2.55 +lemma add_eq_self_empty_iff: "M + N = M \<longleftrightarrow> N = {#}"
    2.56 +  by (rule cancel_comm_monoid_add_class.add_cancel_left_right)
    2.57 +
    2.58 +lemma ex_gt_imp_less_multiset: "(\<exists>y. y \<in># N \<and> (\<forall>x. x \<in># M \<longrightarrow> x < y)) \<Longrightarrow> M < N"
    2.59 +  unfolding less_multiset\<^sub>H\<^sub>O
    2.60 +  by (metis count_eq_zero_iff count_greater_zero_iff less_le_not_le)
    2.61 +
    2.62  lemma less_eq_multiset_empty_right[simp]:
    2.63 -  fixes M :: "('a :: linorder) multiset"
    2.64 -  shows "M \<noteq> {#} \<Longrightarrow> \<not> M \<le> {#}"
    2.65 +  "M \<noteq> {#} \<Longrightarrow> \<not> M \<le> {#}"
    2.66    by (metis less_eq_multiset_empty_left antisym)
    2.67  
    2.68 -lemma le_multiset_empty_left[simp]:
    2.69 -  fixes M :: "('a :: linorder) multiset"
    2.70 -  shows "M \<noteq> {#} \<Longrightarrow> {#} < M"
    2.71 +lemma le_multiset_empty_left[simp]: "M \<noteq> {#} \<Longrightarrow> {#} < M"
    2.72    by (simp add: less_multiset\<^sub>H\<^sub>O)
    2.73  
    2.74 -lemma le_multiset_empty_right[simp]:
    2.75 -  fixes M :: "('a :: linorder) multiset"
    2.76 -  shows "\<not> M < {#}"
    2.77 +lemma le_multiset_empty_right[simp]: "\<not> M < {#}"
    2.78    using subset_eq_empty less_multiset\<^sub>D\<^sub>M by blast
    2.79  
    2.80 +lemma union_le_diff_plus: "P \<le># M \<Longrightarrow> N < P \<Longrightarrow> M - P + N < M"
    2.81 +  by (drule subset_mset.diff_add[symmetric]) (metis union_le_mono2)
    2.82 +
    2.83 +instantiation multiset :: (linorder) linorder
    2.84 +begin
    2.85 +
    2.86 +lemma less_eq_multiset\<^sub>H\<^sub>O:
    2.87 +  "M \<le> N \<longleftrightarrow> (\<forall>y. count N y < count M y \<longrightarrow> (\<exists>x. y < x \<and> count M x < count N x))"
    2.88 +  by (auto simp: less_eq_multiset_def less_multiset\<^sub>H\<^sub>O)
    2.89 +
    2.90 +instance by standard (metis less_eq_multiset\<^sub>H\<^sub>O not_less_iff_gr_or_eq)
    2.91 +
    2.92 +lemma less_eq_multiset_total:
    2.93 +  fixes M N :: "'a multiset"
    2.94 +  shows "\<not> M \<le> N \<Longrightarrow> N \<le> M"
    2.95 +  by simp
    2.96 +
    2.97  lemma
    2.98 -  fixes M N :: "('a :: linorder) multiset"
    2.99 +  fixes M N :: "'a multiset"
   2.100    shows
   2.101      less_eq_multiset_plus_left[simp]: "N \<le> (M + N)" and
   2.102      less_eq_multiset_plus_right[simp]: "M \<le> (M + N)"
   2.103 -  using [[metis_verbose = false]] by (metis subset_eq_imp_le_multiset mset_subset_eq_add_left add.commute)+
   2.104 +  using [[metis_verbose = false]]
   2.105 +  by (metis subset_eq_imp_le_multiset mset_subset_eq_add_left add.commute)+
   2.106  
   2.107  lemma
   2.108 -  fixes M N :: "('a :: linorder) multiset"
   2.109 +  fixes M N :: "'a multiset"
   2.110    shows
   2.111      le_multiset_plus_plus_left_iff[simp]: "M + N < M' + N \<longleftrightarrow> M < M'" and
   2.112      le_multiset_plus_plus_right_iff[simp]: "M + N < M + N' \<longleftrightarrow> N < N'"
   2.113    unfolding less_multiset\<^sub>H\<^sub>O by auto
   2.114  
   2.115 -lemma add_eq_self_empty_iff: "M + N = M \<longleftrightarrow> N = {#}"
   2.116 -  by (rule cancel_comm_monoid_add_class.add_cancel_left_right)
   2.117 -
   2.118  lemma
   2.119 -  fixes M N :: "('a :: linorder) multiset"
   2.120 +  fixes M N :: "'a multiset"
   2.121    shows
   2.122      le_multiset_plus_left_nonempty[simp]: "M \<noteq> {#} \<Longrightarrow> N < M + N" and
   2.123      le_multiset_plus_right_nonempty[simp]: "N \<noteq> {#} \<Longrightarrow> M < M + N"
   2.124    using [[metis_verbose = false]]
   2.125 -  by (metis add.right_neutral le_multiset_empty_left le_multiset_plus_plus_right_iff
   2.126 -    add.commute)+
   2.127 -
   2.128 -lemma ex_gt_imp_less_multiset: "(\<exists>y :: 'a :: linorder. y \<in># N \<and> (\<forall>x. x \<in># M \<longrightarrow> x < y)) \<Longrightarrow> M < N"
   2.129 -  unfolding less_multiset\<^sub>H\<^sub>O
   2.130 -  by (metis count_eq_zero_iff count_greater_zero_iff less_le_not_le)
   2.131 +  by (metis add.right_neutral le_multiset_empty_left le_multiset_plus_plus_right_iff add.commute)+
   2.132  
   2.133  lemma ex_gt_count_imp_le_multiset:
   2.134    "(\<forall>y :: 'a :: linorder. y \<in># M + N \<longrightarrow> y \<le> x) \<Longrightarrow> count M x < count N x \<Longrightarrow> M < N"
   2.135    unfolding less_multiset\<^sub>H\<^sub>O
   2.136    by (metis add_gr_0 count_union mem_Collect_eq not_gr0 not_le not_less_iff_gr_or_eq set_mset_def)
   2.137  
   2.138 -lemma union_le_diff_plus: "P \<le># M \<Longrightarrow> N < P \<Longrightarrow> M - P + N < M"
   2.139 -  by (drule subset_mset.diff_add[symmetric]) (metis union_le_mono2)
   2.140 +end
   2.141 +
   2.142 +instantiation multiset :: (wellorder) wellorder
   2.143 +begin
   2.144 +
   2.145 +lemma wf_less_multiset: "wf {(M :: 'a multiset, N). M < N}"
   2.146 +  unfolding less_multiset_def by (auto intro: wf_mult wf)
   2.147 +
   2.148 +instance by standard (metis less_multiset_def wf wf_def wf_mult)
   2.149  
   2.150  end
   2.151 +
   2.152 +end
     3.1 --- a/src/HOL/UNITY/Comp/AllocBase.thy	Thu Jul 07 00:43:27 2016 +0200
     3.2 +++ b/src/HOL/UNITY/Comp/AllocBase.thy	Thu Jul 07 09:24:03 2016 +0200
     3.3 @@ -39,7 +39,6 @@
     3.4  lemma subseteq_le_multiset: "(A :: 'a::order multiset) \<le> A + B"
     3.5  unfolding less_eq_multiset_def apply (cases B; simp)
     3.6  apply (rule union_le_mono2[of "{#}" "_ + {#_#}" A, simplified])
     3.7 -apply (simp add: less_multiset\<^sub>H\<^sub>O)
     3.8  done
     3.9  
    3.10  lemma mono_bag_of: "mono (bag_of :: 'a list => ('a::order) multiset)"