lib/isabelle/Why3_Map.thy.2019

   1 theory Why3_Map
   2 imports Why3_Setup
   3 begin
   4
   5 section \<open> Generic Maps \<close>
   6
   7 why3_open "map/Map.xml"
   8
   9 why3_vc setqtdef by auto
  10
  11 why3_end
  12
  13
  14 section \<open> Constant Maps \<close>
  15
  16 definition abs_const :: "'a \<Rightarrow> ('b \<Rightarrow> 'a)" where
  17   "abs_const v y = v"
  18
  19 why3_open "map/Const.xml"
  20   constants
  21     const=abs_const
  22
  23 why3_vc constqtdef
  24   by (simp add: abs_const_def)
  25
  26 why3_end
  27
  28 section \<open> Number of occurrences \<close>
  29
  30 definition occ :: "'a \<Rightarrow> (int \<Rightarrow> 'a) \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int" where
  31   "occ v m l u = int (card (m -` {v} \<inter> {l..<u}))"
  32
  33 why3_open "map/Occ.xml"
  34   constants
  35     occ = occ
  36
  37 why3_vc occ_empty
  38   using assms
  39   by (simp add: occ_def)
  40
  41 why3_vc occ_right_no_add
  42 proof -
  43   from assms have "{l..<u} = {l..<u - 1} \<union> {u - 1}" by auto
  44   with assms show ?thesis by (simp add: occ_def)
  45 qed
  46
  47 why3_vc occ_right_add
  48 proof -
  49   from assms have "{l..<u} = {l..<u - 1} \<union> {u - 1}" by auto
  50   with assms show ?thesis by (simp add: occ_def)
  51 qed
  52
  53 why3_vc occ_bounds
  54 proof -
  55   have "card ({l..<u} \<inter> m -` {v}) \<le> card {l..<u}"
  56     by (blast intro: card_mono)
  57   moreover have "card ({l..<u} - m -` {v}) = card {l..<u} - card ({l..<u} \<inter> m -` {v})"
  58     by (blast intro: card_Diff_subset_Int)
  59   ultimately have "card {l..<u} = card ({l..<u} - m -` {v}) + card ({l..<u} \<inter> m -` {v})"
  60     by simp
  61   with assms show ?C2
  62     by (simp add: occ_def Int_commute)
  63 qed (simp add: occ_def)
  64
  65 why3_vc occ_append
  66 proof -
  67   from assms have "{l..<u} = {l..<mid} \<union> {mid..<u}"
  68     by (simp add: ivl_disj_un)
  69   moreover have "m -` {v} \<inter> {l..<mid} \<inter> (m -` {v} \<inter> {mid..<u}) =
  70     m -` {v} \<inter> ({l..<mid} \<inter> {mid..<u})"
  71     by auto
  72   ultimately show ?thesis
  73     by (simp add: occ_def Int_Un_distrib card_Un_disjoint)
  74 qed
  75
  76 why3_vc occ_neq
  77   using assms
  78   by (auto simp add: occ_def)
  79
  80 why3_vc occ_exists
  81   using assms
  82   by (auto simp add: occ_def card_gt_0_iff)
  83
  84 why3_vc occ_pos
  85   using assms
  86   by (auto simp add: occ_def card_gt_0_iff)
  87
  88 why3_vc occ_eq
  89 proof -
  90   from assms have "m1 -` {v} \<inter> {l..<u} = m2 -` {v} \<inter> {l..<u}" by auto
  91   then show ?thesis by (simp add: occ_def)
  92 qed
  93
  94 lemma vimage_update:
  95   "m(i := x) -` {z} = (if x = z then m -` {z} \<union> {i} else m -` {z} - {i})"
  96   by auto
  97
  98 why3_vc occ_exchange
  99   using assms
 100   by (simp add: occ_def vimage_update insert_Diff_if card_insert)
 101     (auto simp add: Diff_Int_distrib2 card_Diff_subset_Int)
 102
 103 why3_vc occ_left_add
 104 proof -
 105   from assms have "{l..<u} = {l} \<union> {l + 1..<u}" by auto
 106   with assms show ?thesis by (simp add: occ_def)
 107 qed
 108
 109 why3_vc occ_left_no_add
 110 proof -
 111   from assms have "{l..<u} = {l} \<union> {l + 1..<u}" by auto
 112   with assms show ?thesis by (simp add: occ_def)
 113 qed
 114
 115 why3_end
 116
 117 why3_open "map/MapPermut.xml"
 118
 119 why3_vc permut_trans
 120   using assms
 121   by (simp add: permut_def)
 122
 123 why3_vc permut_exists
 124 proof -
 125   from assms have "0 < occ (a2 i) a1 l u"
 126     by (simp add: permut_def occ_pos)
 127   then show ?thesis by (auto dest: occ_exists)
 128 qed
 129
 130 why3_end
 131
 132
 133 section \<open> Injectivity and surjectivity for maps (indexed by integers) \<close>
 134
 135 why3_open "map/MapInjection.xml"
 136
 137 why3_vc injective_surjective
 138 proof -
 139   have "finite {0..<n}" by simp
 140   moreover from assms have "a ` {0..<n} \<subseteq> {0..<n}"
 141     by (auto simp add: range_def)
 142   moreover from assms have "inj_on a {0..<n}"
 143     by (force intro!: inj_onI simp add: injective_def)
 144   ultimately have "a ` {0..<n} = {0..<n}" by (rule endo_inj_surj)
 145   then have "{0..<n} \<subseteq> a ` {0..<n}" by simp
 146   then show ?thesis by (force simp add: surjective_def)
 147 qed
 148
 149 why3_vc injection_occ
 150   unfolding injective_def occ_def
 151 proof
 152   assume H: "\<forall>i j. 0 \<le> i \<and> i < n \<longrightarrow> 0 \<le> j \<and> j < n \<longrightarrow> i \<noteq> j \<longrightarrow> m i \<noteq> m j"
 153   show "\<forall>v. int (card (m -` {v} \<inter> {0..<n})) \<le> 1"
 154   proof
 155     fix v
 156     let ?S = "m -` {v} \<inter> {0..<n}"
 157     show "int (card ?S) \<le> 1"
 158     proof (rule ccontr)
 159       assume "\<not> int (card ?S) \<le> 1"
 160       with card_le_Suc_iff [of 1 ?S]
 161       obtain x S where "?S = insert x S"
 162         "x \<notin> S" "1 \<le> card S" "finite S"
 163         by auto
 164       with card_le_Suc_iff [of 0 S]
 165       obtain x' S' where "S = insert x' S'" by auto
 166       with `?S = insert x S` `x \<notin> S`
 167       have "m x = v" "m x' = v" "x \<noteq> x'" "0 \<le> x" "x < n" "0 \<le> x'" "x' < n"
 168         by auto
 169       with H show False by auto
 170     qed
 171   qed
 172 next
 173   assume H: "\<forall>v. int (card (m -` {v} \<inter> {0..<n})) \<le> 1"
 174   show "\<forall>i j. 0 \<le> i \<and> i < n \<longrightarrow> 0 \<le> j \<and> j < n \<longrightarrow> i \<noteq> j \<longrightarrow> m i \<noteq> m j"
 175   proof (intro strip notI)
 176     fix i j
 177     let ?S = "m -` {m i} \<inter> {0..<n}"
 178     assume "0 \<le> i \<and> i < n" "0 \<le> j \<and> j < n" "i \<noteq> j" "m i = m j"
 179     have "finite ?S" by simp
 180     moreover from `0 \<le> i \<and> i < n` have "i \<in> ?S" by simp
 181     ultimately have S: "card ?S = Suc (card (?S - {i}))"
 182       by (rule card.remove)
 183     have "finite (?S - {i})" by simp
 184     moreover from `0 \<le> j \<and> j < n` `i \<noteq> j` `m i = m j`
 185     have "j \<in> ?S - {i}" by simp
 186     ultimately have "card (?S - {i}) = Suc (card (?S - {i} - {j}))"
 187       by (rule card.remove)
 188     with S have "\<not> int (card ?S) \<le> 1" by simp
 189     with H show False by simp
 190   qed
 191 qed
 192
 193 why3_end
 194
 195 end