diff --git a/thys/Cauchy/CauchysMeanTheorem.thy b/thys/Cauchy/CauchysMeanTheorem.thy
--- a/thys/Cauchy/CauchysMeanTheorem.thy
+++ b/thys/Cauchy/CauchysMeanTheorem.thy
@@ -1,1194 +1,1194 @@
 (*  Title:       Cauchy's Mean Theorem
     Author:      Benjamin Porter <Benjamin.Porter at gmail.com>, 2006
                  cleaned up a bit by Tobias Nipkow, 2007
     Maintainer:  Benjamin Porter <Benjamin.Porter at gmail.com>
 *)
 
 chapter \<open>Cauchy's Mean Theorem\<close>
 
 theory CauchysMeanTheorem
 imports Complex_Main
 begin
 
 section \<open>Abstract\<close>
 
 text \<open>The following document presents a proof of Cauchy's Mean
 theorem formalised in the Isabelle/Isar theorem proving system.
 
 {\em Theorem}: For any collection of positive real numbers the
 geometric mean is always less than or equal to the arithmetic mean. In
 mathematical terms: $$\sqrt[n]{x_1 x_2 \dots x_n} \leq \frac{x_1 +
 \dots + x_n}{n}$$ We will use the term {\em mean} to denote the
 arithmetic mean and {\em gmean} to denote the geometric mean.
 
 {\em Informal Proof}:
 
 This proof is based on the proof presented in [1]. First we need an
 auxiliary lemma (the proof of which is presented formally below) that
 states:
 
 Given two pairs of numbers of equal sum, the pair with the greater
 product is the pair with the least difference. Using this lemma we now
 present the proof -
 
 Given any collection $C$ of positive numbers with mean $M$ and product
 $P$ and with some element not equal to M we can choose two elements
 from the collection, $a$ and $b$ where $a>M$ and $b<M$. Remove these
 elements from the collection and replace them with two new elements,
 $a'$ and $b'$ such that $a' = M$ and $a' + b' = a + b$. This new
 collection $C'$ now has a greater product $P'$ but equal mean with
 respect to $C$. We can continue in this fashion until we have a
 collection $C_n$ such that $P_n > P$ and $M_n = M$, but $C_n$ has all
 its elements equal to $M$ and thus $P_n = M^n$. Using the definition
 of geometric and arithmetic means above we can see that for any
 collection of positive elements $E$ it is always true that gmean E
 $\leq$ mean E. QED.
 
 
 [1] Dorrie, H. "100 Great Problems of Elementary Mathematics." 1965, Dover.
 \<close>
 
 
 section \<open>Formal proof\<close>
 
 (* ============================================================================= *)
 (* ============================================================================= *)
 (* ============================================================================= *)
 
 subsection \<open>Collection sum and product\<close>
 
 text \<open>The finite collections of numbers will be modelled as
 lists. We then define sum and product operations over these lists.\<close>
 
 subsubsection \<open>Sum and product definitions\<close>
 
 notation (input) sum_list ("\<Sum>:_" [999] 998)
 
 notation (input) prod_list ("\<Prod>:_" [999] 998)
 
 subsubsection \<open>Properties of sum and product\<close>
 
 text \<open>We now present some useful properties of sum and product over
 collections.\<close>
 
 text \<open>These lemmas just state that if all the elements in a
 collection $C$ are less (greater than) than some value $m$, then the
 sum will less than (greater than) $m*length(C)$.\<close>
 
 lemma sum_list_mono_lt [rule_format]:
   fixes xs::"real list"
   shows "xs \<noteq> [] \<and> (\<forall>x\<in> set xs. x < m)
          \<longrightarrow> ((\<Sum>:xs) < (m*(real (length xs))))"
 proof (induct xs)
   case Nil show ?case by simp
 next
   case (Cons y ys)
   {
     assume ant: "y#ys \<noteq> [] \<and> (\<forall>x\<in>set(y#ys). x < m)"
     hence ylm: "y < m" by simp
     have "\<Sum>:(y#ys) < m * real (length (y#ys))"
     proof cases
       assume "ys \<noteq> []"
       moreover with ant have "\<forall>x\<in>set ys. x < m" by simp
       moreover with calculation Cons have "\<Sum>:ys < m*real (length ys)" by simp
       hence "\<Sum>:ys + y < m*real(length ys) + y" by simp
       with ylm have "\<Sum>:(y#ys) < m*(real(length ys) + 1)" by(simp add:field_simps)
       then have "\<Sum>:(y#ys) < m*(real(length ys + 1))"
         by (simp add: algebra_simps)
       hence "\<Sum>:(y#ys) < m*(real (length(y#ys)))" by simp
       thus ?thesis .
     next
       assume "\<not> (ys \<noteq> [])"
       hence "ys = []" by simp
       with ylm show ?thesis by simp
     qed
   }
   thus ?case by simp
 qed
 
 
 lemma sum_list_mono_gt [rule_format]:
   fixes xs::"real list"
   shows "xs \<noteq> [] \<and> (\<forall>x\<in>set xs. x > m)
          \<longrightarrow> ((\<Sum>:xs) > (m*(real (length xs))))"
 txt \<open>proof omitted\<close>
 (*<*)
 proof (induct xs)
   case Nil show ?case by simp
 next
   case (Cons y ys)
   {
     assume ant: "y#ys \<noteq> [] \<and> (\<forall>x\<in>set(y#ys). x > m)"
     hence ylm: "y > m" by simp
     have "\<Sum>:(y#ys) > m * real (length (y#ys))"
     proof cases
       assume "ys \<noteq> []"
       moreover with ant have "\<forall>x\<in>set ys. x > m" by simp
       moreover with calculation Cons have "\<Sum>:ys > m*real (length ys)" by simp
       hence "\<Sum>:ys + y > m*real(length ys) + y" by simp
       with ylm have "\<Sum>:(y#ys) > m*(real(length ys) + 1)" by(simp add:field_simps)
       then have "\<Sum>:(y#ys) > m*(real(length ys + 1))"
         by (simp add: algebra_simps)
       hence "\<Sum>:(y#ys) > m*(real (length(y#ys)))" by simp
       thus ?thesis .
     next
       assume "\<not> (ys \<noteq> [])"
       hence "ys = []" by simp
       with ylm show ?thesis by simp
     qed
   }
   thus ?case by simp
 (*>*)
 qed
 
 text \<open>If $a$ is in $C$ then the sum of the collection $D$ where $D$
 is $C$ with $a$ removed is the sum of $C$ minus $a$.\<close>
 
 lemma sum_list_rmv1:
   "a \<in> set xs \<Longrightarrow> \<Sum>:(remove1 a xs) = \<Sum>:xs - (a :: 'a :: ab_group_add)"
 by (induct xs) auto
 
 text \<open>A handy addition and division distribution law over collection
 sums.\<close>
 
 lemma list_sum_distrib_aux:
   shows "(\<Sum>:xs/(n :: 'a :: archimedean_field) + \<Sum>:xs) = (1 + (1/n)) * \<Sum>:xs"
 proof (induct xs)
   case Nil show ?case by simp
 next
   case (Cons x xs)
   show ?case
   proof -
     have
       "\<Sum>:(x#xs)/n = x/n + \<Sum>:xs/n"
       by (simp add: add_divide_distrib)
     also with Cons have
       "\<dots> = x/n + (1+1/n)*\<Sum>:xs - \<Sum>:xs"
       by simp
     finally have
       "\<Sum>:(x#xs) / n + \<Sum>:(x#xs) = x/n + (1+1/n)*\<Sum>:xs - \<Sum>:xs + \<Sum>:(x#xs)"
       by simp
     also have
       "\<dots> = x/n + (1+(1/n)- 1)*\<Sum>:xs + \<Sum>:(x#xs)"
       by (subst mult_1_left [symmetric, of "\<Sum>:xs"]) (simp add: field_simps)
     also have
       "\<dots> = x/n + (1/n)*\<Sum>:xs + \<Sum>:(x#xs)"
       by simp
     also have
       "\<dots> = (1/n)*\<Sum>:(x#xs) + 1*\<Sum>:(x#xs)" by(simp add: divide_simps)
     finally show ?thesis by (simp add: field_simps)
   qed
 qed
 
 lemma remove1_retains_prod:
   fixes a and xs::"'a :: comm_ring_1 list"
   shows "a : set xs \<longrightarrow> \<Prod>:xs = \<Prod>:(remove1 a xs) * a"
   (is "?P xs")
 proof (induct xs)
   case Nil
   show ?case by simp
 next
   case (Cons aa list)
   assume plist: "?P list"
   show "?P (aa#list)"
   proof
     assume aml: "a : set(aa#list)"
     show "\<Prod>:(aa # list) = \<Prod>:remove1 a (aa # list) * a"
     proof (cases)
       assume aeq: "a = aa"
       hence
         "remove1 a (aa#list) = list"
         by simp
       hence
         "\<Prod>:(remove1 a (aa#list)) = \<Prod>:list"
         by simp
       moreover with aeq have
         "\<Prod>:(aa#list) = \<Prod>:list * a"
         by simp
       ultimately show
         "\<Prod>:(aa#list) = \<Prod>:remove1 a (aa # list) * a"
         by simp
     next
       assume naeq: "a \<noteq> aa"
       with aml have aml2: "a : set list" by simp
       from naeq have
         "remove1 a (aa#list) = aa#(remove1 a list)"
         by simp
       moreover hence
         "\<Prod>:(remove1 a (aa#list)) = aa * \<Prod>:(remove1 a list)"
         by simp
       moreover from aml2 plist have
         "\<Prod>:list = \<Prod>:(remove1 a list) * a"
         by simp
       ultimately show
         "\<Prod>:(aa#list) = \<Prod>:remove1 a (aa # list) * a"
         by simp
     qed
   qed
 qed
 
 text \<open>The final lemma of this section states that if all elements
 are positive and non-zero then the product of these elements is also
 positive and non-zero.\<close>
 
 lemma el_gt0_imp_prod_gt0 [rule_format]:
   fixes xs::"'a :: archimedean_field list"
   shows "\<forall>y. y : set xs \<longrightarrow> y > 0 \<Longrightarrow> \<Prod>:xs > 0"
 proof (induct xs)
   case Nil show ?case by simp
 next
   case (Cons a xs)
   have exp: "\<Prod>:(a#xs) = \<Prod>:xs * a" by simp
   with Cons have "a > 0" by simp
   with exp Cons show ?case by simp
 qed
 
 
 (* ============================================================================= *)
 (* ============================================================================= *)
 (* ============================================================================= *)
 
 subsection \<open>Auxiliary lemma\<close>
 
 text \<open>This section presents a proof of the auxiliary lemma required
 for this theorem.\<close>
 
 lemma prod_exp:
   fixes x::real
   shows "4*(x*y) = (x+y)^2 - (x-y)^2"
   by (simp add: power2_diff power2_sum)
 
 lemma abs_less_imp_sq_less [rule_format]:
   fixes x::real and y::real and z::real and w::real
   assumes diff: "abs (x-y) < abs (z-w)"
   shows "(x-y)^2 < (z-w)^2"
 proof cases
   assume "x=y"
   hence "abs (x-y) = 0" by simp
   moreover with diff have "abs(z-w) > 0" by simp
   hence "(z-w)^2 > 0" by simp
   ultimately show ?thesis by auto
 next
   assume "x\<noteq>y"
   hence "abs (x - y) > 0" by simp
   with diff have "(abs (x-y))^2 < (abs (z-w))^2"
     by - (drule power_strict_mono [where a="abs (x-y)" and n=2 and b="abs (z-w)"], auto)
   thus ?thesis by simp
 qed
 
 text \<open>The required lemma (phrased slightly differently than in the
 informal proof.) Here we show that for any two pairs of numbers with
 equal sums the pair with the least difference has the greater
 product.\<close>
 
 lemma le_diff_imp_gt_prod [rule_format]:
   fixes x::real and y::real and z::real and w::real
   assumes diff: "abs (x-y) < abs (z-w)" and sum: "x+y = z+w"
   shows "x*y > z*w"
 proof -
   from sum have "(x+y)^2 = (z+w)^2" by simp
   moreover from diff have "(x-y)^2 < (z-w)^2" by (rule abs_less_imp_sq_less)
   ultimately have "(x+y)^2 - (x-y)^2 > (z+w)^2 - (z-w)^2" by auto
   thus "x*y > z*w" by (simp only: prod_exp [symmetric])
 qed
 
 (* ============================================================================= *)
 (* ============================================================================= *)
 (* ============================================================================= *)
 
 subsection \<open>Mean and GMean\<close>
 
 text \<open>Now we introduce definitions and properties of arithmetic and
 geometric means over collections of real numbers.\<close>
 
 subsubsection \<open>Definitions\<close>
 
 text \<open>{\em Arithmetic mean}\<close>
 
 definition
   mean :: "(real list)\<Rightarrow>real" where
   "mean s = (\<Sum>:s / real (length s))"
 
 text \<open>{\em Geometric mean}\<close>
 
 definition
   gmean :: "(real list)\<Rightarrow>real" where
   "gmean s = root (length s) (\<Prod>:s)"
 
 
 subsubsection \<open>Properties\<close>
 
-text \<open>Here we present some trival properties of {\em mean} and {\em gmean}.\<close>
+text \<open>Here we present some trivial properties of {\em mean} and {\em gmean}.\<close>
 
 lemma list_sum_mean:
   fixes xs::"real list"
   shows "\<Sum>:xs = ((mean xs) * (real (length xs)))"
 apply (induct_tac xs)
 apply simp
 apply clarsimp
 apply (unfold mean_def)
 apply clarsimp
 done
 
 lemma list_mean_eq_iff:
   fixes one::"real list" and two::"real list"
   assumes
     se: "( \<Sum>:one = \<Sum>:two )" and
     le: "(length one = length two)"
   shows "(mean one = mean two)"
 proof -
   from se le have
     "(\<Sum>:one / real (length one)) = (\<Sum>:two / real (length two))"
     by auto
   thus ?thesis unfolding mean_def .
 qed
 
 lemma list_gmean_gt_iff:
   fixes one::"real list" and two::"real list"
   assumes
     gz1: "\<Prod>:one > 0" and gz2: "\<Prod>:two > 0" and
     ne1: "one \<noteq> []" and ne2: "two \<noteq> []" and
     pe: "(\<Prod>:one > \<Prod>:two)" and
     le: "(length one = length two)"
   shows "(gmean one > gmean two)"
   unfolding gmean_def
   using le ne2 pe by simp
 
 text \<open>This slightly more complicated lemma shows that for every non-empty collection with mean $M$, adding another element $a$ where $a=M$ results in a new list with the same mean $M$.\<close>
 
 lemma list_mean_cons [rule_format]:
   fixes xs::"real list"
   shows "xs \<noteq> [] \<longrightarrow> mean ((mean xs)#xs) = mean xs"
 proof
   assume lne: "xs \<noteq> []"
   obtain len where ld: "len = real (length xs)" by simp
   with lne have lgt0: "len > 0" by simp
   hence lnez: "len \<noteq> 0" by simp
   from lgt0 have l1nez: "len + 1 \<noteq> 0" by simp
   from ld have mean: "mean xs = \<Sum>:xs / len" unfolding mean_def by simp
   with ld of_nat_add of_int_1 mean_def
   have "mean ((mean xs)#xs) = (\<Sum>:xs/len + \<Sum>:xs) / (1+len)"
     by simp
   also from list_sum_distrib_aux[of xs] have
     "\<dots> = (1 + (1/len))*\<Sum>:xs / (1+len)" by simp
   also with lnez have
     "\<dots> = (len + 1)*\<Sum>:xs / (len * (1+len))"
     apply -
     apply (drule mult_divide_mult_cancel_left
       [symmetric, where c="len" and a="(1 + 1 / len) * \<Sum>:xs" and b="1+len"])
     apply (clarsimp simp:field_simps)
     done
   also from l1nez have "\<dots> = \<Sum>:xs / len"
     apply (subst mult.commute [where a="len"])
     apply (drule mult_divide_mult_cancel_left
       [where c="len+1" and a="\<Sum>:xs" and b="len"])
     by (simp add: ac_simps ac_simps)
   finally show "mean ((mean xs)#xs) = mean xs" by (simp add: mean)
 qed
 
 text \<open>For a non-empty collection with positive mean, if we add a positive number to the collection then the mean remains positive.\<close>
 
 lemma mean_gt_0 [rule_format]:
   "xs\<noteq>[] \<and> 0 < x \<and> 0 < (mean xs) \<longrightarrow> 0 < (mean (x#xs))"
 proof
   assume a: "xs \<noteq> [] \<and> 0 < x \<and> 0 < mean xs"
   hence xgt0: "0 < x" and mgt0: "0 < mean xs" by auto
   from a have lxsgt0: "length xs \<noteq> 0" by simp
   from mgt0 have xsgt0: "0 < \<Sum>:xs"
   proof -
     have "mean xs = \<Sum>:xs / real (length xs)" unfolding mean_def by simp
     hence "\<Sum>:xs = mean xs * real (length xs)" by simp
     moreover from lxsgt0 have "real (length xs) > 0" by simp
     moreover with calculation lxsgt0 mgt0 show ?thesis by auto
   qed
   with xgt0 have "\<Sum>:(x#xs) > 0" by simp
   thus "0 < (mean (x#xs))"
   proof -
     assume "0 < \<Sum>:(x#xs)"
     moreover have "real (length (x#xs)) > 0" by simp
     ultimately show ?thesis unfolding mean_def by simp
   qed
 qed
 
 (* ============================================================================= *)
 (* ============================================================================= *)
 (* ============================================================================= *)
 
 subsection \<open>\<open>list_neq\<close>, \<open>list_eq\<close>\<close>
 
 text \<open>This section presents a useful formalisation of the act of removing all the elements from a collection that are equal (not equal) to a particular value. We use this to extract all the non-mean elements from a collection as is required by the proof.\<close>
 
 subsubsection \<open>Definitions\<close>
 
 text \<open>\<open>list_neq\<close> and \<open>list_eq\<close> just extract elements from a collection that are not equal (or equal) to some value.\<close>
 
 abbreviation
   list_neq :: "('a list) \<Rightarrow> 'a \<Rightarrow> ('a list)" where
   "list_neq xs el == filter (\<lambda>x. x\<noteq>el) xs"
 
 abbreviation
   list_eq :: "('a list) \<Rightarrow> 'a \<Rightarrow> ('a list)" where
   "list_eq xs el == filter (\<lambda>x. x=el) xs"
 
 subsubsection \<open>Properties\<close>
 
 text \<open>This lemma just proves a required fact about \<open>list_neq\<close>, {\em remove1} and {\em length}.\<close>
 
 lemma list_neq_remove1 [rule_format]:
   shows "a\<noteq>m \<and> a : set xs
   \<longrightarrow> length (list_neq (remove1 a xs) m) < length (list_neq xs m)"
   (is "?A xs \<longrightarrow> ?B xs" is "?P xs")
 proof (induct xs)
   case Nil show ?case by simp
 next
   case (Cons x xs)
   note \<open>?P xs\<close>
   {
     assume a: "?A (x#xs)"
     hence
       a_ne_m: "a\<noteq>m" and
       a_mem_x_xs: "a : set(x#xs)"
       by auto
     have b: "?B (x#xs)"
     proof cases
       assume "xs = []"
       with a_ne_m a_mem_x_xs show ?thesis
         apply (cases "x=a")
         by auto
     next
       assume xs_ne: "xs \<noteq> []"
       with a_ne_m a_mem_x_xs show ?thesis
       proof cases
         assume "a=x" with a_ne_m show ?thesis by simp
       next
         assume a_ne_x: "a\<noteq>x"
         with a_mem_x_xs have a_mem_xs: "a : set xs" by simp
         with xs_ne a_ne_m Cons have
           rel: "length (list_neq (remove1 a xs) m) < length (list_neq xs m)"
           by simp
         show ?thesis
         proof cases
           assume x_e_m: "x=m"
           with Cons xs_ne a_ne_m a_mem_xs show ?thesis by simp
         next
           assume x_ne_m: "x\<noteq>m"
           from a_ne_x have
             "remove1 a (x#xs) = x#(remove1 a xs)"
             by simp
           hence
             "length (list_neq (remove1 a (x#xs)) m) =
              length (list_neq (x#(remove1 a xs)) m)"
             by simp
           also with x_ne_m have
             "\<dots> = 1 + length (list_neq (remove1 a xs) m)"
             by simp
           finally have
             "length (list_neq (remove1 a (x#xs)) m) =
              1 + length (list_neq (remove1 a xs) m)"
             by simp
           moreover with x_ne_m a_ne_x have
             "length (list_neq (x#xs) m) =
              1 + length (list_neq xs m)"
             by simp
           moreover with rel show ?thesis by simp
         qed
       qed
     qed
   }
   thus "?P (x#xs)" by simp
 qed
 
 text \<open>We now prove some facts about \<open>list_eq\<close>, \<open>list_neq\<close>, length, sum and product.\<close>
 
 lemma list_eq_sum [simp]:
   fixes xs::"real list"
   shows "\<Sum>:(list_eq xs m) = (m * (real (length (list_eq xs m))))"
 apply (induct_tac xs)
 apply simp
 apply (simp add:field_simps)
 done
 
 lemma list_eq_prod [simp]:
   fixes xs::"real list"
   shows "\<Prod>:(list_eq xs m) = (m ^ (length (list_eq xs m)))"
 apply (induct_tac xs)
 apply simp
 apply clarsimp
 done
 
 lemma sum_list_split:
   fixes xs::"real list"
   shows "\<Sum>:xs = (\<Sum>:(list_neq xs m) + \<Sum>:(list_eq xs m))"
 apply (induct xs)
 apply simp
 apply clarsimp
 done
 
 lemma prod_list_split:
   fixes xs::"real list"
   shows "\<Prod>:xs = (\<Prod>:(list_neq xs m) * \<Prod>:(list_eq xs m))"
 apply (induct xs)
 apply simp
 apply clarsimp
 done
 
 lemma sum_list_length_split:
   fixes xs::"real list"
   shows "length xs = length (list_neq xs m) + length (list_eq xs m)"
 apply (induct xs)
 apply simp+
 done
 
 
 
 (* ============================================================================= *)
 (* ============================================================================= *)
 (* ============================================================================= *)
 
 subsection \<open>Element selection\<close>
 
 text \<open>We now show that given after extracting all the elements not equal to the mean there exists one that is greater then (or less than) the mean.\<close>
 
 lemma pick_one_gt:
   fixes xs::"real list" and m::real
   defines m: "m \<equiv> (mean xs)" and neq: "noteq \<equiv> list_neq xs m"
   assumes asum: "noteq\<noteq>[]"
   shows "\<exists>e. e : set noteq \<and> e > m"
 proof (rule ccontr)
   let ?m = "(mean xs)"
   let ?neq = "list_neq xs ?m"
   let ?eq = "list_eq xs ?m"
   from list_eq_sum have "(\<Sum>:?eq) = ?m * (real (length ?eq))" by simp
   from asum have neq_ne: " ?neq \<noteq> []" unfolding m neq .
   assume not_el: "\<not>(\<exists>e. e : set noteq \<and> m < e)"
   hence not_el_exp: "\<not>(\<exists>e. e : set ?neq \<and> ?m < e)" unfolding m neq .
   hence "\<forall>e. \<not>(e : set ?neq) \<or> \<not>(e > ?m)" by simp
   hence "\<forall>e. e : set ?neq \<longrightarrow> \<not>(e > ?m)" by blast
   hence "\<forall>e. e : set ?neq \<longrightarrow> e \<le> ?m" by (simp add: linorder_not_less)
   hence "\<forall>e. e : set ?neq \<longrightarrow> e < ?m" by (simp add:order_le_less)
   with assms sum_list_mono_lt have "(\<Sum>:?neq) < ?m * (real (length ?neq))" by blast
   hence
     "(\<Sum>:?neq) + (\<Sum>:?eq) < ?m * (real (length ?neq)) + (\<Sum>:?eq)" by simp
   also have
     "\<dots> = (?m * ((real (length ?neq) + (real (length ?eq)))))"
       by (simp add:field_simps)
   also have
     "\<dots> = (?m * (real (length xs)))"
       apply (subst of_nat_add [symmetric])
       by (simp add: sum_list_length_split [symmetric])
   also have
     "\<dots> = \<Sum>:xs"
       by (simp add: list_sum_mean [symmetric])
   also from not_el calculation show False by (simp only: sum_list_split [symmetric])
 qed
 
 lemma pick_one_lt:
   fixes xs::"real list" and m::real
   defines m: "m \<equiv> (mean xs)" and neq: "noteq \<equiv> list_neq xs m"
   assumes asum: "noteq\<noteq>[]"
   shows "\<exists>e. e : set noteq \<and> e < m"
 proof (rule ccontr) \<comment> \<open>reductio ad absurdum\<close>
   let ?m = "(mean xs)"
   let ?neq = "list_neq xs ?m"
   let ?eq = "list_eq xs ?m"
   from list_eq_sum have "(\<Sum>:?eq) = ?m * (real (length ?eq))" by simp
   from asum have neq_ne: " ?neq \<noteq> []" unfolding m neq .
   assume not_el: "\<not>(\<exists>e. e : set noteq \<and> m > e)"
   hence not_el_exp: "\<not>(\<exists>e. e : set ?neq \<and> ?m > e)" unfolding m neq .
   hence "\<forall>e. \<not>(e : set ?neq) \<or> \<not>(e < ?m)" by simp
   hence "\<forall>e. e : set ?neq \<longrightarrow> \<not>(e < ?m)" by blast
   hence "\<forall>e. e : set ?neq \<longrightarrow> e \<ge> ?m" by (simp add: linorder_not_less)
   hence "\<forall>e. e : set ?neq \<longrightarrow> e > ?m" by (auto simp: order_le_less)
   with assms sum_list_mono_gt have "(\<Sum>:?neq) > ?m * (real (length ?neq))" by blast
   hence
     "(\<Sum>:?neq) + (\<Sum>:?eq) > ?m * (real (length ?neq)) + (\<Sum>:?eq)" by simp
   also have
     "(?m * (real (length ?neq)) + (\<Sum>:?eq)) =
      (?m * (real (length ?neq)) + (?m * (real (length ?eq))))"
     by simp
   also have
     "\<dots> = (?m * ((real (length ?neq) + (real (length ?eq)))))"
       by (simp add:field_simps)
   also have
     "\<dots> = (?m * (real (length xs)))"
       apply (subst of_nat_add [symmetric])
       by (simp add: sum_list_length_split [symmetric])
   also have
     "\<dots> = \<Sum>:xs"
       by (simp add: list_sum_mean [symmetric])
   also from not_el calculation show False by (simp only: sum_list_split [symmetric])
 qed
 
 (* =================================================================== *)
 (* =================================================================== *)
 (* =================================================================== *)
 (* =================================================================== *)
 
 subsection \<open>Abstract properties\<close>
 
 text \<open>In order to maintain some comprehension of the following proofs we now introduce some properties of collections.\<close>
 
 subsubsection \<open>Definitions\<close>
 
 
 
 
 text \<open>{\em het}: The heterogeneity of a collection is the number of elements not equal to its mean. A heterogeneity of zero implies the all the elements in the collection are the same (i.e. homogeneous).\<close>
 
 definition
   het :: "real list \<Rightarrow> nat" where
   "het l = length (list_neq l (mean l))"
 
 lemma het_gt_0_imp_noteq_ne: "het l > 0 \<Longrightarrow> list_neq l (mean l) \<noteq> []"
   unfolding het_def by simp
 
 lemma het_gt_0I: assumes a: "a \<in> set xs" and b: "b \<in> set xs" and neq: "a \<noteq> b"
   shows "het xs > 0"
 proof (rule ccontr)
   assume "\<not> ?thesis"
   hence "het xs = 0" by auto
   from this[unfolded het_def] have "list_neq xs (mean xs) = []" by simp
   from arg_cong[OF this, of set] have mean: "\<And> x. x \<in> set xs \<Longrightarrow> x = mean xs" by auto
   from mean[OF a] mean[OF b] neq show False by auto
 qed
 
 
 text \<open>\<open>\<gamma>-eq\<close>: Two lists are $\gamma$-equivalent if and only
 if they both have the same number of elements and the same arithmetic
 means.\<close>
 
 definition
   \<gamma>_eq :: "((real list)*(real list)) \<Rightarrow> bool" where
   "\<gamma>_eq a \<longleftrightarrow> mean (fst a) = mean (snd a) \<and> length (fst a) = length (snd a)"
 
 text \<open>\<open>\<gamma>_eq\<close> is transitive and symmetric.\<close>
 
 lemma \<gamma>_eq_sym: "\<gamma>_eq (a,b) = \<gamma>_eq (b,a)"
   unfolding \<gamma>_eq_def by auto
 
 lemma \<gamma>_eq_trans:
   "\<gamma>_eq (x,y) \<Longrightarrow> \<gamma>_eq (y,z) \<Longrightarrow> \<gamma>_eq (x,z)"
   unfolding \<gamma>_eq_def by simp
 
 
 text \<open>{\em pos}: A list is positive if all its elements are greater than 0.\<close>
 
 definition
   pos :: "real list \<Rightarrow> bool" where
   "pos l \<longleftrightarrow> (if l=[] then False else \<forall>e. e : set l \<longrightarrow> e > 0)"
 
 lemma pos_empty [simp]: "pos [] = False" unfolding pos_def by simp
 lemma pos_single [simp]: "pos [x] = (x > 0)" unfolding pos_def by simp
 lemma pos_imp_ne: "pos xs \<Longrightarrow> xs\<noteq>[]" unfolding pos_def by auto
 
 lemma pos_cons [simp]:
   "xs \<noteq> [] \<longrightarrow> pos (x#xs) =
    (if (x>0) then pos xs else False)"
   (is "?P x xs" is "?A xs \<longrightarrow> ?S x xs")
 proof (simp add: if_split, rule impI)
   assume xsne: "xs \<noteq> []"
   hence pxs_simp:
     "pos xs = (\<forall>e. e : set xs \<longrightarrow> e > 0)"
     unfolding pos_def by simp
   show
     "(0 < x \<longrightarrow> pos (x # xs) = pos xs) \<and>
      (\<not> 0 < x \<longrightarrow> \<not> pos (x # xs))"
   proof
     {
       assume xgt0: "0 < x"
       {
         assume pxs: "pos xs"
         with pxs_simp have "\<forall>e. e : set xs \<longrightarrow> e > 0" by simp
         with xgt0 have "\<forall>e. e : set (x#xs) \<longrightarrow> e > 0" by simp
         hence "pos (x#xs)" unfolding pos_def by simp
       }
       moreover
       {
         assume pxxs: "pos (x#xs)"
         hence "\<forall>e. e : set (x#xs) \<longrightarrow> e > 0" unfolding pos_def by simp
         hence "\<forall>e. e : set xs \<longrightarrow> e > 0" by simp
         with xsne have "pos xs" unfolding pos_def by simp
       }
       ultimately have "pos (x # xs) = pos xs"
         apply -
         apply (rule iffI)
         apply auto
         done
     }
     thus "0 < x \<longrightarrow> pos (x # xs) = pos xs" by simp
   next
     {
       assume xngt0: "\<not> (0<x)"
       {
         assume pxs: "pos xs"
         with pxs_simp have "\<forall>e. e : set xs \<longrightarrow> e > 0" by simp
         with xngt0 have "\<not> (\<forall>e. e : set (x#xs) \<longrightarrow> e > 0)" by auto
         hence "\<not> (pos (x#xs))" unfolding pos_def by simp
       }
       moreover
       {
         assume pxxs: "\<not>pos xs"
         with xsne have "\<not> (\<forall>e. e : set xs \<longrightarrow> e > 0)" unfolding pos_def by simp
         hence "\<not> (\<forall>e. e : set (x#xs) \<longrightarrow> e > 0)" by auto
         hence "\<not> (pos (x#xs))" unfolding pos_def by simp
       }
       ultimately have "\<not> pos (x#xs)" by auto
     }
     thus "\<not> 0 < x \<longrightarrow> \<not> pos (x # xs)" by simp
   qed
 qed
 
 subsubsection \<open>Properties\<close>
 
 text \<open>Here we prove some non-trivial properties of the abstract properties.\<close>
 
 text \<open>Two lemmas regarding {\em pos}. The first states the removing
 an element from a positive collection (of more than 1 element) results
 in a positive collection. The second asserts that the mean of a
 positive collection is positive.\<close>
 
 lemma pos_imp_rmv_pos:
   assumes "(remove1 a xs)\<noteq>[]" "pos xs" shows "pos (remove1 a xs)"
 proof -
   from assms have pl: "pos xs" and rmvne: "(remove1 a xs)\<noteq>[]" by auto
   from pl have "xs \<noteq> []" by (rule pos_imp_ne)
   with pl pos_def have "\<forall>x. x : set xs \<longrightarrow> x > 0" by simp
   hence "\<forall>x. x : set (remove1 a xs) \<longrightarrow> x > 0"
     using set_remove1_subset[of _ xs] by(blast)
   with rmvne show "pos (remove1 a xs)" unfolding pos_def by simp
 qed
 
 lemma pos_mean: "pos xs \<Longrightarrow> mean xs > 0"
 proof (induct xs)
   case Nil thus ?case by(simp add: pos_def)
 next
   case (Cons x xs)
   show ?case
   proof cases
     assume xse: "xs = []"
     hence "pos (x#xs) = (x > 0)" by simp
     with Cons(2) have "x>0" by(simp)
     with xse have "0 < mean (x#xs)" by(auto simp:mean_def)
     thus ?thesis by simp
   next
     assume xsne: "xs \<noteq> []"
     show ?thesis
     proof cases
       assume pxs: "pos xs"
       with Cons(1) have z_le_mxs: "0 < mean xs" by(simp)
       {
         assume ass: "x > 0"
         with ass z_le_mxs xsne have "0 < mean (x#xs)"
           apply -
           apply (rule mean_gt_0)
           by simp
       }
       moreover
       {
         from xsne pxs have "0 < x"
         proof cases
           assume "0 < x" thus ?thesis by simp
         next
           assume "\<not>(0 < x)"
           with xsne pos_cons have "pos (x#xs) = False" by simp
           with Cons(2) show ?thesis by simp
         qed
       }
       ultimately have "0 < mean (x#xs)" by simp
       thus ?thesis by simp
     next
       assume npxs: "\<not>pos xs"
       with xsne pos_cons have "pos (x#xs) = False"  by simp
       thus ?thesis using Cons(2) by simp
     qed
   qed
 qed
 
 text \<open>We now show that homogeneity of a non-empty collection $x$
 implies that its product is equal to \<open>(mean x)^(length x)\<close>.\<close>
 
 lemma prod_list_het0:
   shows "x\<noteq>[] \<and> het x = 0 \<Longrightarrow> \<Prod>:x = (mean x) ^ (length x)"
 proof -
   assume "x\<noteq>[] \<and> het x = 0"
   hence xne: "x\<noteq>[]" and hetx: "het x = 0" by auto
   from hetx have lz: "length (list_neq x (mean x)) = 0" unfolding het_def .
   hence "\<Prod>:(list_neq x (mean x)) = 1" by simp
   with prod_list_split have "\<Prod>:x = \<Prod>:(list_eq x (mean x))"
     apply -
     apply (drule meta_spec [of _ x])
     apply (drule meta_spec [of _ "mean x"])
     by simp
   also with list_eq_prod have
     "\<dots> = (mean x) ^ (length (list_eq x (mean x)))" by simp
   also with calculation lz sum_list_length_split have
     "\<Prod>:x = (mean x) ^ (length x)"
     apply -
     apply (drule meta_spec [of _ x])
     apply (drule meta_spec [of _ "mean x"])
     by simp
   thus ?thesis by simp
 qed
 
 text \<open>Furthermore we present an important result - that a
 homogeneous collection has equal geometric and arithmetic means.\<close>
 
 lemma het_base:
   shows "pos x \<and> het x = 0 \<Longrightarrow> gmean x = mean x"
 proof -
   assume ass: "pos x \<and> het x = 0"
   hence
     xne: "x\<noteq>[]" and
     hetx: "het x = 0" and
     posx: "pos x"
     by auto
   from posx pos_mean have mxgt0: "mean x > 0" by simp
   from xne have lxgt0: "length x > 0" by simp
   with ass prod_list_het0 have
     "root (length x) (\<Prod>:x) = root (length x) ((mean x)^(length x))"
     by simp
   also from lxgt0 mxgt0 real_root_power_cancel have "\<dots> = mean x" by auto
   finally show "gmean x = mean x" unfolding gmean_def .
 qed
 
 (* =================================================================== *)
 (* =================================================================== *)
 (* =================================================================== *)
 (* =================================================================== *)
 
 
 subsection \<open>Existence of a new collection\<close>
 
 text \<open>We now present the largest and most important proof in this
 document. Given any positive and non-homogeneous collection of real
 numbers there exists a new collection that is $\gamma$-equivalent,
 positive, has a strictly lower heterogeneity and a greater geometric
 mean.\<close>
 
 lemma new_list_gt_gmean:
   fixes xs :: "real list" and m :: real
   and neq and eq
   defines
     m: "m \<equiv> mean xs" and
     neq: "noteq \<equiv> list_neq xs m" and
     eq: "eq \<equiv> list_eq xs m"
   assumes pos_xs: "pos xs" and het_gt_0: "het xs > 0"
   shows
   "\<exists>xs'. gmean xs' > gmean xs \<and> \<gamma>_eq (xs',xs) \<and>
           het xs' < het xs \<and> pos xs'"
 proof -
   from pos_xs pos_imp_ne have
     pos_els: "\<forall>y. y : set xs \<longrightarrow> y > 0" by (unfold pos_def, simp)
   with el_gt0_imp_prod_gt0[of xs] have pos_asm: "\<Prod>:xs > 0" by simp
   from neq het_gt_0 het_gt_0_imp_noteq_ne m have
     neqne: "noteq \<noteq> []" by simp
 
   txt \<open>Pick two elements from xs, one greater than m, one less than m.\<close>
   from assms pick_one_gt neqne obtain \<alpha> where
     \<alpha>_def: "\<alpha> : set noteq \<and> \<alpha> > m" unfolding neq m by auto
   from assms pick_one_lt neqne obtain \<beta> where
     \<beta>_def: "\<beta> : set noteq \<and> \<beta> < m" unfolding neq m by auto
   from \<alpha>_def \<beta>_def have \<alpha>_gt: "\<alpha> > m" and \<beta>_lt: "\<beta> < m" by auto
   from \<alpha>_def \<beta>_def have el_neq: "\<beta> \<noteq> \<alpha>" by simp
   from neqne neq have xsne: "xs \<noteq> []" by auto
 
   from \<beta>_def have \<beta>_mem: "\<beta> : set xs" by (auto simp: neq)
   from \<alpha>_def have \<alpha>_mem: "\<alpha> : set xs" by (auto simp: neq)
 
   from pos_xs pos_def xsne \<alpha>_mem \<beta>_mem \<alpha>_def \<beta>_def have
     \<alpha>_pos: "\<alpha> > 0" and \<beta>_pos: "\<beta> > 0" by auto
 
   \<comment> \<open>remove these elements from xs, and insert two new elements\<close>
   obtain left_over where lo: "left_over = (remove1 \<beta> (remove1 \<alpha> xs))" by simp
   obtain b where bdef: "m + b = \<alpha> + \<beta>"
     by (drule meta_spec [of _ "\<alpha> + \<beta> - m"], simp)
 
   from m pos_xs pos_def pos_mean have m_pos: "m > 0" by simp
   with bdef \<alpha>_pos \<beta>_pos \<alpha>_gt \<beta>_lt have b_pos: "b > 0" by simp
 
   obtain new_list where nl: "new_list = m#b#(left_over)" by auto
 
   from el_neq \<beta>_mem \<alpha>_mem have "\<beta> : set xs \<and> \<alpha> : set xs \<and> \<beta> \<noteq> \<alpha>" by simp
   hence "\<alpha> : set (remove1 \<beta> xs) \<and> \<beta> : set(remove1 \<alpha> xs)" by (auto simp add: in_set_remove1)
   moreover hence "(remove1 \<alpha> xs) \<noteq> [] \<and> (remove1 \<beta> xs) \<noteq> []" by (auto)
   ultimately have
     mem : "\<alpha> : set(remove1 \<beta> xs) \<and> \<beta> : set(remove1 \<alpha> xs) \<and>
           (remove1 \<alpha> xs) \<noteq> [] \<and> (remove1 \<beta> xs) \<noteq> []" by simp
   \<comment> \<open>prove that new list is positive\<close>
   from nl have nl_pos: "pos new_list"
   proof cases
     assume "left_over = []"
     with nl b_pos m_pos show ?thesis by simp
   next
     assume lone: "left_over \<noteq> []"
     from mem pos_imp_rmv_pos pos_xs have "pos (remove1 \<alpha> xs)" by simp
     with lo lone pos_imp_rmv_pos have "pos left_over" by simp
     with lone mem nl m_pos b_pos show ?thesis by simp
   qed
 
   \<comment> \<open>now show that the new list has the same mean as the old list\<close>
   with mem nl lo bdef \<alpha>_mem \<beta>_mem
     have "\<Sum>:new_list = \<Sum>:xs"
       apply clarsimp
       apply (subst sum_list_rmv1)
         apply simp
       apply (subst sum_list_rmv1)
         apply simp
       apply clarsimp
     done
   moreover from lo nl \<beta>_mem \<alpha>_mem mem have
     leq: "length new_list = length xs"
     apply -
     apply (erule conjE)+
     apply (clarsimp)
     apply (subst length_remove1, simp)
     apply (simp add: length_remove1)
     apply (auto dest!:length_pos_if_in_set)
     done
   ultimately have eq_mean: "mean new_list = mean xs" by (rule list_mean_eq_iff)
 
   \<comment> \<open>finally show that the new list has a greater gmean than the old list\<close>
   have gt_gmean: "gmean new_list > gmean xs"
   proof -
     from bdef \<alpha>_gt \<beta>_lt have "abs (m - b) < abs (\<alpha> - \<beta>)" by arith
     moreover from bdef have "m+b = \<alpha>+\<beta>" .
     ultimately have mb_gt_gt: "m*b > \<alpha>*\<beta>" by (rule le_diff_imp_gt_prod)
     moreover from nl have
       "\<Prod>:new_list = \<Prod>:left_over * (m*b)" by auto
     moreover
     from lo \<alpha>_mem \<beta>_mem mem remove1_retains_prod[where 'a = real] have
       xsprod: "\<Prod>:xs = \<Prod>:left_over * (\<alpha>*\<beta>)" by auto
     moreover from xsne have
       "xs \<noteq> []" .
     moreover from nl have
       nlne: "new_list \<noteq> []" by simp
     moreover from pos_asm lo have
       "\<Prod>:left_over > 0"
       proof -
         from pos_asm have "\<Prod>:xs > 0" .
         moreover
         from xsprod have "\<Prod>:xs = \<Prod>:left_over * (\<alpha>*\<beta>)" .
         ultimately have "\<Prod>:left_over * (\<alpha>*\<beta>) > 0" by simp
         moreover
         from pos_els \<alpha>_mem \<beta>_mem have "\<alpha> > 0" and "\<beta> > 0" by auto
         hence "\<alpha>*\<beta> > 0" by simp
         ultimately show "\<Prod>:left_over > 0"
           apply -
           apply (rule zero_less_mult_pos2 [where a="(\<alpha> * \<beta>)"])
           by auto
       qed
     ultimately have "\<Prod>:new_list > \<Prod>:xs"
       by simp
     moreover with pos_asm nl have "\<Prod>:new_list > 0" by auto
     moreover from calculation pos_asm xsne nlne leq list_gmean_gt_iff
     show "gmean new_list > gmean xs" by simp
   qed
 
   \<comment> \<open>auxiliary info\<close>
   from \<beta>_lt have \<beta>_ne_m: "\<beta> \<noteq> m" by simp
   from mem have
     \<beta>_mem_rmv_\<alpha>: "\<beta> : set (remove1 \<alpha> xs)" and rmv_\<alpha>_ne: "(remove1 \<alpha> xs) \<noteq> []" by auto
 
   from \<alpha>_def have \<alpha>_ne_m: "\<alpha> \<noteq> m" by simp
 
   \<comment> \<open>now show that new list is more homogeneous\<close>
   have lt_het: "het new_list < het xs"
   proof cases
     assume bm: "b=m"
     with het_def have
       "het new_list = length (list_neq new_list (mean new_list))"
       by simp
     also with m nl eq_mean have
       "\<dots> = length (list_neq (m#b#(left_over)) m)"
       by simp
     also with bm have
       "\<dots> = length (list_neq left_over m)"
       by simp
     also with lo \<beta>_def \<alpha>_def have
       "\<dots> = length (list_neq (remove1 \<beta> (remove1 \<alpha> xs)) m)"
       by simp
     also from \<beta>_ne_m \<beta>_mem_rmv_\<alpha> rmv_\<alpha>_ne have
       "\<dots> < length (list_neq (remove1 \<alpha> xs) m)"
       apply -
       apply (rule list_neq_remove1)
       by simp
     also from \<alpha>_mem \<alpha>_ne_m xsne have
       "\<dots> < length (list_neq xs m)"
       apply -
       apply (rule list_neq_remove1)
       by simp
     also with m het_def have "\<dots> = het xs" by simp
     finally show "het new_list < het xs" .
   next
     assume bnm: "b\<noteq>m"
     with het_def have
       "het new_list = length (list_neq new_list (mean new_list))"
       by simp
     also with m nl eq_mean have
       "\<dots> = length (list_neq (m#b#(left_over)) m)"
       by simp
     also with bnm have
       "\<dots> = length (b#(list_neq left_over m))"
       by simp
     also have
       "\<dots> = 1 + length (list_neq left_over m)"
       by simp
     also with lo \<beta>_def \<alpha>_def have
       "\<dots> = 1 + length (list_neq (remove1 \<beta> (remove1 \<alpha> xs)) m)"
       by simp
     also from \<beta>_ne_m \<beta>_mem_rmv_\<alpha> rmv_\<alpha>_ne have
       "\<dots> < 1 + length (list_neq (remove1 \<alpha> xs) m)"
       apply -
       apply (simp only: nat_add_left_cancel_less)
       apply (rule list_neq_remove1)
       by simp
     finally have
       "het new_list \<le> length (list_neq (remove1 \<alpha> xs) m)"
       by simp
     also from \<alpha>_mem \<alpha>_ne_m xsne have "\<dots> < length (list_neq xs m)"
       apply -
       apply (rule list_neq_remove1)
       by simp
     also with m het_def have "\<dots> = het xs" by simp
     finally show "het new_list < het xs" .
   qed
 
       \<comment> \<open>thus thesis by existence of newlist\<close>
   from \<gamma>_eq_def lt_het gt_gmean eq_mean leq nl_pos show ?thesis by auto
 qed
 
 
 text \<open>Furthermore we show that for all non-homogeneous positive
 collections there exists another collection that is
 $\gamma$-equivalent, positive, has a greater geometric mean {\em and}
 is homogeneous.\<close>
 
 lemma existence_of_het0 [rule_format]:
   shows "\<forall>x. p = het x \<and> p > 0 \<and> pos x \<longrightarrow>
   (\<exists>y. gmean y > gmean x \<and> \<gamma>_eq (x,y) \<and> het y = 0 \<and> pos y)"
   (is "?Q p" is "\<forall>x. (?A x p \<longrightarrow> ?S x)")
 proof (induct p rule: nat_less_induct)
   fix n
   assume ind: "\<forall>m<n. ?Q m"
   {
     fix x
     assume ass: "?A x n"
     hence "het x > 0" and "pos x" by auto
     with new_list_gt_gmean have
       "\<exists>y. gmean y > gmean x \<and> \<gamma>_eq (x,y) \<and> het y < het x \<and> pos y"
       apply - 
       apply (drule meta_spec [of _ x])
       apply (drule meta_mp)
         apply assumption
       apply (drule meta_mp)
         apply assumption
       apply (subst(asm) \<gamma>_eq_sym)
       apply simp
       done
     then obtain \<beta> where
       \<beta>_def: "gmean \<beta> > gmean x \<and> \<gamma>_eq (x,\<beta>) \<and> het \<beta> < het x \<and> pos \<beta>" ..
     then obtain b where bdef: "b = het \<beta>" by simp
     with ass \<beta>_def have "b < n" by auto
     with ind have "?Q b" by simp
     with \<beta>_def have
       ind2: "b = het \<beta> \<and> 0 < b \<and> pos \<beta> \<longrightarrow>
       (\<exists>y. gmean \<beta> < gmean y \<and> \<gamma>_eq (\<beta>, y) \<and> het y = 0 \<and> pos y)" by simp
     {
       assume "\<not>(0<b)"
       hence "b=0" by simp
       with bdef have "het \<beta> = 0" by simp
       with \<beta>_def have "?S x" by auto
     }
     moreover
     {
       assume "0 < b"
       with bdef ind2 \<beta>_def have "?S \<beta>" by simp
       then obtain \<gamma> where
         "gmean \<beta> < gmean \<gamma> \<and> \<gamma>_eq (\<beta>, \<gamma>) \<and> het \<gamma> = 0 \<and> pos \<gamma>" ..
       with \<beta>_def have "gmean x < gmean \<gamma> \<and> \<gamma>_eq (x,\<gamma>) \<and> het \<gamma> = 0 \<and> pos \<gamma>"
         apply clarsimp
         apply (rule \<gamma>_eq_trans)
         by auto
       hence "?S x" by auto
     }
     ultimately have "?S x" by auto
   }
   thus "?Q n" by simp
 qed
 
 
 subsection \<open>Cauchy's Mean Theorem\<close>
 
 text \<open>We now present the final proof of the theorem. For any
 positive collection we show that its geometric mean is less than or
 equal to its arithmetic mean.\<close>
 
 theorem CauchysMeanTheorem:
   fixes z::"real list"
   assumes "pos z"
   shows "gmean z \<le> mean z"
 proof -
   from \<open>pos z\<close> have zne: "z\<noteq>[]" by (rule pos_imp_ne)
   show "gmean z \<le> mean z"
   proof cases
     assume "het z = 0"
     with \<open>pos z\<close> zne het_base have "gmean z = mean z" by simp
     thus ?thesis by simp
   next
     assume "het z \<noteq> 0"
     hence "het z > 0" by simp
     moreover obtain k where "k = het z" by simp
     moreover with calculation \<open>pos z\<close> existence_of_het0 have
       "\<exists>y. gmean y > gmean z \<and> \<gamma>_eq (z,y) \<and> het y = 0 \<and> pos y" by auto
     then obtain \<alpha> where
       "gmean \<alpha> > gmean z \<and> \<gamma>_eq (z,\<alpha>) \<and> het \<alpha> = 0 \<and> pos \<alpha>" ..
     with het_base \<gamma>_eq_def pos_imp_ne have
       "mean z = mean \<alpha>" and
       "gmean \<alpha> > gmean z" and
       "gmean \<alpha> = mean \<alpha>" by auto
     hence "gmean z < mean z" by simp
     thus ?thesis by simp
   qed
 qed
 
 text \<open>In the equality version we prove that the geometric mean
   is identical to the arithmetic mean iff the collection is 
   homogeneous.\<close>
 theorem CauchysMeanTheorem_Eq:
   fixes z::"real list"
   assumes "pos z"
   shows "gmean z = mean z \<longleftrightarrow> het z = 0"
 proof 
   assume "het z = 0"
   with het_base[of z] \<open>pos z\<close> show "gmean z = mean z" by auto
 next
   assume eq: "gmean z = mean z"
   show "het z = 0"
   proof (rule ccontr)
     assume "het z \<noteq> 0"
     hence "het z > 0" by auto
     moreover obtain k where "k = het z" by simp
     moreover with calculation \<open>pos z\<close> existence_of_het0 have
       "\<exists>y. gmean y > gmean z \<and> \<gamma>_eq (z,y) \<and> het y = 0 \<and> pos y" by auto
     then obtain \<alpha> where
       "gmean \<alpha> > gmean z \<and> \<gamma>_eq (z,\<alpha>) \<and> het \<alpha> = 0 \<and> pos \<alpha>" ..
     with het_base \<gamma>_eq_def pos_imp_ne have
       "mean z = mean \<alpha>" and
       "gmean \<alpha> > gmean z" and
       "gmean \<alpha> = mean \<alpha>" by auto
     hence "gmean z < mean z" by simp
     thus False using eq by auto
   qed
 qed
  
 corollary CauchysMeanTheorem_Less:
   fixes z::"real list"
   assumes "pos z" and "het z > 0"
   shows "gmean z < mean z"
   using 
     CauchysMeanTheorem[OF \<open>pos z\<close>] 
     CauchysMeanTheorem_Eq[OF \<open>pos z\<close>]
     \<open>het z > 0\<close>
     by auto
 
 end
diff --git a/thys/HereditarilyFinite/HF.thy b/thys/HereditarilyFinite/HF.thy
--- a/thys/HereditarilyFinite/HF.thy
+++ b/thys/HereditarilyFinite/HF.thy
@@ -1,1107 +1,1107 @@
 chapter \<open>The Hereditarily Finite Sets\<close>
 
 theory HF
 imports "HOL-Library.Nat_Bijection"
 abbrevs "<:" = "\<^bold>\<in>"
   and "~<:" = "\<^bold>\<notin>"
 begin
 
 text \<open>From "Finite sets and Gödel's Incompleteness Theorems" by S. Swierczkowski.
       Thanks for Brian Huffman for this development, up to the cases and induct rules.\<close>
 
 section \<open>Basic Definitions and Lemmas\<close>
 
 typedef hf = "UNIV :: nat set" ..
 
 definition hfset :: "hf \<Rightarrow> hf set"
   where "hfset a = Abs_hf ` set_decode (Rep_hf a)"
 
 definition HF :: "hf set \<Rightarrow> hf"
   where "HF A = Abs_hf (set_encode (Rep_hf ` A))"
 
 definition hinsert :: "hf \<Rightarrow> hf \<Rightarrow> hf"
   where "hinsert a b = HF (insert a (hfset b))"
 
 definition hmem :: "hf \<Rightarrow> hf \<Rightarrow> bool"  (infixl "\<^bold>\<in>" 50)
   where "hmem a b \<longleftrightarrow> a \<in> hfset b"
   
 abbreviation not_hmem :: "hf \<Rightarrow> hf \<Rightarrow> bool"  (infixl "\<^bold>\<notin>" 50)
   where "a \<^bold>\<notin> b \<equiv> \<not> a \<^bold>\<in> b"
 
 notation (ASCII)
   hmem (infixl "<:" 50)
 
 instantiation hf :: zero
 begin
   definition Zero_hf_def: "0 = HF {}"
   instance ..
 end
 
 lemma Abs_hf_0 [simp]: "Abs_hf 0 = 0"
   by (simp add: HF_def Zero_hf_def)
 
 
 text \<open>HF Set enumerations\<close>
 
 abbreviation inserthf :: "hf \<Rightarrow> hf \<Rightarrow> hf"  (infixl "\<triangleleft>" 60)
   where "y \<triangleleft> x \<equiv> hinsert x y"
 
 syntax (ASCII)
   "_HFinset" :: "args \<Rightarrow> hf"      ("{|(_)|}")
 syntax
   "_HFinset" :: "args \<Rightarrow> hf"      ("\<lbrace>_\<rbrace>")
 translations
   "\<lbrace>x, y\<rbrace>" \<rightleftharpoons> "\<lbrace>y\<rbrace> \<triangleleft> x"
   "\<lbrace>x\<rbrace>"    \<rightleftharpoons> "0 \<triangleleft> x"
 
 lemma finite_hfset [simp]: "finite (hfset a)"
   unfolding hfset_def by simp
 
 lemma HF_hfset [simp]: "HF (hfset a) = a"
   unfolding HF_def hfset_def
   by (simp add: image_image Abs_hf_inverse Rep_hf_inverse)
 
 lemma hfset_HF [simp]: "finite A \<Longrightarrow> hfset (HF A) = A"
   unfolding HF_def hfset_def
   by (simp add: image_image Abs_hf_inverse Rep_hf_inverse)
 
 lemma inj_on_HF: "inj_on HF (Collect finite)"
   by (metis hfset_HF inj_onI mem_Collect_eq)
 
 lemma hmem_hempty [simp]: "a \<^bold>\<notin> 0"
   unfolding hmem_def Zero_hf_def by simp
 
 lemmas hemptyE [elim!] = hmem_hempty [THEN notE]
 
 lemma hmem_hinsert [iff]:
   "hmem a (c \<triangleleft> b) \<longleftrightarrow> a = b \<or> a \<^bold>\<in> c"
   unfolding hmem_def hinsert_def by simp
 
 lemma hf_ext: "a = b \<longleftrightarrow> (\<forall>x. x \<^bold>\<in> a \<longleftrightarrow> x \<^bold>\<in> b)"
   unfolding hmem_def set_eq_iff [symmetric]
   by (metis HF_hfset)
 
 lemma finite_cases [consumes 1, case_names empty insert]:
   "\<lbrakk>finite F; F = {} \<Longrightarrow> P; \<And>A x. \<lbrakk>F = insert x A; x \<notin> A; finite A\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
 by (induct F rule: finite_induct, simp_all)
 
 lemma hf_cases [cases type: hf, case_names 0 hinsert]:
   obtains "y = 0" | a b where "y = b \<triangleleft> a" and "a \<^bold>\<notin> b"
 proof -
   have "finite (hfset y)" by (rule finite_hfset)
   thus thesis
     by (metis Zero_hf_def finite_cases hf_ext hfset_HF hinsert_def hmem_def that)
 qed
 
 lemma Rep_hf_hinsert:
   "a \<^bold>\<notin> b \<Longrightarrow> Rep_hf (hinsert a b) = 2 ^ (Rep_hf a) + Rep_hf b"
   unfolding hinsert_def HF_def hfset_def
   apply (simp add: image_image Abs_hf_inverse Rep_hf_inverse)
   apply (subst set_encode_insert, simp)
   apply (clarsimp simp add: hmem_def hfset_def image_def
     Rep_hf_inject [symmetric] Abs_hf_inverse, simp)
   done
 
 lemma less_two_power: "n < 2 ^ n"
   by (induct n, auto)
 
 
 section \<open>Verifying the Axioms of HF\<close>
 
 text \<open>HF1\<close>
 lemma hempty_iff: "z=0 \<longleftrightarrow> (\<forall>x. x \<^bold>\<notin> z)"
   by (simp add: hf_ext)
 
 text \<open>HF2\<close>
 lemma hinsert_iff: "z = x \<triangleleft> y \<longleftrightarrow> (\<forall>u. u \<^bold>\<in> z \<longleftrightarrow> u \<^bold>\<in> x \<or> u = y)"
   by (auto simp: hf_ext)
 
 text \<open>HF induction\<close>
 lemma hf_induct [induct type: hf, case_names 0 hinsert]:
   assumes [simp]: "P 0"
                   "\<And>x y. \<lbrakk>P x; P y; x \<^bold>\<notin> y\<rbrakk> \<Longrightarrow> P (y \<triangleleft> x)"
   shows "P z"
 proof (induct z rule: wf_induct [where r="measure Rep_hf", OF wf_measure])
   case (1 x) show ?case
     proof (cases x rule: hf_cases)
       case 0 thus ?thesis by simp
     next
       case (hinsert a b)
       thus ?thesis using 1
         by (simp add: Rep_hf_hinsert
                       less_le_trans [OF less_two_power le_add1])
     qed
 qed
 
 text \<open>HF3\<close>
 lemma hf_induct_ax: "\<lbrakk>P 0; \<forall>x. P x \<longrightarrow> (\<forall>y. P y \<longrightarrow> P (x \<triangleleft> y))\<rbrakk> \<Longrightarrow> P x"
   by (induct x, auto)
 
 lemma hf_equalityI [intro]: "(\<And>x. x \<^bold>\<in> a \<longleftrightarrow> x \<^bold>\<in> b) \<Longrightarrow> a = b"
   by (simp add: hf_ext)
 
 lemma hinsert_nonempty [simp]: "A \<triangleleft> a \<noteq> 0"
   by (auto simp: hf_ext)
 
 lemma hinsert_commute: "(z \<triangleleft> y) \<triangleleft> x = (z \<triangleleft> x) \<triangleleft> y"
   by (auto simp: hf_ext)
 
 lemma hmem_HF_iff [simp]: "x \<^bold>\<in> HF A \<longleftrightarrow> x \<in> A \<and> finite A"
   apply (cases "finite A", auto)
   apply (simp add: hmem_def)
   apply (simp add: hmem_def)
   apply (metis HF_def Rep_hf_inject Abs_hf_0 finite_imageD hempty_iff inj_onI set_encode_inf)
   done
 
 
 section \<open>Ordered Pairs, from ZF/ZF.thy\<close>
 
 lemma singleton_eq_iff [iff]: "\<lbrace>a\<rbrace> = \<lbrace>b\<rbrace> \<longleftrightarrow> a=b"
   by (metis hmem_hempty hmem_hinsert)
 
 lemma doubleton_eq_iff: "\<lbrace>a,b\<rbrace> = \<lbrace>c,d\<rbrace> \<longleftrightarrow> (a=c \<and> b=d) \<or> (a=d \<and> b=c)"
   by auto (metis hmem_hempty hmem_hinsert)+
 
 definition hpair :: "hf \<Rightarrow> hf \<Rightarrow> hf"
   where "hpair a b = \<lbrace>\<lbrace>a\<rbrace>,\<lbrace>a,b\<rbrace>\<rbrace>"
 
 definition hfst :: "hf \<Rightarrow> hf"
   where "hfst p \<equiv> THE x. \<exists>y. p = hpair x y"
 
 definition hsnd :: "hf \<Rightarrow> hf"
   where "hsnd p \<equiv> THE y. \<exists>x. p = hpair x y"
 
 definition hsplit :: "[[hf, hf] \<Rightarrow> 'a, hf] \<Rightarrow> 'a::{}"  \<comment> \<open>for pattern-matching\<close>
   where "hsplit c \<equiv> \<lambda>p. c (hfst p) (hsnd p)"
 
 text \<open>Ordered Pairs, from ZF/ZF.thy\<close>
 
 nonterminal hfs
 syntax (ASCII)
   "_Tuple"    :: "[hf, hfs] \<Rightarrow> hf"              ("<(_,/ _)>")
   "_hpattern" :: "[pttrn, patterns] \<Rightarrow> pttrn"   ("<_,/ _>")
 syntax
   ""          :: "hf \<Rightarrow> hfs"                    ("_")
   "_Enum"     :: "[hf, hfs] \<Rightarrow> hfs"             ("_,/ _")
   "_Tuple"    :: "[hf, hfs] \<Rightarrow> hf"              ("\<langle>(_,/ _)\<rangle>")
   "_hpattern" :: "[pttrn, patterns] \<Rightarrow> pttrn"   ("\<langle>_,/ _\<rangle>")
 translations
   "<x, y, z>"    \<rightleftharpoons> "<x, <y, z>>"
   "<x, y>"       \<rightleftharpoons> "CONST hpair x y"
   "<x, y, z>"    \<rightleftharpoons> "<x, <y, z>>"
   "\<lambda><x,y,zs>. b" \<rightleftharpoons> "CONST hsplit(\<lambda>x <y,zs>. b)"
   "\<lambda><x,y>. b"    \<rightleftharpoons> "CONST hsplit(\<lambda>x y. b)"
 
 
 lemma hpair_def': "hpair a b = \<lbrace>\<lbrace>a,a\<rbrace>,\<lbrace>a,b\<rbrace>\<rbrace>"
   by (auto simp: hf_ext hpair_def)
 
 lemma hpair_iff [simp]: "hpair a b = hpair a' b' \<longleftrightarrow> a=a' \<and> b=b'"
   by (auto simp: hpair_def' doubleton_eq_iff)
 
 lemmas hpair_inject = hpair_iff [THEN iffD1, THEN conjE, elim!]
 
 lemma hfst_conv [simp]: "hfst \<langle>a,b\<rangle> = a"
   by (simp add: hfst_def)
 
 lemma hsnd_conv [simp]: "hsnd \<langle>a,b\<rangle> = b"
   by (simp add: hsnd_def)
 
 lemma hsplit [simp]: "hsplit c \<langle>a,b\<rangle> = c a b"
   by (simp add: hsplit_def)
 
 
 section \<open>Unions, Comprehensions, Intersections\<close>
 
 subsection \<open>Unions\<close>
 
 text \<open>Theorem 1.5 (Existence of the union of two sets).\<close>
 lemma binary_union: "\<exists>z. \<forall>u. u \<^bold>\<in> z \<longleftrightarrow> u \<^bold>\<in> x \<or> u \<^bold>\<in> y"
 proof (induct x rule: hf_induct)
   case 0 thus ?case by auto
 next
   case (hinsert a b) thus ?case by (metis hmem_hinsert)
 qed
 
 text \<open>Theorem 1.6 (Existence of the union of a set of sets).\<close>
 lemma union_of_set: "\<exists>z. \<forall>u. u \<^bold>\<in> z \<longleftrightarrow> (\<exists>y. y \<^bold>\<in> x \<and> u \<^bold>\<in> y)"
 proof (induct x rule: hf_induct)
   case 0 thus ?case by (metis hmem_hempty)
 next
   case (hinsert a b)
   then show ?case
     by (metis hmem_hinsert binary_union [of a])
 qed
 
 
 subsection \<open>Set comprehensions\<close>
 
 text \<open>Theorem 1.7, comprehension scheme\<close>
 lemma comprehension: "\<exists>z. \<forall>u. u \<^bold>\<in> z \<longleftrightarrow> u \<^bold>\<in> x \<and> P u"
 proof (induct x rule: hf_induct)
   case 0 thus ?case by (metis hmem_hempty)
 next
   case (hinsert a b) thus ?case by (metis hmem_hinsert)
 qed
 
 definition HCollect :: "(hf \<Rightarrow> bool) \<Rightarrow> hf \<Rightarrow> hf" \<comment> \<open>comprehension\<close>
   where "HCollect P A = (THE z. \<forall>u. u \<^bold>\<in> z = (P u \<and> u \<^bold>\<in> A))"
 
 syntax (ASCII)
   "_HCollect" :: "idt \<Rightarrow> hf \<Rightarrow> bool \<Rightarrow> hf"    ("(1\<lbrace>_ <:/ _./ _\<rbrace>)")
 syntax
   "_HCollect" :: "idt \<Rightarrow> hf \<Rightarrow> bool \<Rightarrow> hf"    ("(1\<lbrace>_ \<^bold>\<in>/ _./ _\<rbrace>)")
 translations
   "\<lbrace>x \<^bold>\<in> A. P\<rbrace>" \<rightleftharpoons> "CONST HCollect (\<lambda>x. P) A"
 
 lemma HCollect_iff [iff]: "hmem x (HCollect P A) \<longleftrightarrow> P x \<and> x \<^bold>\<in> A"
 apply (insert comprehension [of A P], clarify)
 apply (simp add: HCollect_def)
 apply (rule theI2, blast)
 apply (auto simp: hf_ext)
 done
 
 lemma HCollectI: "a \<^bold>\<in> A \<Longrightarrow> P a \<Longrightarrow> hmem a \<lbrace>x \<^bold>\<in> A. P x\<rbrace>"
   by simp
 
 lemma HCollectE:
   assumes "a \<^bold>\<in> \<lbrace>x \<^bold>\<in> A. P x\<rbrace>" obtains "a \<^bold>\<in> A" "P a"
   using assms by auto
 
 lemma HCollect_hempty [simp]: "HCollect P 0 = 0"
   by (simp add: hf_ext)
 
 
 subsection \<open>Union operators\<close>
 
 instantiation hf :: sup
 begin
   definition "sup a b = (THE z. \<forall>u. u \<^bold>\<in> z \<longleftrightarrow> u \<^bold>\<in> a \<or> u \<^bold>\<in> b)"
   instance ..
 end
 
 abbreviation hunion :: "hf \<Rightarrow> hf \<Rightarrow> hf" (infixl "\<squnion>" 65) where
   "hunion \<equiv> sup"
 
 lemma hunion_iff [iff]: "hmem x (a \<squnion> b) \<longleftrightarrow> x \<^bold>\<in> a \<or> x \<^bold>\<in> b"
 apply (insert binary_union [of a b], clarify)
 apply (simp add: sup_hf_def)
 apply (rule theI2)
 apply (auto simp: hf_ext)
 done
 
 definition HUnion :: "hf \<Rightarrow> hf"        ("\<Squnion>_" [900] 900)
   where "HUnion A = (THE z. \<forall>u. u \<^bold>\<in> z \<longleftrightarrow> (\<exists>y. y \<^bold>\<in> A \<and> u \<^bold>\<in> y))"
 
 lemma HUnion_iff [iff]: "hmem x (\<Squnion> A) \<longleftrightarrow> (\<exists>y. y \<^bold>\<in> A \<and> x \<^bold>\<in> y)"
 apply (insert union_of_set [of A], clarify)
 apply (simp add: HUnion_def)
 apply (rule theI2)
 apply (auto simp: hf_ext)
 done
 
 lemma HUnion_hempty [simp]: "\<Squnion> 0 = 0"
   by (simp add: hf_ext)
 
 lemma HUnion_hinsert [simp]: "\<Squnion>(A \<triangleleft> a) = a \<squnion> \<Squnion>A"
   by (auto simp: hf_ext)
 
 lemma HUnion_hunion [simp]: "\<Squnion>(A \<squnion> B) =  \<Squnion>A \<squnion> \<Squnion>B"
   by blast
 
 
 subsection \<open>Definition 1.8, Intersections\<close>
 
 instantiation hf :: inf
 begin
   definition "inf a b = \<lbrace>x \<^bold>\<in> a. x \<^bold>\<in> b\<rbrace>"
   instance ..
 end
 
 abbreviation hinter :: "hf \<Rightarrow> hf \<Rightarrow> hf" (infixl "\<sqinter>" 70) where
   "hinter \<equiv> inf"
 
 lemma hinter_iff [iff]: "hmem u (x \<sqinter> y) \<longleftrightarrow> u \<^bold>\<in> x \<and> u \<^bold>\<in> y"
   by (metis HCollect_iff inf_hf_def)
 
 definition HInter :: "hf \<Rightarrow> hf"           ("\<Sqinter>_" [900] 900)
   where "HInter(A) = \<lbrace>x \<^bold>\<in> HUnion(A). \<forall>y. y \<^bold>\<in> A \<longrightarrow> x \<^bold>\<in> y\<rbrace>"
 
 lemma HInter_hempty [iff]: "\<Sqinter> 0 = 0"
   by (metis HCollect_hempty HUnion_hempty HInter_def)
 
 lemma HInter_iff [simp]: "A\<noteq>0 \<Longrightarrow> hmem x (\<Sqinter> A) \<longleftrightarrow> (\<forall>y. y \<^bold>\<in> A \<longrightarrow> x \<^bold>\<in> y)"
   by (auto simp: HInter_def)
 
 lemma HInter_hinsert [simp]: "A\<noteq>0 \<Longrightarrow> \<Sqinter>(A \<triangleleft> a) = a \<sqinter> \<Sqinter>A"
   by (auto simp: hf_ext HInter_iff [OF hinsert_nonempty])
 
 
 subsection \<open>Set Difference\<close>
 
 instantiation hf :: minus
 begin
   definition "A - B = \<lbrace>x \<^bold>\<in> A. x \<^bold>\<notin> B\<rbrace>"
   instance ..
 end
 
 lemma hdiff_iff [iff]: "hmem u (x - y) \<longleftrightarrow> u \<^bold>\<in> x \<and> u \<^bold>\<notin> y"
   by (auto simp: minus_hf_def)
 
 lemma hdiff_zero [simp]: fixes x :: hf shows "(x - 0) = x"
   by blast
 
 lemma zero_hdiff [simp]: fixes x :: hf shows "(0 - x) = 0"
   by blast
 
 lemma hdiff_insert: "A - (B \<triangleleft> a) = A - B - \<lbrace>a\<rbrace>"
   by blast
 
 lemma hinsert_hdiff_if:
   "(A \<triangleleft> x) - B = (if x \<^bold>\<in> B then A - B else (A - B) \<triangleleft> x)"
   by auto
 
 
 section \<open>Replacement\<close>
 
 text \<open>Theorem 1.9 (Replacement Scheme).\<close>
 lemma replacement:
   "(\<forall>u v v'. u \<^bold>\<in> x \<longrightarrow> R u v \<longrightarrow> R u v' \<longrightarrow> v'=v) \<Longrightarrow> \<exists>z. \<forall>v. v \<^bold>\<in> z \<longleftrightarrow> (\<exists>u. u \<^bold>\<in> x \<and> R u v)"
 proof (induct x rule: hf_induct)
   case 0 thus ?case
     by (metis hmem_hempty)
 next
   case (hinsert a b) thus ?case
     by simp (metis hmem_hinsert)
 qed
 
 lemma replacement_fun: "\<exists>z. \<forall>v. v \<^bold>\<in> z \<longleftrightarrow> (\<exists>u. u \<^bold>\<in> x \<and> v = f u)"
   by (rule replacement [where R = "\<lambda>u v. v = f u"]) auto
 
 definition PrimReplace :: "hf \<Rightarrow> (hf \<Rightarrow> hf \<Rightarrow> bool) \<Rightarrow> hf"
   where "PrimReplace A R = (THE z. \<forall>v. v \<^bold>\<in> z \<longleftrightarrow> (\<exists>u. u \<^bold>\<in> A \<and> R u v))"
 
 definition Replace :: "hf \<Rightarrow> (hf \<Rightarrow> hf \<Rightarrow> bool) \<Rightarrow> hf"
   where "Replace A R = PrimReplace A (\<lambda>x y. (\<exists>!z. R x z) \<and> R x y)"
 
 definition RepFun :: "hf \<Rightarrow> (hf \<Rightarrow> hf) \<Rightarrow> hf"
   where "RepFun A f = Replace A (\<lambda>x y. y = f x)"
 
 
 syntax (ASCII)
   "_HReplace"  :: "[pttrn, pttrn, hf, bool] \<Rightarrow> hf" ("(1{|_ ./ _<: _, _|})")
   "_HRepFun"   :: "[hf, pttrn, hf] \<Rightarrow> hf"          ("(1{|_ ./ _<: _|})" [51,0,51])
   "_HINTER"    :: "[pttrn, hf, hf] \<Rightarrow> hf"          ("(3INT _<:_./ _)" 10)
   "_HUNION"    :: "[pttrn, hf, hf] \<Rightarrow> hf"          ("(3UN _<:_./ _)" 10)
 syntax
   "_HReplace"  :: "[pttrn, pttrn, hf, bool] \<Rightarrow> hf" ("(1\<lbrace>_ ./ _ \<^bold>\<in> _, _\<rbrace>)")
   "_HRepFun"   :: "[hf, pttrn, hf] \<Rightarrow> hf"          ("(1\<lbrace>_ ./ _ \<^bold>\<in> _\<rbrace>)" [51,0,51])
   "_HINTER"    :: "[pttrn, hf, hf] \<Rightarrow> hf"          ("(3\<Sqinter>_\<^bold>\<in>_./ _)" 10)
   "_HUNION"    :: "[pttrn, hf, hf] \<Rightarrow> hf"          ("(3\<Squnion>_\<^bold>\<in>_./ _)" 10)
 translations
   "\<lbrace>y. x\<^bold>\<in>A, Q\<rbrace>" \<rightleftharpoons> "CONST Replace A (\<lambda>x y. Q)"
   "\<lbrace>b. x\<^bold>\<in>A\<rbrace>"    \<rightleftharpoons> "CONST RepFun A (\<lambda>x. b)"
   "\<Sqinter>x\<^bold>\<in>A. B"    \<rightleftharpoons> "CONST HInter(CONST RepFun A (\<lambda>x. B))"
   "\<Squnion>x\<^bold>\<in>A. B"    \<rightleftharpoons> "CONST HUnion(CONST RepFun A (\<lambda>x. B))"
 
 lemma PrimReplace_iff:
   assumes sv: "\<forall>u v v'. u \<^bold>\<in> A \<longrightarrow> R u v \<longrightarrow> R u v' \<longrightarrow> v'=v"
   shows "v \<^bold>\<in> (PrimReplace A R) \<longleftrightarrow> (\<exists>u. u \<^bold>\<in> A \<and> R u v)"
 apply (insert replacement [OF sv], clarify)
 apply (simp add: PrimReplace_def)
 apply (rule theI2)
 apply (auto simp: hf_ext)
 done
 
 lemma Replace_iff [iff]:
   "v \<^bold>\<in> Replace A R \<longleftrightarrow> (\<exists>u. u \<^bold>\<in> A \<and> R u v \<and> (\<forall>y. R u y \<longrightarrow> y=v))"
 apply (simp add: Replace_def)
 apply (subst PrimReplace_iff, auto)
 done
 
 lemma Replace_0 [simp]: "Replace 0 R = 0"
   by blast
 
 lemma Replace_hunion [simp]: "Replace (A \<squnion> B) R = Replace A R  \<squnion>  Replace B R"
   by blast
 
 lemma Replace_cong [cong]:
     "\<lbrakk> A=B;  \<And>x y. x \<^bold>\<in> B \<Longrightarrow> P x y \<longleftrightarrow> Q x y \<rbrakk>  \<Longrightarrow> Replace A P = Replace B Q"
   by (simp add: hf_ext cong: conj_cong)
 
 lemma RepFun_iff [iff]: "v \<^bold>\<in> (RepFun A f) \<longleftrightarrow> (\<exists>u. u \<^bold>\<in> A \<and> v = f u)"
   by (auto simp: RepFun_def)
 
 lemma RepFun_cong [cong]:
     "\<lbrakk> A=B;  \<And>x. x \<^bold>\<in> B \<Longrightarrow> f(x)=g(x) \<rbrakk>  \<Longrightarrow> RepFun A f = RepFun B g"
 by (simp add: RepFun_def)
 
 lemma triv_RepFun [simp]: "RepFun A (\<lambda>x. x) = A"
 by blast
 
 lemma RepFun_0 [simp]: "RepFun 0 f = 0"
   by blast
 
 lemma RepFun_hinsert [simp]: "RepFun (hinsert a b) f = hinsert (f a) (RepFun b f)"
   by blast
 
 lemma RepFun_hunion [simp]:
   "RepFun (A \<squnion> B) f = RepFun A f  \<squnion>  RepFun B f"
   by blast
 
 lemma HF_HUnion: "\<lbrakk>finite A; \<And>x. x\<in>A \<Longrightarrow> finite (B x)\<rbrakk> \<Longrightarrow> HF (\<Union>x \<in> A. B x) = (\<Squnion>x\<^bold>\<in>HF A. HF (B x))"
   by (rule hf_equalityI) (auto)
 
 
 section \<open>Subset relation and the Lattice Properties\<close>
 
 text \<open>Definition 1.10 (Subset relation).\<close>
 instantiation hf :: order
 begin
   definition less_eq_hf where "A \<le> B \<longleftrightarrow> (\<forall>x. x \<^bold>\<in> A \<longrightarrow> x \<^bold>\<in> B)"
 
   definition less_hf    where "A < B \<longleftrightarrow> A \<le> B \<and> A \<noteq> (B::hf)"
 
   instance by standard (auto simp: less_eq_hf_def less_hf_def)
 end
 
 
 subsection \<open>Rules for subsets\<close>
 
 lemma hsubsetI [intro!]:
     "(\<And>x. x\<^bold>\<in>A \<Longrightarrow> x\<^bold>\<in>B) \<Longrightarrow> A \<le> B"
   by (simp add: less_eq_hf_def)
 
 text \<open>Classical elimination rule\<close>
 lemma hsubsetCE [elim]: "\<lbrakk> A \<le> B;  c\<^bold>\<notin>A \<Longrightarrow> P;  c\<^bold>\<in>B \<Longrightarrow> P \<rbrakk>  \<Longrightarrow> P"
   by (auto simp: less_eq_hf_def)
 
 text \<open>Rule in Modus Ponens style\<close>
 lemma hsubsetD [elim]: "\<lbrakk> A \<le> B;  c\<^bold>\<in>A \<rbrakk> \<Longrightarrow> c\<^bold>\<in>B"
   by (simp add: less_eq_hf_def)
 
 text \<open>Sometimes useful with premises in this order\<close>
 lemma rev_hsubsetD: "\<lbrakk> c\<^bold>\<in>A; A\<le>B \<rbrakk> \<Longrightarrow> c\<^bold>\<in>B"
   by blast
 
 lemma contra_hsubsetD: "\<lbrakk> A \<le> B; c \<notin> B \<rbrakk>  \<Longrightarrow> c \<notin> A"
   by blast
 
 lemma rev_contra_hsubsetD: "\<lbrakk> c \<notin> B;  A \<le> B \<rbrakk>  \<Longrightarrow> c \<notin> A"
   by blast
 
 lemma hf_equalityE:
   fixes A :: hf shows "A = B \<Longrightarrow> (A \<le> B \<Longrightarrow> B \<le> A \<Longrightarrow> P) \<Longrightarrow> P"
   by (metis order_refl)
 
 
 subsection \<open>Lattice properties\<close>
 
 instantiation hf :: distrib_lattice
 begin
   instance by standard (auto simp: less_eq_hf_def less_hf_def inf_hf_def)
 end
 
 instantiation hf :: bounded_lattice_bot
 begin
   definition "bot = (0::hf)"
   instance by standard (auto simp: less_eq_hf_def bot_hf_def)
 end
 
 lemma hinter_hempty_left [simp]: "0 \<sqinter> A = 0"
   by (metis bot_hf_def inf_bot_left)
 
 lemma hinter_hempty_right [simp]: "A \<sqinter> 0 = 0"
   by (metis bot_hf_def inf_bot_right)
 
 lemma hunion_hempty_left [simp]: "0 \<squnion> A = A"
   by (metis bot_hf_def sup_bot_left)
 
 lemma hunion_hempty_right [simp]: "A \<squnion> 0 = A"
   by (metis bot_hf_def sup_bot_right)
 
 lemma less_eq_hempty [simp]: "u \<le> 0 \<longleftrightarrow> u = (0::hf)"
   by (metis hempty_iff less_eq_hf_def)
 
 lemma less_eq_insert1_iff [iff]: "(hinsert x y) \<le> z \<longleftrightarrow> x \<^bold>\<in> z \<and> y \<le> z"
   by (auto simp: less_eq_hf_def)
 
 lemma less_eq_insert2_iff:
   "z \<le> (hinsert x y) \<longleftrightarrow> z \<le> y \<or> (\<exists>u. hinsert x u = z \<and> x \<^bold>\<notin> u \<and> u \<le> y)"
 proof (cases "x \<^bold>\<in> z")
   case True
   hence u: "hinsert x (z - \<lbrace>x\<rbrace>) = z" by auto
   show ?thesis
     proof
       assume "z \<le> (hinsert x y)"
       thus "z \<le> y \<or> (\<exists>u. hinsert x u = z \<and> x \<^bold>\<notin> u \<and> u \<le> y)"
         by (simp add: less_eq_hf_def) (metis u hdiff_iff hmem_hinsert)
     next
       assume "z \<le> y \<or> (\<exists>u. hinsert x u = z \<and> x \<^bold>\<notin> u \<and> u \<le> y)"
       thus "z \<le> (hinsert x y)"
         by (auto simp: less_eq_hf_def)
     qed
 next
   case False thus ?thesis
     by (metis hmem_hinsert less_eq_hf_def)
 qed
 
 lemma zero_le [simp]: "0 \<le> (x::hf)"
   by blast
 
 lemma hinsert_eq_sup: "b \<triangleleft> a = b \<squnion> \<lbrace>a\<rbrace>"
   by blast
 
 lemma hunion_hinsert_left: "hinsert x A \<squnion> B = hinsert x (A \<squnion> B)"
   by blast
 
 lemma hunion_hinsert_right: "B \<squnion> hinsert x A = hinsert x (B \<squnion> A)"
   by blast
 
 lemma hinter_hinsert_left: "hinsert x A \<sqinter> B = (if x \<^bold>\<in> B then hinsert x (A \<sqinter> B) else A \<sqinter> B)"
   by auto
 
 lemma hinter_hinsert_right: "B \<sqinter> hinsert x A = (if x \<^bold>\<in> B then hinsert x (B \<sqinter> A) else B \<sqinter> A)"
   by auto
 
 
 section \<open>Foundation, Cardinality, Powersets\<close>
 
 subsection \<open>Foundation\<close>
 
 text \<open>Theorem 1.13: Foundation (Regularity) Property.\<close>
 lemma foundation:
   assumes z: "z \<noteq> 0" shows "\<exists>w. w \<^bold>\<in> z \<and> w \<sqinter> z = 0"
 proof -
   { fix x
     assume z: "(\<forall>w. w \<^bold>\<in> z \<longrightarrow> w \<sqinter> z \<noteq> 0)"
     have "x \<^bold>\<notin> z \<and> x \<sqinter> z = 0"
     proof (induction x rule: hf_induct)
       case 0 thus ?case
         by (metis hinter_hempty_left z)
     next
       case (hinsert x y) thus ?case
         by (metis hinter_hinsert_left z)
     qed
   }
   thus ?thesis using z
     by (metis z hempty_iff)
 qed
 
 lemma hmem_not_refl: "x \<^bold>\<notin> x"
   using foundation [of "\<lbrace>x\<rbrace>"]
   by (metis hinter_iff hmem_hempty hmem_hinsert)
 
 lemma hmem_not_sym: "\<not> (x \<^bold>\<in> y \<and> y \<^bold>\<in> x)"
   using foundation [of "\<lbrace>x,y\<rbrace>"]
   by (metis hinter_iff hmem_hempty hmem_hinsert)
 
 lemma hmem_ne: "x \<^bold>\<in> y \<Longrightarrow> x \<noteq> y"
   by (metis hmem_not_refl)
 
 lemma hmem_Sup_ne: "x \<^bold>\<in> y \<Longrightarrow> \<Squnion>x \<noteq> y"
   by (metis HUnion_iff hmem_not_sym)
 
 lemma hpair_neq_fst: "\<langle>a,b\<rangle> \<noteq> a"
   by (metis hpair_def hinsert_iff hmem_not_sym)
 
 lemma hpair_neq_snd: "\<langle>a,b\<rangle> \<noteq> b"
   by (metis hpair_def hinsert_iff hmem_not_sym)
 
 lemma hpair_nonzero [simp]: "\<langle>x,y\<rangle> \<noteq> 0"
   by (auto simp: hpair_def)
 
 lemma zero_notin_hpair: "0 \<^bold>\<notin> \<langle>x,y\<rangle>"
   by (auto simp: hpair_def)
 
 
 subsection \<open>Cardinality\<close>
 
 text \<open>First we need to hack the underlying representation\<close>
 lemma hfset_0 [simp]: "hfset 0 = {}"
   by (metis Zero_hf_def finite.emptyI hfset_HF)
 
 lemma hfset_hinsert: "hfset (b \<triangleleft> a) = insert a (hfset b)"
   by (metis finite_insert hinsert_def HF.finite_hfset hfset_HF)
 
 lemma hfset_hdiff: "hfset (x - y) = hfset x - hfset y"
 proof (induct x arbitrary: y rule: hf_induct)
   case 0 thus ?case
     by simp
 next
   case (hinsert a b) thus ?case
     by (simp add: hfset_hinsert Set.insert_Diff_if hinsert_hdiff_if hmem_def)
 qed
 
 definition hcard :: "hf \<Rightarrow> nat"
   where "hcard x = card (hfset x)"
 
 lemma hcard_0 [simp]: "hcard 0 = 0"
   by (simp add: hcard_def)
 
 lemma hcard_hinsert_if: "hcard (hinsert x y) = (if x \<^bold>\<in> y then hcard y else Suc (hcard y))"
   by (simp add: hcard_def hfset_hinsert card_insert_if hmem_def)
 
 lemma hcard_union_inter: "hcard (x \<squnion> y) + hcard (x \<sqinter> y) = hcard x + hcard y"
   apply (induct x arbitrary: y rule: hf_induct)
   apply (auto simp: hcard_hinsert_if hunion_hinsert_left hinter_hinsert_left)
   done
 
 lemma hcard_hdiff1_less: "x \<^bold>\<in> z \<Longrightarrow> hcard (z - \<lbrace>x\<rbrace>) < hcard z"
   by (simp add: hcard_def hfset_hdiff hfset_hinsert)
      (metis card_Diff1_less finite_hfset hmem_def)
 
 
 subsection \<open>Powerset Operator\<close>
 
 text \<open>Theorem 1.11 (Existence of the power set).\<close>
 lemma powerset: "\<exists>z. \<forall>u. u \<^bold>\<in> z \<longleftrightarrow> u \<le> x"
 proof (induction x rule: hf_induct)
  case 0 thus ?case
     by (metis hmem_hempty hmem_hinsert less_eq_hempty)
 next
   case (hinsert a b)
   then obtain Pb where Pb: "\<forall>u. u \<^bold>\<in> Pb \<longleftrightarrow> u \<le> b"
     by auto
   obtain RPb where RPb: "\<forall>v. v \<^bold>\<in> RPb \<longleftrightarrow> (\<exists>u. u \<^bold>\<in> Pb \<and> v = hinsert a u)"
     using replacement_fun ..
   thus ?case using Pb binary_union [of Pb RPb]
     apply (simp add: less_eq_insert2_iff, clarify)
     apply (rule_tac x=z in exI)
     apply (metis hinsert.hyps less_eq_hf_def)
     done
 qed
 
 definition HPow :: "hf \<Rightarrow> hf"
   where "HPow x = (THE z. \<forall>u. u \<^bold>\<in> z \<longleftrightarrow> u \<le> x)"
 
 lemma HPow_iff [iff]: "u \<^bold>\<in> HPow x \<longleftrightarrow> u \<le> x"
 apply (insert powerset [of x], clarify)
 apply (simp add: HPow_def)
 apply (rule theI2)
 apply (auto simp: hf_ext)
 done
 
 lemma HPow_mono: "x \<le> y \<Longrightarrow> HPow x \<le> HPow y"
   by (metis HPow_iff less_eq_hf_def order_trans)
 
 lemma HPow_mono_strict: "x < y \<Longrightarrow> HPow x < HPow y"
   by (metis HPow_iff HPow_mono less_le_not_le order_eq_iff)
 
 lemma HPow_mono_iff [simp]: "HPow x \<le> HPow y \<longleftrightarrow> x \<le> y"
   by (metis HPow_iff HPow_mono hsubsetCE order_refl)
 
 lemma HPow_mono_strict_iff [simp]: "HPow x < HPow y \<longleftrightarrow> x < y"
   by (metis HPow_mono_iff less_le_not_le)
 
 
 section \<open>Bounded Quantifiers\<close>
 
 definition HBall :: "hf \<Rightarrow> (hf \<Rightarrow> bool) \<Rightarrow> bool" where
   "HBall A P \<longleftrightarrow> (\<forall>x. x \<^bold>\<in> A \<longrightarrow> P x)"   \<comment> \<open>bounded universal quantifiers\<close>
 
 definition HBex :: "hf \<Rightarrow> (hf \<Rightarrow> bool) \<Rightarrow> bool" where
   "HBex A P \<longleftrightarrow> (\<exists>x. x \<^bold>\<in> A \<and> P x)"   \<comment> \<open>bounded existential quantifiers\<close>
 
 syntax (ASCII)
   "_HBall"       :: "pttrn \<Rightarrow> hf \<Rightarrow> bool \<Rightarrow> bool"      ("(3ALL _<:_./ _)" [0, 0, 10] 10)
   "_HBex"        :: "pttrn \<Rightarrow> hf \<Rightarrow> bool \<Rightarrow> bool"      ("(3EX _<:_./ _)"  [0, 0, 10] 10)
   "_HBex1"       :: "pttrn \<Rightarrow> hf \<Rightarrow> bool \<Rightarrow> bool"      ("(3EX! _<:_./ _)" [0, 0, 10] 10)
 syntax
   "_HBall"       :: "pttrn \<Rightarrow> hf \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<forall>_\<^bold>\<in>_./ _)"  [0, 0, 10] 10)
   "_HBex"        :: "pttrn \<Rightarrow> hf \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<exists>_\<^bold>\<in>_./ _)"  [0, 0, 10] 10)
   "_HBex1"       :: "pttrn \<Rightarrow> hf \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<exists>!_\<^bold>\<in>_./ _)" [0, 0, 10] 10)
 translations
   "\<forall>x\<^bold>\<in>A. P" \<rightleftharpoons> "CONST HBall A (\<lambda>x. P)"
   "\<exists>x\<^bold>\<in>A. P" \<rightleftharpoons> "CONST HBex A (\<lambda>x. P)"
   "\<exists>!x\<^bold>\<in>A. P" \<rightharpoonup> "\<exists>!x. x\<in>A \<and> P"
 
 lemma hball_cong [cong]:
     "\<lbrakk> A=A';  \<And>x. x \<^bold>\<in> A' \<Longrightarrow> P(x) \<longleftrightarrow> P'(x) \<rbrakk>  \<Longrightarrow> (\<forall>x\<^bold>\<in>A. P(x)) \<longleftrightarrow> (\<forall>x\<^bold>\<in>A'. P'(x))"
   by (simp add: HBall_def)
 
 lemma hballI [intro!]: "(\<And>x. x\<^bold>\<in>A \<Longrightarrow> P x) \<Longrightarrow> \<forall>x\<^bold>\<in>A. P x"
   by (simp add: HBall_def)
 
 lemma hbspec [dest?]: "\<forall>x\<^bold>\<in>A. P x \<Longrightarrow> x\<^bold>\<in>A \<Longrightarrow> P x"
   by (simp add: HBall_def)
 
 lemma hballE [elim]: "\<forall>x\<^bold>\<in>A. P x \<Longrightarrow> (P x \<Longrightarrow> Q) \<Longrightarrow> (x \<^bold>\<notin> A \<Longrightarrow> Q) \<Longrightarrow> Q"
   by (unfold HBall_def) blast
 
 lemma hbex_cong [cong]:
     "\<lbrakk> A=A';  \<And>x. x \<^bold>\<in> A' \<Longrightarrow> P(x) \<longleftrightarrow> P'(x) \<rbrakk>  \<Longrightarrow> (\<exists>x\<^bold>\<in>A. P(x)) \<longleftrightarrow> (\<exists>x\<^bold>\<in>A'. P'(x))"
   by (simp add: HBex_def cong: conj_cong)
 
 lemma hbexI [intro]: "P x \<Longrightarrow> x\<^bold>\<in>A \<Longrightarrow> \<exists>x\<^bold>\<in>A. P x"
   by (unfold HBex_def) blast
 
 lemma rev_hbexI [intro?]: "x\<^bold>\<in>A \<Longrightarrow> P x \<Longrightarrow> \<exists>x\<^bold>\<in>A. P x"
   by (unfold HBex_def) blast
 
 lemma bexCI: "(\<forall>x\<^bold>\<in>A. \<not> P x \<Longrightarrow> P a) \<Longrightarrow> a\<^bold>\<in>A \<Longrightarrow> \<exists>x\<^bold>\<in>A. P x"
   by (unfold HBex_def) blast
 
 lemma hbexE [elim!]: "\<exists>x\<^bold>\<in>A. P x \<Longrightarrow> (\<And>x. x\<^bold>\<in>A \<Longrightarrow> P x \<Longrightarrow> Q) \<Longrightarrow> Q"
   by (unfold HBex_def) blast
 
 lemma hball_triv [simp]: "(\<forall>x\<^bold>\<in>A. P) = ((\<exists>x. x\<^bold>\<in>A) \<longrightarrow> P)"
-  \<comment> \<open>Trival rewrite rule.\<close>
+  \<comment> \<open>trivial rewrite rule.\<close>
   by (simp add: HBall_def)
 
 lemma hbex_triv [simp]: "(\<exists>x\<^bold>\<in>A. P) = ((\<exists>x. x\<^bold>\<in>A) \<and> P)"
   \<comment> \<open>Dual form for existentials.\<close>
   by (simp add: HBex_def)
 
 lemma hbex_triv_one_point1 [simp]: "(\<exists>x\<^bold>\<in>A. x = a) = (a\<^bold>\<in>A)"
   by blast
 
 lemma hbex_triv_one_point2 [simp]: "(\<exists>x\<^bold>\<in>A. a = x) = (a\<^bold>\<in>A)"
   by blast
 
 lemma hbex_one_point1 [simp]: "(\<exists>x\<^bold>\<in>A. x = a \<and> P x) = (a\<^bold>\<in>A \<and> P a)"
   by blast
 
 lemma hbex_one_point2 [simp]: "(\<exists>x\<^bold>\<in>A. a = x \<and> P x) = (a\<^bold>\<in>A \<and> P a)"
   by blast
 
 lemma hball_one_point1 [simp]: "(\<forall>x\<^bold>\<in>A. x = a \<longrightarrow> P x) = (a\<^bold>\<in>A \<longrightarrow> P a)"
   by blast
 
 lemma hball_one_point2 [simp]: "(\<forall>x\<^bold>\<in>A. a = x \<longrightarrow> P x) = (a\<^bold>\<in>A \<longrightarrow> P a)"
   by blast
 
 lemma hball_conj_distrib:
   "(\<forall>x\<^bold>\<in>A. P x \<and> Q x) \<longleftrightarrow> ((\<forall>x\<^bold>\<in>A. P x) \<and> (\<forall>x\<^bold>\<in>A. Q x))"
   by blast
 
 lemma hbex_disj_distrib:
   "(\<exists>x\<^bold>\<in>A. P x \<or> Q x) \<longleftrightarrow> ((\<exists>x\<^bold>\<in>A. P x) \<or> (\<exists>x\<^bold>\<in>A. Q x))"
   by blast
 
 lemma hb_all_simps [simp, no_atp]:
   "\<And>A P Q. (\<forall>x \<^bold>\<in> A. P x \<or> Q) \<longleftrightarrow> ((\<forall>x \<^bold>\<in> A. P x) \<or> Q)"
   "\<And>A P Q. (\<forall>x \<^bold>\<in> A. P \<or> Q x) \<longleftrightarrow> (P \<or> (\<forall>x \<^bold>\<in> A. Q x))"
   "\<And>A P Q. (\<forall>x \<^bold>\<in> A. P \<longrightarrow> Q x) \<longleftrightarrow> (P \<longrightarrow> (\<forall>x \<^bold>\<in> A. Q x))"
   "\<And>A P Q. (\<forall>x \<^bold>\<in> A. P x \<longrightarrow> Q) \<longleftrightarrow> ((\<exists>x \<^bold>\<in> A. P x) \<longrightarrow> Q)"
   "\<And>P. (\<forall>x \<^bold>\<in> 0. P x) \<longleftrightarrow> True"
   "\<And>a B P. (\<forall>x \<^bold>\<in> B \<triangleleft> a. P x) \<longleftrightarrow> (P a \<and> (\<forall>x \<^bold>\<in> B. P x))"
   "\<And>P Q. (\<forall>x \<^bold>\<in> HCollect Q A. P x) \<longleftrightarrow> (\<forall>x \<^bold>\<in> A. Q x \<longrightarrow> P x)"
   "\<And>A P. (\<not> (\<forall>x \<^bold>\<in> A. P x)) \<longleftrightarrow> (\<exists>x \<^bold>\<in> A. \<not> P x)"
   by auto
 
 lemma hb_ex_simps [simp, no_atp]:
   "\<And>A P Q. (\<exists>x \<^bold>\<in> A. P x \<and> Q) \<longleftrightarrow> ((\<exists>x \<^bold>\<in> A. P x) \<and> Q)"
   "\<And>A P Q. (\<exists>x \<^bold>\<in> A. P \<and> Q x) \<longleftrightarrow> (P \<and> (\<exists>x \<^bold>\<in> A. Q x))"
   "\<And>P. (\<exists>x \<^bold>\<in> 0. P x) \<longleftrightarrow> False"
   "\<And>a B P. (\<exists>x \<^bold>\<in> B \<triangleleft> a. P x) \<longleftrightarrow> (P a \<or> (\<exists>x \<^bold>\<in> B. P x))"
   "\<And>P Q. (\<exists>x \<^bold>\<in> HCollect Q A. P x) \<longleftrightarrow> (\<exists>x \<^bold>\<in> A. Q x \<and> P x)"
   "\<And>A P. (\<not>(\<exists>x \<^bold>\<in> A. P x)) \<longleftrightarrow> (\<forall>x \<^bold>\<in> A. \<not> P x)"
   by auto
 
 lemma le_HCollect_iff: "A \<le> \<lbrace>x \<^bold>\<in> B. P x\<rbrace> \<longleftrightarrow> A \<le> B \<and> (\<forall>x \<^bold>\<in> A. P x)"
   by blast
 
 
 section \<open>Relations and Functions\<close>
 
 definition is_hpair :: "hf \<Rightarrow> bool"
   where "is_hpair z = (\<exists>x y. z = \<langle>x,y\<rangle>)"
 
 definition hconverse :: "hf \<Rightarrow> hf"
   where "hconverse(r) = \<lbrace>z. w \<^bold>\<in> r, \<exists>x y. w = \<langle>x,y\<rangle> \<and> z = \<langle>y,x\<rangle>\<rbrace>"
 
 definition hdomain :: "hf \<Rightarrow> hf"
   where "hdomain(r) = \<lbrace>x. w \<^bold>\<in> r, \<exists>y. w = \<langle>x,y\<rangle>\<rbrace>"
 
 definition hrange :: "hf \<Rightarrow> hf"
   where "hrange(r) = hdomain(hconverse(r))"
 
 definition hrelation :: "hf \<Rightarrow> bool"
   where "hrelation(r) = (\<forall>z. z \<^bold>\<in> r \<longrightarrow> is_hpair z)"
 
 definition hrestrict :: "hf \<Rightarrow> hf \<Rightarrow> hf"
   \<comment> \<open>Restrict the relation r to the domain A\<close>
   where "hrestrict r A = \<lbrace>z \<^bold>\<in> r. \<exists>x \<^bold>\<in> A. \<exists>y. z = \<langle>x,y\<rangle>\<rbrace>"
 
 definition nonrestrict :: "hf \<Rightarrow> hf \<Rightarrow> hf"
   where "nonrestrict r A = \<lbrace>z \<^bold>\<in> r. \<forall>x \<^bold>\<in> A. \<forall>y. z \<noteq> \<langle>x,y\<rangle>\<rbrace>"
 
 definition hfunction :: "hf \<Rightarrow> bool"
   where "hfunction(r) = (\<forall>x y. \<langle>x,y\<rangle> \<^bold>\<in> r \<longrightarrow> (\<forall>y'. \<langle>x,y'\<rangle> \<^bold>\<in> r \<longrightarrow> y=y'))"
 
 definition app :: "hf \<Rightarrow> hf \<Rightarrow> hf"
   where "app f x = (THE y. \<langle>x, y\<rangle> \<^bold>\<in> f)"
 
 lemma hrestrict_iff [iff]:
     "z \<^bold>\<in> hrestrict r A \<longleftrightarrow> z \<^bold>\<in> r \<and> (\<exists> x y. z = \<langle>x, y\<rangle> \<and> x \<^bold>\<in> A)"
   by (auto simp: hrestrict_def)
 
 lemma hrelation_0 [simp]: "hrelation 0"
   by (force simp add: hrelation_def)
 
 lemma hrelation_restr [iff]: "hrelation (hrestrict r x)"
   by (metis hrelation_def hrestrict_iff is_hpair_def)
 
 lemma hrelation_hunion [simp]: "hrelation (f \<squnion> g) \<longleftrightarrow> hrelation f \<and> hrelation g"
   by (auto simp: hrelation_def)
 
 lemma hfunction_restr: "hfunction r \<Longrightarrow> hfunction (hrestrict r x)"
   by (auto simp: hfunction_def hrestrict_def)
 
 lemma hdomain_restr [simp]: "hdomain (hrestrict r x) = hdomain r \<sqinter> x"
   by (force simp add: hdomain_def hrestrict_def)
 
 lemma hdomain_0 [simp]: "hdomain 0 = 0"
   by (force simp add: hdomain_def)
 
 lemma hdomain_ins [simp]: "hdomain (r \<triangleleft> \<langle>x, y\<rangle>) = hdomain r \<triangleleft> x"
   by (force simp add: hdomain_def)
 
 lemma hdomain_hunion [simp]: "hdomain (f \<squnion> g) = hdomain f \<squnion> hdomain g"
   by (simp add: hdomain_def)
 
 lemma hdomain_not_mem [iff]: "\<langle>hdomain r, a\<rangle> \<^bold>\<notin> r"
   by (metis hdomain_ins hinter_hinsert_right hmem_hinsert hmem_not_refl
             hunion_hinsert_right sup_inf_absorb)
 
 lemma app_singleton [simp]: "app \<lbrace>\<langle>x, y\<rangle>\<rbrace> x = y"
   by (simp add: app_def)
 
 lemma app_equality: "hfunction f \<Longrightarrow> \<langle>x, y\<rangle> \<^bold>\<in> f \<Longrightarrow> app f x = y"
   by (auto simp: app_def hfunction_def intro: the1I2)
 
 lemma app_ins2: "x' \<noteq> x \<Longrightarrow> app (f \<triangleleft> \<langle>x, y\<rangle>) x' = app f x'"
   by (simp add: app_def)
 
 lemma hfunction_0 [simp]: "hfunction 0"
   by (force simp add: hfunction_def)
 
 lemma hfunction_ins: "hfunction f \<Longrightarrow> x \<^bold>\<notin> hdomain f \<Longrightarrow> hfunction (f\<triangleleft> \<langle>x, y\<rangle>)"
   by (auto simp: hfunction_def hdomain_def)
 
 lemma hdomainI: "\<langle>x, y\<rangle> \<^bold>\<in> f \<Longrightarrow> x \<^bold>\<in> hdomain f"
   by (auto simp: hdomain_def)
 
 lemma hfunction_hunion: "hdomain f \<sqinter> hdomain g = 0
             \<Longrightarrow> hfunction (f \<squnion> g) \<longleftrightarrow> hfunction f \<and> hfunction g"
   by (auto simp: hfunction_def) (metis hdomainI hinter_iff hmem_hempty)+
 
 lemma app_hrestrict [simp]: "x \<^bold>\<in> A \<Longrightarrow> app (hrestrict f A) x = app f x"
   by (simp add: hrestrict_def app_def)
 
 
 section \<open>Operations on families of sets\<close>
 
 definition HLambda :: "hf \<Rightarrow> (hf \<Rightarrow> hf) \<Rightarrow> hf"
   where "HLambda A b = RepFun A (\<lambda>x. \<langle>x, b x\<rangle>)"
 
 definition HSigma :: "hf \<Rightarrow> (hf \<Rightarrow> hf) \<Rightarrow> hf"
   where "HSigma A B = (\<Squnion>x\<^bold>\<in>A. \<Squnion>y\<^bold>\<in>B(x). \<lbrace>\<langle>x,y\<rangle>\<rbrace>)"
 
 definition HPi :: "hf \<Rightarrow> (hf \<Rightarrow> hf) \<Rightarrow> hf"
   where "HPi A B = \<lbrace> f \<^bold>\<in> HPow(HSigma A B). A \<le> hdomain(f) \<and> hfunction(f)\<rbrace>"
 
 
 syntax (ASCII)
   "_PROD"     :: "[pttrn, hf, hf] \<Rightarrow> hf"        ("(3PROD _<:_./ _)" 10)
   "_SUM"      :: "[pttrn, hf, hf] \<Rightarrow> hf"        ("(3SUM _<:_./ _)" 10)
   "_lam"      :: "[pttrn, hf, hf] \<Rightarrow> hf"        ("(3lam _<:_./ _)" 10)
 syntax
   "_PROD"     :: "[pttrn, hf, hf] \<Rightarrow> hf"        ("(3\<Prod>_\<^bold>\<in>_./ _)" 10)
   "_SUM"      :: "[pttrn, hf, hf] \<Rightarrow> hf"        ("(3\<Sum>_\<^bold>\<in>_./ _)" 10)
   "_lam"      :: "[pttrn, hf, hf] \<Rightarrow> hf"        ("(3\<lambda>_\<^bold>\<in>_./ _)" 10)
 translations
   "\<Prod>x\<^bold>\<in>A. B" \<rightleftharpoons> "CONST HPi A (\<lambda>x. B)"
   "\<Sum>x\<^bold>\<in>A. B" \<rightleftharpoons> "CONST HSigma A (\<lambda>x. B)"
   "\<lambda>x\<^bold>\<in>A. f"  \<rightleftharpoons> "CONST HLambda A (\<lambda>x. f)"
 
 
 subsection \<open>Rules for Unions and Intersections of families\<close>
 
 lemma HUN_iff [simp]: "b \<^bold>\<in> (\<Squnion>x\<^bold>\<in>A. B(x)) \<longleftrightarrow> (\<exists>x\<^bold>\<in>A. b \<^bold>\<in> B(x))"
   by auto
 
 (*The order of the premises presupposes that A is rigid; b may be flexible*)
 lemma HUN_I: "\<lbrakk> a \<^bold>\<in> A;  b \<^bold>\<in> B(a) \<rbrakk>  \<Longrightarrow> b \<^bold>\<in> (\<Squnion>x\<^bold>\<in>A. B(x))"
   by auto
 
 lemma HUN_E [elim!]: assumes "b \<^bold>\<in> (\<Squnion>x\<^bold>\<in>A. B(x))" obtains x where "x \<^bold>\<in> A"  "b \<^bold>\<in> B(x)"
   using assms  by blast
 
 lemma HINT_iff: "b \<^bold>\<in> (\<Sqinter>x\<^bold>\<in>A. B(x)) \<longleftrightarrow> (\<forall>x\<^bold>\<in>A. b \<^bold>\<in> B(x)) \<and> A\<noteq>0"
   by (simp add: HInter_def HBall_def) (metis foundation hmem_hempty)
 
 lemma HINT_I: "\<lbrakk> \<And>x. x \<^bold>\<in> A \<Longrightarrow> b \<^bold>\<in> B(x);  A\<noteq>0 \<rbrakk> \<Longrightarrow> b \<^bold>\<in> (\<Sqinter>x\<^bold>\<in>A. B(x))"
   by (simp add: HINT_iff)
 
 lemma HINT_E: "\<lbrakk> b \<^bold>\<in> (\<Sqinter>x\<^bold>\<in>A. B(x));  a \<^bold>\<in> A \<rbrakk> \<Longrightarrow> b \<^bold>\<in> B(a)"
   by (auto simp: HINT_iff)
 
 
 subsection \<open>Generalized Cartesian product\<close>
 
 lemma HSigma_iff [simp]: "\<langle>a,b\<rangle> \<^bold>\<in> HSigma A B \<longleftrightarrow> a \<^bold>\<in> A \<and> b \<^bold>\<in> B(a)"
   by (force simp add: HSigma_def)
 
 lemma HSigmaI [intro!]: "\<lbrakk> a \<^bold>\<in> A;  b \<^bold>\<in> B(a) \<rbrakk>  \<Longrightarrow> \<langle>a,b\<rangle> \<^bold>\<in> HSigma A B"
   by simp
 
 lemmas HSigmaD1 = HSigma_iff [THEN iffD1, THEN conjunct1]
 lemmas HSigmaD2 = HSigma_iff [THEN iffD1, THEN conjunct2]
 
 text \<open>The general elimination rule\<close>
 lemma HSigmaE [elim!]:
   assumes "c \<^bold>\<in> HSigma A B"
   obtains x y where "x \<^bold>\<in> A" "y \<^bold>\<in> B(x)" "c=\<langle>x,y\<rangle>"
   using assms  by (force simp add: HSigma_def)
 
 lemma HSigmaE2 [elim!]:
   assumes "\<langle>a,b\<rangle> \<^bold>\<in> HSigma A B" obtains "a \<^bold>\<in> A" and "b \<^bold>\<in> B(a)"
   using assms  by auto
 
 lemma HSigma_empty1 [simp]: "HSigma 0 B = 0"
   by blast
 
 instantiation hf :: times
 begin
   definition "A * B = HSigma A (\<lambda>x. B)"
   instance ..
 end
 
 lemma times_iff [simp]: "\<langle>a,b\<rangle> \<^bold>\<in> A * B \<longleftrightarrow> a \<^bold>\<in> A \<and> b \<^bold>\<in> B"
   by (simp add: times_hf_def)
 
 lemma timesI [intro!]: "\<lbrakk> a \<^bold>\<in> A;  b \<^bold>\<in> B \<rbrakk>  \<Longrightarrow> \<langle>a,b\<rangle> \<^bold>\<in> A * B"
   by simp
 
 lemmas timesD1 = times_iff [THEN iffD1, THEN conjunct1]
 lemmas timesD2 = times_iff [THEN iffD1, THEN conjunct2]
 
 text \<open>The general elimination rule\<close>
 lemma timesE [elim!]:
   assumes c: "c \<^bold>\<in> A * B"
   obtains x y where "x \<^bold>\<in> A" "y \<^bold>\<in> B" "c=\<langle>x,y\<rangle>" using c
   by (auto simp: times_hf_def)
 
 text \<open>...and a specific one\<close>
 lemma timesE2 [elim!]:
   assumes "\<langle>a,b\<rangle> \<^bold>\<in> A * B" obtains "a \<^bold>\<in> A" and "b \<^bold>\<in> B"
 using assms
   by auto
 
 lemma times_empty1 [simp]: "0 * B = (0::hf)"
   by auto
 
 lemma times_empty2 [simp]: "A*0 = (0::hf)"
   by blast
 
 lemma times_empty_iff: "A*B=0 \<longleftrightarrow> A=0 \<or> B=(0::hf)"
   by (auto simp: times_hf_def hf_ext)
 
 instantiation hf :: mult_zero
 begin
   instance by standard auto
 end
 
 
 section \<open>Disjoint Sum\<close>
 
 instantiation hf :: zero_neq_one
 begin
   definition One_hf_def: "1 = \<lbrace>0\<rbrace>"
   instance by standard (auto simp: One_hf_def)
 end
 
 instantiation hf :: plus
 begin
   definition "A + B = (\<lbrace>0\<rbrace> * A) \<squnion> (\<lbrace>1\<rbrace> * B)"
   instance ..
 end
 
 definition Inl :: "hf\<Rightarrow>hf" where
      "Inl(a) \<equiv> \<langle>0,a\<rangle>"
 
 definition Inr :: "hf\<Rightarrow>hf" where
      "Inr(b) \<equiv> \<langle>1,b\<rangle>"
 
 lemmas sum_defs = plus_hf_def Inl_def Inr_def
 
 lemma Inl_nonzero [simp]:"Inl x \<noteq> 0"
   by (metis Inl_def hpair_nonzero)
 
 lemma Inr_nonzero [simp]:"Inr x \<noteq> 0"
   by (metis Inr_def hpair_nonzero)
 
 text\<open>Introduction rules for the injections (as equivalences)\<close>
 
 lemma Inl_in_sum_iff [iff]: "Inl(a) \<^bold>\<in> A+B \<longleftrightarrow> a \<^bold>\<in> A"
   by (auto simp: sum_defs)
 
 lemma Inr_in_sum_iff [iff]: "Inr(b) \<^bold>\<in> A+B \<longleftrightarrow> b \<^bold>\<in> B"
   by (auto simp: sum_defs)
 
 text \<open>Elimination rule\<close>
 
 lemma sumE [elim!]:
   assumes u: "u \<^bold>\<in> A+B"
   obtains x where "x \<^bold>\<in> A" "u=Inl(x)" | y where "y \<^bold>\<in> B" "u=Inr(y)" using u
   by (auto simp: sum_defs)
 
 text \<open>Injection and freeness equivalences, for rewriting\<close>
 
 lemma Inl_iff [iff]: "Inl(a)=Inl(b) \<longleftrightarrow> a=b"
   by (simp add: sum_defs)
 
 lemma Inr_iff [iff]: "Inr(a)=Inr(b) \<longleftrightarrow> a=b"
   by (simp add: sum_defs)
 
 lemma Inl_Inr_iff [iff]: "Inl(a)=Inr(b) \<longleftrightarrow> False"
   by (simp add: sum_defs)
 
 lemma Inr_Inl_iff [iff]: "Inr(b)=Inl(a) \<longleftrightarrow> False"
   by (simp add: sum_defs)
 
 lemma sum_empty [simp]: "0+0 = (0::hf)"
   by (auto simp: sum_defs)
 
 lemma sum_iff: "u \<^bold>\<in> A+B \<longleftrightarrow> (\<exists>x. x \<^bold>\<in> A \<and> u=Inl(x)) \<or> (\<exists>y. y \<^bold>\<in> B \<and> u=Inr(y))"
   by blast
 
 lemma sum_subset_iff:
   fixes A :: hf shows "A+B \<le> C+D \<longleftrightarrow> A\<le>C \<and> B\<le>D"
   by blast
 
 lemma sum_equal_iff:
   fixes A :: hf shows "A+B = C+D \<longleftrightarrow> A=C \<and> B=D"
   by (auto simp: hf_ext sum_subset_iff)
 
 definition is_hsum :: "hf \<Rightarrow> bool"
   where "is_hsum z = (\<exists>x. z = Inl x \<or> z = Inr x)"
 
 definition sum_case  :: "(hf \<Rightarrow> 'a) \<Rightarrow> (hf \<Rightarrow> 'a) \<Rightarrow> hf \<Rightarrow> 'a"
   where
   "sum_case f g a \<equiv>
     THE z. (\<forall>x. a = Inl x \<longrightarrow> z = f x) \<and> (\<forall>y. a = Inr y \<longrightarrow> z = g y) \<and> (\<not> is_hsum a \<longrightarrow> z = undefined)"
 
 lemma sum_case_Inl [simp]: "sum_case f g (Inl x) = f x"
   by (simp add: sum_case_def is_hsum_def)
 
 lemma sum_case_Inr [simp]: "sum_case f g (Inr y) = g y"
   by (simp add: sum_case_def is_hsum_def)
 
 lemma sum_case_non [simp]: "\<not> is_hsum a \<Longrightarrow> sum_case f g a = undefined"
   by (simp add: sum_case_def is_hsum_def)
 
 lemma is_hsum_cases: "(\<exists>x. z = Inl x \<or> z = Inr x) \<or> \<not> is_hsum z"
   by (auto simp: is_hsum_def)
 
 lemma sum_case_split:
   "P (sum_case f g a) \<longleftrightarrow> (\<forall>x. a = Inl x \<longrightarrow> P(f x)) \<and> (\<forall>y. a = Inr y \<longrightarrow> P(g y)) \<and> (\<not> is_hsum a \<longrightarrow> P undefined)"
   by (cases "is_hsum a") (auto simp: is_hsum_def)
 
 lemma sum_case_split_asm:
   "P (sum_case f g a) \<longleftrightarrow> \<not> ((\<exists>x. a = Inl x \<and> \<not> P(f x)) \<or> (\<exists>y. a = Inr y \<and> \<not> P(g y)) \<or> (\<not> is_hsum a \<and> \<not> P undefined))"
   by (auto simp add: sum_case_split)
 
 end
diff --git a/thys/LLL_Basis_Reduction/Missing_Lemmas.thy b/thys/LLL_Basis_Reduction/Missing_Lemmas.thy
--- a/thys/LLL_Basis_Reduction/Missing_Lemmas.thy
+++ b/thys/LLL_Basis_Reduction/Missing_Lemmas.thy
@@ -1,835 +1,835 @@
 (*
     Authors:    Jose Divasón
                 Sebastiaan Joosten
                 René Thiemann
                 Akihisa Yamada
     License:    BSD
 *)
 
 section \<open>Missing lemmas\<close>
 
 text \<open>This theory contains many results that are important but not specific for our development. 
       They could be moved to the stardard library and some other AFP entries.\<close> 
 
 theory Missing_Lemmas
   imports
     Berlekamp_Zassenhaus.Sublist_Iteration (* for thm upt_append *)
     Berlekamp_Zassenhaus.Square_Free_Int_To_Square_Free_GFp (* for thm large_mod_0 *)
     Algebraic_Numbers.Resultant
     Jordan_Normal_Form.Conjugate
     Jordan_Normal_Form.Missing_VectorSpace
     Jordan_Normal_Form.VS_Connect
     Berlekamp_Zassenhaus.Finite_Field_Factorization_Record_Based (* for transfer rules for thm vec_of_list_Nil *)
     Berlekamp_Zassenhaus.Berlekamp_Hensel (* for unique_factorization_m_factor *)
 begin
 
 no_notation test_bit (infixl "!!" 100)
 
 hide_const(open) module.smult up_ring.monom up_ring.coeff
 
 (**** Could be merged to HOL/Rings.thy ****)
 
 lemma (in zero_less_one) zero_le_one [simp]: "0 \<le> 1" by (rule less_imp_le, simp)
 subclass (in zero_less_one) zero_neq_one by (unfold_locales, simp add: less_imp_neq)
 
 class ordered_semiring_1 = Rings.ordered_semiring_0 + monoid_mult + zero_less_one
 begin
 
 subclass semiring_1..
 
 lemma of_nat_ge_zero[intro!]: "of_nat n \<ge> 0"
   using add_right_mono[of _ _ 1] by (induct n, auto)
 
 (* Following lemmas are moved from @{class ordered_idom}. *)
 lemma zero_le_power [simp]: "0 \<le> a \<Longrightarrow> 0 \<le> a ^ n"
   by (induct n) simp_all
 
 lemma power_mono: "a \<le> b \<Longrightarrow> 0 \<le> a \<Longrightarrow> a ^ n \<le> b ^ n"
   by (induct n) (auto intro: mult_mono order_trans [of 0 a b])
 
 lemma one_le_power [simp]: "1 \<le> a \<Longrightarrow> 1 \<le> a ^ n"
   using power_mono [of 1 a n] by simp
 
 lemma power_le_one: "0 \<le> a \<Longrightarrow> a \<le> 1 \<Longrightarrow> a ^ n \<le> 1"
   using power_mono [of a 1 n] by simp
 
 lemma power_gt1_lemma:
   assumes gt1: "1 < a"
   shows "1 < a * a ^ n"
 proof -
   from gt1 have "0 \<le> a"
     by (fact order_trans [OF zero_le_one less_imp_le])
   from gt1 have "1 * 1 < a * 1" by simp
   also from gt1 have "\<dots> \<le> a * a ^ n"
     by (simp only: mult_mono \<open>0 \<le> a\<close> one_le_power order_less_imp_le zero_le_one order_refl)
   finally show ?thesis by simp
 qed
 
 lemma power_gt1: "1 < a \<Longrightarrow> 1 < a ^ Suc n"
   by (simp add: power_gt1_lemma)
 
 lemma one_less_power [simp]: "1 < a \<Longrightarrow> 0 < n \<Longrightarrow> 1 < a ^ n"
   by (cases n) (simp_all add: power_gt1_lemma)
 
 lemma power_decreasing: "n \<le> N \<Longrightarrow> 0 \<le> a \<Longrightarrow> a \<le> 1 \<Longrightarrow> a ^ N \<le> a ^ n"
 proof (induction N)
   case (Suc N)
   then have "a * a^N \<le> 1 * a^n" if "n \<le> N"
     using that by (intro mult_mono) auto
   then show ?case
     using Suc by (auto simp add: le_Suc_eq)
 qed (auto)
 
 lemma power_increasing: "n \<le> N \<Longrightarrow> 1 \<le> a \<Longrightarrow> a ^ n \<le> a ^ N"
 proof (induction N)
   case (Suc N)
   then have "1 * a^n \<le> a * a^N" if "n \<le> N"
     using that by (intro mult_mono) (auto simp add: order_trans[OF zero_le_one])
   then show ?case
     using Suc by (auto simp add: le_Suc_eq)
 qed (auto)
 
 lemma power_Suc_le_self: "0 \<le> a \<Longrightarrow> a \<le> 1 \<Longrightarrow> a ^ Suc n \<le> a"
   using power_decreasing [of 1 "Suc n" a] by simp
 
 end
 
 lemma prod_list_nonneg: "(\<And> x. (x :: 'a :: ordered_semiring_1) \<in> set xs \<Longrightarrow> x \<ge> 0) \<Longrightarrow> prod_list xs \<ge> 0"
   by (induct xs, auto)
 
 subclass (in ordered_idom) ordered_semiring_1 by unfold_locales auto
 
 (**** End of lemmas that could be moved to HOL/Rings.thy ****)
 
 (* missing lemma on logarithms *)
 lemma log_prod: assumes "0 < a" "a \<noteq> 1" "\<And> x. x \<in> X \<Longrightarrow> 0 < f x" 
   shows "log a (prod f X) = sum (log a o f) X" 
   using assms(3)
 proof (induct X rule: infinite_finite_induct)
   case (insert x F)
   have "log a (prod f (insert x F)) = log a (f x * prod f F)" using insert by simp
   also have "\<dots> = log a (f x) + log a (prod f F)" 
     by (rule log_mult[OF assms(1-2) insert(4) prod_pos], insert insert, auto)
   finally show ?case using insert by auto
 qed auto
 
 (* TODO: Jordan_Normal_Form/Missing_Ring.ordered_idom should be redefined *)
 subclass (in ordered_idom) zero_less_one by (unfold_locales, auto)
 hide_fact Missing_Ring.zero_less_one
 
 (**** The following lemmas could be part of the standard library ****)
 
 instance real :: ordered_semiring_strict by (intro_classes, auto)
 instance real :: linordered_idom..
 
 (*This is a generalisation of thm less_1_mult*) 
 lemma less_1_mult': 
   fixes a::"'a::linordered_semidom"
   shows "1 < a \<Longrightarrow> 1 \<le> b \<Longrightarrow> 1 < a * b"
   by (metis le_less less_1_mult mult.right_neutral)
 
 lemma upt_minus_eq_append: "i\<le>j \<Longrightarrow> i\<le>j-k \<Longrightarrow> [i..<j] = [i..<j-k] @ [j-k..<j]"
 proof (induct k)
   case (Suc k)
   have hyp: "[i..<j] = [i..<j - k] @ [j - k..<j]" using Suc.hyps Suc.prems by auto
   then show ?case
     by (metis Suc.prems(2) append.simps(1) diff_Suc_less nat_less_le neq0_conv upt_append upt_rec zero_diff)
 qed auto
 
 lemma list_trisect: "x < length lst \<Longrightarrow> [0..<length lst] = [0..<x]@x#[Suc x..<length lst]"
   by (induct lst, force, rename_tac a lst, case_tac "x = length lst", auto)
 
 lemma id_imp_bij_betw:
   assumes f: "f : A \<rightarrow> A"
       and ff: "\<And>a. a \<in> A \<Longrightarrow> f (f a) = a"
   shows "bij_betw f A A"
   by (intro bij_betwI[OF f f], simp_all add: ff)
 
 lemma range_subsetI:
   assumes "\<And>x. f x = g (h x)" shows "range f \<subseteq> range g"
   using assms by auto
 
 lemma Gcd_uminus: 
   fixes A::"int set"
   assumes "finite A"
   shows "Gcd A = Gcd (uminus ` A)"
   using assms
   by (induct A, auto)
 
 lemma aux_abs_int: fixes c :: int
   assumes "c \<noteq> 0" 
   shows "\<bar>x\<bar> \<le> \<bar>x * c\<bar>"
 proof -
   have "abs x = abs x * 1" by simp
   also have "\<dots> \<le> abs x * abs c" 
     by (rule mult_left_mono, insert assms, auto)
   finally show ?thesis unfolding abs_mult by auto
 qed
 
 lemma mod_0_abs_less_imp_0:
   fixes a::int
   assumes a1: "[a = 0] (mod m)"
   and a2: "abs(a)<m"
   shows "a = 0"
 proof -
   have "m\<ge>0" using assms by auto
   thus ?thesis  
     using assms unfolding cong_def
     using int_mod_pos_eq large_mod_0 zless_imp_add1_zle 
-      by (metis abs_of_nonneg le_less not_less zabs_less_one_iff zmod_trival_iff)
+      by (metis abs_of_nonneg le_less not_less zabs_less_one_iff zmod_trivial_iff)
 qed
 
 (* an intro version of sum_list_0 *)
 lemma sum_list_zero:
   assumes "set xs \<subseteq> {0}" shows "sum_list xs = 0"
   using assms by (induct xs, auto)
 
 (* About @{const max} *)
 lemma max_idem [simp]: shows "max a a = a" by (simp add: max_def)
 
 lemma hom_max:
   assumes "a \<le> b \<longleftrightarrow> f a \<le> f b"
   shows "f (max a b) = max (f a) (f b)" using assms by (auto simp: max_def)
 
 lemma le_max_self:
   fixes a b :: "'a :: preorder"
   assumes "a \<le> b \<or> b \<le> a" shows "a \<le> max a b" and "b \<le> max a b"
   using assms by (auto simp: max_def)
 
 lemma le_max:
   fixes a b :: "'a :: preorder"
   assumes "c \<le> a \<or> c \<le> b" and "a \<le> b \<or> b \<le> a" shows "c \<le> max a b"
   using assms(1) le_max_self[OF assms(2)] by (auto dest: order_trans)
 
 fun max_list where
   "max_list [] = (THE x. False)" (* more convenient than "undefined" *)
 | "max_list [x] = x"
 | "max_list (x # y # xs) = max x (max_list (y # xs))"
 
 declare max_list.simps(1) [simp del]
 declare max_list.simps(2-3)[code]
 
 lemma max_list_Cons: "max_list (x#xs) = (if xs = [] then x else max x (max_list xs))"
   by (cases xs, auto)
 
 lemma max_list_mem: "xs \<noteq> [] \<Longrightarrow> max_list xs \<in> set xs"
   by (induct xs, auto simp: max_list_Cons max_def)
 
 lemma mem_set_imp_le_max_list:
   fixes xs :: "'a :: preorder list"
   assumes "\<And>a b. a \<in> set xs \<Longrightarrow> b \<in> set xs \<Longrightarrow> a \<le> b \<or> b \<le> a"
       and "a \<in> set xs"
   shows "a \<le> max_list xs"
 proof (insert assms, induct xs arbitrary:a)
   case Nil
   with assms show ?case by auto
 next
   case (Cons x xs)
   show ?case
   proof (cases "xs = []")
     case False
     have "x \<le> max_list xs \<or> max_list xs \<le> x"
       apply (rule Cons(2)) using max_list_mem[of xs] False by auto
     note 1 = le_max_self[OF this]
     from Cons have "a = x \<or> a \<in> set xs" by auto
     then show ?thesis
     proof (elim disjE)
       assume a: "a = x"
       show ?thesis by (unfold a max_list_Cons, auto simp: False intro!: 1)
     next
       assume "a \<in> set xs"
       then have "a \<le> max_list xs" by (intro Cons, auto)
       with 1 have "a \<le> max x (max_list xs)" by (auto dest: order_trans)
       then show ?thesis by (unfold max_list_Cons, auto simp: False)
     qed
   qed (insert Cons, auto)
 qed
 
 lemma le_max_list:
   fixes xs :: "'a :: preorder list"
   assumes ord: "\<And>a b. a \<in> set xs \<Longrightarrow> b \<in> set xs \<Longrightarrow> a \<le> b \<or> b \<le> a"
       and ab: "a \<le> b"
       and b: "b \<in> set xs"
   shows "a \<le> max_list xs"
 proof-
   note ab
   also have "b \<le> max_list xs"
     by (rule mem_set_imp_le_max_list, fact ord, fact b)
   finally show ?thesis.
 qed
 
 lemma max_list_le:
   fixes xs :: "'a :: preorder list"
   assumes a: "\<And>x. x \<in> set xs \<Longrightarrow> x \<le> a"
       and xs: "xs \<noteq> []"
   shows "max_list xs \<le> a"
   using max_list_mem[OF xs] a by auto
 
 lemma max_list_as_Greatest:
   assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> x \<le> y \<or> y \<le> x"
   shows "max_list xs = (GREATEST a. a \<in> set xs)"
 proof (cases "xs = []")
   case True
   then show ?thesis by (unfold Greatest_def, auto simp: max_list.simps(1))
 next
   case False
   from assms have 1: "x \<in> set xs \<Longrightarrow> x \<le> max_list xs" for x
     by (auto intro: le_max_list)
   have 2: "max_list xs \<in> set xs" by (fact max_list_mem[OF False])
   have "\<exists>!x. x \<in> set xs \<and> (\<forall>y. y \<in> set xs \<longrightarrow> y \<le> x)" (is "\<exists>!x. ?P x")
   proof (intro ex1I)
     from 1 2
     show "?P (max_list xs)" by auto
   next
     fix x assume 3: "?P x"
     with 1 have "x \<le> max_list xs" by auto
     moreover from 2 3 have "max_list xs \<le> x" by auto
     ultimately show "x = max_list xs" by auto
   qed
   note 3 = theI_unique[OF this,symmetric]
   from 1 2 show ?thesis
     by (unfold Greatest_def Cons 3, auto)
 qed
 
 lemma hom_max_list_commute:
   assumes "xs \<noteq> []"
       and "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> h (max x y) = max (h x) (h y)"
   shows "h (max_list xs) = max_list (map h xs)"
   by (insert assms, induct xs, auto simp: max_list_Cons max_list_mem)
 
 
 (*Efficient rev [i..<j]*)
 primrec rev_upt :: "nat \<Rightarrow> nat \<Rightarrow> nat list" ("(1[_>.._])") where
 rev_upt_0: "[0>..j] = []" |
 rev_upt_Suc: "[(Suc i)>..j] = (if i \<ge> j then i # [i>..j] else [])"
 
 lemma rev_upt_rec: "[i>..j] = (if i>j then [i>..Suc j] @ [j] else [])"
   by (induct i, auto)    
 
 definition rev_upt_aux :: "nat \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat list" where
   "rev_upt_aux i j js = [i>..j] @ js"
 
 lemma upt_aux_rec [code]:
   "rev_upt_aux i j js = (if j\<ge>i then js else rev_upt_aux i (Suc j) (j#js))"
   by (induct j, auto simp add: rev_upt_aux_def rev_upt_rec)
 
 lemma rev_upt_code[code]: "[i>..j] = rev_upt_aux i j []"
   by(simp add: rev_upt_aux_def)    
   
 lemma upt_rev_upt:
   "rev [j>..i] = [i..<j]"
   by (induct j, auto)
     
 lemma rev_upt_upt:
   "rev [i..<j] = [j>..i]"
   by (induct j, auto) 
 
 lemma length_rev_upt [simp]: "length [i>..j] = i - j"
   by (induct i) (auto simp add: Suc_diff_le)
     
 lemma nth_rev_upt [simp]: "j + k < i \<Longrightarrow> [i>..j] ! k = i - 1 - k"
 proof -
   assume jk_i: "j + k < i"
   have "[i>..j] = rev [j..<i]" using rev_upt_upt by simp
   also have "... ! k = [j..<i] ! (length [j..<i] - 1 - k)"
     using jk_i by (simp add: rev_nth)
   also have "... = [j..<i] ! (i - j - 1 - k)" by auto
   also have "... = j + (i - j - 1 - k)" by (rule nth_upt, insert jk_i, auto)
   finally show ?thesis using jk_i by auto
 qed    
   
 lemma nth_map_rev_upt: 
   assumes i: "i < m-n"
   shows "(map f [m>..n]) ! i = f (m - 1 - i)"
 proof -
   have "(map f [m>..n]) ! i = f ([m>..n] ! i)" by (rule nth_map, auto simp add: i)
   also have "... = f (m - 1 - i)"
   proof (rule arg_cong[of _ _ f], rule nth_rev_upt)
     show "n + i < m" using i by linarith
   qed
   finally show ?thesis .
 qed
 
 lemma coeff_mult_monom:
  "coeff (p * monom a d) i = (if d \<le> i then a * coeff p (i - d) else 0)"
   using coeff_monom_mult[of a d p] by (simp add: ac_simps)
 
 (**** End of the lemmas which may be part of the standard library ****)
 
 (**** The following lemmas could be moved to Algebraic_Numbers/Resultant.thy ****)
 lemma vec_of_poly_0 [simp]: "vec_of_poly 0 = 0\<^sub>v 1" by (auto simp: vec_of_poly_def)
 
 lemma vec_index_vec_of_poly [simp]: "i \<le> degree p \<Longrightarrow> vec_of_poly p $ i = coeff p (degree p - i)"
   by (simp add: vec_of_poly_def Let_def)
 
 lemma poly_of_vec_vec: "poly_of_vec (vec n f) = Poly (rev (map f [0..<n]))"
 proof (induct n arbitrary:f)
   case 0
   then show ?case by auto
 next
   case (Suc n)
   have "map f [0..<Suc n] = f 0 # map (f \<circ> Suc) [0..<n]" by (simp add: map_upt_Suc del: upt_Suc)
   also have "Poly (rev \<dots>) = Poly (rev (map (f \<circ> Suc) [0..<n])) + monom (f 0) n"
     by (simp add: Poly_snoc smult_monom)
   also have "\<dots> = poly_of_vec (vec n (f \<circ> Suc)) + monom (f 0) n"
     by (fold Suc, simp)
   also have "\<dots> = poly_of_vec (vec (Suc n) f)"
     apply (unfold poly_of_vec_def Let_def dim_vec sum.lessThan_Suc)
     by (auto simp add: Suc_diff_Suc)
   finally show ?case..
 qed
 
 lemma sum_list_map_dropWhile0:
   assumes f0: "f 0 = 0"
   shows "sum_list (map f (dropWhile ((=) 0) xs)) = sum_list (map f xs)"
   by (induct xs, auto simp add: f0)
 
 lemma coeffs_poly_of_vec:
   "coeffs (poly_of_vec v) = rev (dropWhile ((=) 0) (list_of_vec v))"
 proof-
   obtain n f where v: "v = vec n f" by transfer auto
   show ?thesis by (simp add: v poly_of_vec_vec)
 qed
 
 lemma poly_of_vec_vCons:
  "poly_of_vec (vCons a v) = monom a (dim_vec v) + poly_of_vec v" (is "?l = ?r")
   by (auto intro: poly_eqI simp: coeff_poly_of_vec vec_index_vCons)
 
 lemma poly_of_vec_as_Poly: "poly_of_vec v = Poly (rev (list_of_vec v))"
   by (induct v, auto simp:poly_of_vec_vCons Poly_snoc ac_simps)
 
 lemma poly_of_vec_add:
   assumes "dim_vec a = dim_vec b"
   shows "poly_of_vec (a + b) = poly_of_vec a + poly_of_vec b"
   using assms
   by (auto simp add: poly_eq_iff coeff_poly_of_vec)
 
 (*TODO: replace the one in Resultant.thy*)
 lemma degree_poly_of_vec_less:
   assumes "0 < dim_vec v" and "dim_vec v \<le> n" shows "degree (poly_of_vec v) < n"
   using degree_poly_of_vec_less assms by (auto dest: less_le_trans)
 
 lemma (in vec_module) poly_of_vec_finsum:
   assumes "f \<in> X \<rightarrow> carrier_vec n"
   shows "poly_of_vec (finsum V f X) = (\<Sum>i\<in>X. poly_of_vec (f i))"
 proof (cases "finite X")
   case False then show ?thesis by auto
 next
   case True show ?thesis
   proof (insert True assms, induct X rule: finite_induct)
     case IH: (insert a X)
     have [simp]: "f x \<in> carrier_vec n" if x: "x \<in> X" for x 
       using x IH.prems unfolding Pi_def by auto
     have [simp]: "f a \<in> carrier_vec n" using IH.prems unfolding Pi_def by auto
     have [simp]: "dim_vec (finsum V f X) = n" by simp
     have [simp]: "dim_vec (f a) = n" by simp
     show ?case
     proof (cases "a \<in> X")
       case True then show ?thesis by (auto simp: insert_absorb IH)
     next
       case False
       then have "(finsum V f (insert a X)) = f a + (finsum V f X)" 
         by (auto intro: finsum_insert IH)
       also have "poly_of_vec ... = poly_of_vec (f a) + poly_of_vec (finsum V f X)"
         by (rule poly_of_vec_add, simp)
       also have "... = (\<Sum>i\<in>insert a X. poly_of_vec (f i))"
         using IH False by (subst sum.insert, auto)
       finally show ?thesis .
     qed
   qed auto
 qed
 
 (*This function transforms a polynomial to a vector of dimension n*)  
 definition "vec_of_poly_n p n =
   vec n (\<lambda>i. if i < n - degree p - 1 then 0 else coeff p (n - i - 1))"
 
 (* TODO: make it abbreviation? *)
 lemma vec_of_poly_as: "vec_of_poly_n p (Suc (degree p)) = vec_of_poly p"
   by (induct p, auto simp: vec_of_poly_def vec_of_poly_n_def)
 
 lemma vec_of_poly_n_0 [simp]: "vec_of_poly_n p 0 = vNil"
   by (auto simp: vec_of_poly_n_def)
 
 lemma vec_dim_vec_of_poly_n [simp]:
   "dim_vec (vec_of_poly_n p n) = n"
   "vec_of_poly_n p n \<in> carrier_vec n"
   unfolding vec_of_poly_n_def by auto
 
 lemma dim_vec_of_poly [simp]: "dim_vec (vec_of_poly f) = degree f + 1"
   by (simp add: vec_of_poly_as[symmetric])
 
 lemma vec_index_of_poly_n:
   assumes "i < n"
   shows "vec_of_poly_n p n $ i =
     (if i < n - Suc (degree p) then 0 else coeff p (n - i - 1))"
   using assms by (auto simp: vec_of_poly_n_def Let_def)
 
 lemma vec_of_poly_n_pCons[simp]:
   shows "vec_of_poly_n (pCons a p) (Suc n) = vec_of_poly_n p n @\<^sub>v vec_of_list [a]" (is "?l = ?r")
 proof (unfold vec_eq_iff, intro conjI allI impI)
   show "dim_vec ?l = dim_vec ?r" by auto
   show "i < dim_vec ?r \<Longrightarrow> ?l $ i = ?r $ i" for i
     by (cases "n - i", auto simp: coeff_pCons less_Suc_eq_le vec_index_of_poly_n)
 qed
 
 lemma vec_of_poly_pCons:
   shows "vec_of_poly (pCons a p) =
    (if p = 0 then vec_of_list [a] else vec_of_poly p @\<^sub>v vec_of_list [a])"
   by (cases "degree p", auto simp: vec_of_poly_as[symmetric])
 
 lemma list_of_vec_of_poly [simp]:
   "list_of_vec (vec_of_poly p) = (if p = 0 then [0] else rev (coeffs p))"
   by (induct p, auto simp: vec_of_poly_pCons)
 
 lemma poly_of_vec_of_poly_n:
   assumes p: "degree p<n"
   shows "poly_of_vec (vec_of_poly_n p n) = p"
 proof - 
   have "vec_of_poly_n p n $ (n - Suc i) = coeff p i" if i: "i < n" for i    
   proof -
     have n: "n - Suc i < n" using i by auto
     have "vec_of_poly_n p n $ (n - Suc i) = 
       (if n - Suc i < n - Suc (degree p) then 0 else coeff p (n - (n - Suc i) - 1))"
       using vec_index_of_poly_n[OF n, of p] .
     also have "... = coeff p i" using i n le_degree by fastforce
     finally show ?thesis .
   qed
   moreover have "coeff p i = 0" if i2: "i \<ge> n" for i
     by (rule coeff_eq_0, insert i2 p, simp)
   ultimately show ?thesis
   using assms
   unfolding poly_eq_iff
   unfolding coeff_poly_of_vec by auto
 qed
 
 lemma vec_of_poly_n0[simp]: "vec_of_poly_n 0 n = 0\<^sub>v n" 
   unfolding vec_of_poly_n_def by auto
 
 lemma vec_of_poly_n_add: "vec_of_poly_n (a + b) n = vec_of_poly_n a n + vec_of_poly_n b n"
 proof (induct n arbitrary: a b)
   case 0
   then show ?case by auto
 next
   case (Suc n)
   then show ?case by (cases a, cases b, auto)
 qed
 
 lemma vec_of_poly_n_poly_of_vec:
   assumes n: "dim_vec g = n"
   shows "vec_of_poly_n (poly_of_vec g) n = g"
 proof (auto simp add: poly_of_vec_def vec_of_poly_n_def assms vec_eq_iff Let_def)
   have d: "degree (\<Sum>i<n. monom (g $ (n - Suc i)) i) = degree (poly_of_vec g)" 
     unfolding poly_of_vec_def Let_def n by auto
   fix i assume i1: "i < n - Suc (degree (\<Sum>i<n. monom (g $ (n - Suc i)) i))" 
     and i2: "i < n"
   have i3: "i < n - Suc (degree (poly_of_vec g))" 
     using i1 unfolding d by auto
   hence "dim_vec g - Suc i > degree (poly_of_vec g)"
     using n by linarith
   then show "g $ i = 0" using i1 i2 i3    
     by (metis (no_types, lifting) Suc_diff_Suc coeff_poly_of_vec diff_Suc_less 
         diff_diff_cancel leD le_degree less_imp_le_nat n neq0_conv)
 next
   fix i assume "i < n"
   thus "coeff (\<Sum>i<n. monom (g $ (n - Suc i)) i) (n - Suc i) = g $ i"    
     by (metis (no_types) Suc_diff_Suc coeff_poly_of_vec diff_diff_cancel 
         diff_less_Suc less_imp_le_nat n not_less_eq poly_of_vec_def)
 qed
 
 lemma poly_of_vec_scalar_mult:
   assumes "degree b<n"
   shows "poly_of_vec (a \<cdot>\<^sub>v (vec_of_poly_n b n)) = smult a b"
   using assms
   by (auto simp add: poly_eq_iff coeff_poly_of_vec vec_of_poly_n_def coeff_eq_0)
 
 (*TODO: replace the one in Resultant.thy*)
 definition vec_of_poly_rev_shifted where
   "vec_of_poly_rev_shifted p n s j \<equiv>
    vec n (\<lambda>i. if i \<le> j \<and> j \<le> s + i then coeff p (s + i - j) else 0)"
 
 lemma vec_of_poly_rev_shifted_dim[simp]: "dim_vec (vec_of_poly_rev_shifted p n s j) = n"
   unfolding vec_of_poly_rev_shifted_def by auto
 
 lemma col_sylvester_sub: (* TODO: from this directly derive col_sylvester *)
   assumes j: "j < m + n"
   shows "col (sylvester_mat_sub m n p q) j =
     vec_of_poly_rev_shifted p n m j @\<^sub>v vec_of_poly_rev_shifted q m n j" (is "?l = ?r")
 proof
   show "dim_vec ?l = dim_vec ?r" by simp
   fix i assume "i < dim_vec ?r" then have i: "i < m+n" by auto
   show "?l $ i = ?r $ i"
     unfolding vec_of_poly_rev_shifted_def
     apply (subst index_col) using i apply simp using j apply simp
     apply (subst sylvester_mat_sub_index) using i apply simp using j apply simp
     apply (cases "i < n") using i apply force using i
     apply (auto simp: not_less not_le intro!: coeff_eq_0)
     done
 qed
 
 lemma vec_of_poly_rev_shifted_scalar_prod:
   fixes p v
   defines "q \<equiv> poly_of_vec v"
   assumes m: "degree p \<le> m" and n: "dim_vec v = n"
   assumes j: "j < m+n"
   shows "vec_of_poly_rev_shifted p n m (n+m-Suc j) \<bullet> v = coeff (p * q) j" (is "?l = ?r")
 proof -
   have id1: "\<And> i. m + i - (n + m - Suc j) = i + Suc j - n"
     using j by auto
   let ?g = "\<lambda> i. if i \<le> n + m - Suc j \<and> n - Suc j \<le> i then coeff p (i + Suc j - n) *  v $ i else 0"
   have "?thesis = ((\<Sum>i = 0..<n. ?g i) =          
         (\<Sum>i\<le>j. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else 0)))" (is "_ = (?l = ?r)")
     unfolding vec_of_poly_rev_shifted_def coeff_mult m scalar_prod_def n q_def
       coeff_poly_of_vec 
     by (subst sum.cong, insert id1, auto)
   also have "..." 
   proof -
     have "?r = (\<Sum>i\<le>j. (if j - i < n then coeff p i * v $ (n - Suc (j - i)) else 0))" (is "_ = sum ?f _")
       by (rule sum.cong, auto)
     also have "sum ?f {..j} = sum ?f ({i. i \<le> j \<and> j - i < n} \<union> {i. i \<le> j \<and> \<not> j - i < n})" 
       (is "_ = sum _ (?R1 \<union> ?R2)")
       by (rule sum.cong, auto)
     also have "\<dots> = sum ?f ?R1 + sum ?f ?R2"
       by (subst sum.union_disjoint, auto)
     also have "sum ?f ?R2 = 0"
       by (rule sum.neutral, auto)
     also have "sum ?f ?R1 + 0 = sum (\<lambda> i. coeff p i * v $ (i + n - Suc j)) ?R1"
       (is "_ = sum ?F _")
       by (subst sum.cong, auto simp: ac_simps)
     also have "\<dots> = sum ?F ((?R1 \<inter> {..m}) \<union> (?R1 - {..m}))"
       (is "_ = sum _ (?R \<union> ?R')")
       by (rule sum.cong, auto)
     also have "\<dots> = sum ?F ?R + sum ?F ?R'"
       by (subst sum.union_disjoint, auto)
     also have "sum ?F ?R' = 0"
     proof -
       { 
         fix x
         assume "x > m" 
         with m
         have "?F x = 0" by (subst coeff_eq_0, auto)
       }
       thus ?thesis
         by (subst sum.neutral, auto)
     qed
     finally have r: "?r = sum ?F ?R" by simp
 
     have "?l = sum ?g ({i. i < n \<and> i \<le> n + m - Suc j \<and> n - Suc j \<le> i} 
       \<union> {i. i < n \<and> \<not> (i \<le> n + m - Suc j \<and> n - Suc j \<le> i)})" 
       (is "_ = sum _ (?L1 \<union> ?L2)")
       by (rule sum.cong, auto)
     also have "\<dots> = sum ?g ?L1 + sum ?g ?L2"
       by (subst sum.union_disjoint, auto)
     also have "sum ?g ?L2 = 0"
       by (rule sum.neutral, auto)
     also have "sum ?g ?L1 + 0 = sum (\<lambda> i. coeff p (i + Suc j - n) * v $ i) ?L1"
       (is "_ = sum ?G _")
       by (subst sum.cong, auto)
     also have "\<dots> = sum ?G (?L1 \<inter> {i. i + Suc j - n \<le> m} \<union> (?L1 - {i. i + Suc j - n \<le> m}))"
       (is "_ = sum _ (?L \<union> ?L')")
       by (subst sum.cong, auto)
     also have "\<dots> = sum ?G ?L + sum ?G ?L'"
       by (subst sum.union_disjoint, auto)
     also have "sum ?G ?L' = 0"
     proof -
       {
         fix x
         assume "x + Suc j - n > m" 
         with m
         have "?G x = 0" by (subst coeff_eq_0, auto)
       }
       thus ?thesis
         by (subst sum.neutral, auto)
     qed
     finally have l: "?l = sum ?G ?L" by simp
 
     let ?bij = "\<lambda> i. i + n - Suc j"
     {
       fix x
       assume x: "j < m + n" "Suc (x + j) - n \<le> m" "x < n" "n - Suc j \<le> x" 
       define y where "y = x + Suc j - n"
       from x have "x + Suc j \<ge> n" by auto
       with x have xy: "x = ?bij y" unfolding y_def by auto
       from x have y: "y \<in> ?R" unfolding y_def by auto
       have "x \<in> ?bij ` ?R" unfolding xy using y by blast
     } note tedious = this
     show ?thesis unfolding l r
       by (rule sum.reindex_cong[of ?bij], insert j, auto simp: inj_on_def tedious)
   qed
   finally show ?thesis by simp
 qed
 
 lemma sylvester_sub_poly:
   fixes p q :: "'a :: comm_semiring_0 poly"
   assumes m: "degree p \<le> m"
   assumes n: "degree q \<le> n"
   assumes v: "v \<in> carrier_vec (m+n)"
   shows "poly_of_vec ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v) =
     poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q" (is "?l = ?r")
 proof (rule poly_eqI)
   fix i
   let ?Tv = "(sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v"
   have dim: "dim_vec (vec_first v n) = n" "dim_vec (vec_last v m) = m" "dim_vec ?Tv = n + m" 
     using v by auto
   have if_distrib: "\<And> x y z. (if x then y else (0 :: 'a)) * z = (if x then y * z else 0)" 
     by auto
   show "coeff ?l i = coeff ?r i"
   proof (cases "i < m+n")
     case False
       hence i_mn: "i \<ge> m+n"
         and i_n: "\<And>x. x \<le> i \<and> x < n \<longleftrightarrow> x < n"
         and i_m: "\<And>x. x \<le> i \<and> x < m \<longleftrightarrow> x < m" by auto
       have "coeff ?r i =
             (\<Sum> x < n. vec_first v n $ (n - Suc x) * coeff p (i - x)) +
             (\<Sum> x < m. vec_last v m $ (m - Suc x) * coeff q (i - x))"
         (is "_ = sum ?f _ + sum ?g _")
         unfolding coeff_add coeff_mult Let_def 
         unfolding coeff_poly_of_vec dim if_distrib
         unfolding atMost_def
         apply(subst sum.inter_filter[symmetric],simp)
         apply(subst sum.inter_filter[symmetric],simp)
         unfolding mem_Collect_eq
         unfolding i_n i_m
         unfolding lessThan_def by simp
       also { fix x assume x: "x < n"
         have "coeff p (i-x) = 0"
           apply(rule coeff_eq_0) using i_mn x m by auto
         hence "?f x = 0" by auto
       } hence "sum ?f {..<n} = 0" by auto
       also { fix x assume x: "x < m"
         have "coeff q (i-x) = 0"
           apply(rule coeff_eq_0) using i_mn x n by auto
         hence "?g x = 0" by auto
       } hence "sum ?g {..<m} = 0" by auto
       finally have "coeff ?r i = 0" by auto
       also from False have "0 = coeff ?l i"
         unfolding coeff_poly_of_vec dim sum.distrib[symmetric] by auto
       finally show ?thesis by auto
     next case True
       hence "coeff ?l i = ((sylvester_mat_sub m n p q)\<^sup>T *\<^sub>v v) $ (n + m - Suc i)"
         unfolding coeff_poly_of_vec dim sum.distrib[symmetric] by auto
       also have "... = coeff (p * poly_of_vec (vec_first v n) + q * poly_of_vec (vec_last v m)) i"
         apply(subst index_mult_mat_vec) using True apply simp
         apply(subst row_transpose) using True apply simp
         apply(subst col_sylvester_sub)
         using True apply simp
         apply(subst vec_first_last_append[of v n m,symmetric]) using v apply(simp add: add.commute)
         apply(subst scalar_prod_append)
         apply (rule carrier_vecI,simp)+
         apply (subst vec_of_poly_rev_shifted_scalar_prod[OF m],simp) using True apply simp
         apply (subst add.commute[of n m])
         apply (subst vec_of_poly_rev_shifted_scalar_prod[OF n]) apply simp using True apply simp
         by simp
       also have "... =
         (\<Sum>x\<le>i. (if x < n then vec_first v n $ (n - Suc x) else 0) * coeff p (i - x)) +
         (\<Sum>x\<le>i. (if x < m then vec_last v m $ (m - Suc x) else 0) * coeff q (i - x))"
         unfolding coeff_poly_of_vec[of "vec_first v n",unfolded dim_vec_first,symmetric]
         unfolding coeff_poly_of_vec[of "vec_last v m",unfolded dim_vec_last,symmetric]
         unfolding coeff_mult[symmetric] by (simp add: mult.commute)
       also have "... = coeff ?r i"
         unfolding coeff_add coeff_mult Let_def
         unfolding coeff_poly_of_vec dim..
       finally show ?thesis.
   qed
 qed
 
 (**** End of the lemmas which could be moved to Algebraic_Numbers/Resultant.thy ****)
 
 (**** The following lemmas could be moved to Computational_Algebra/Polynomial.thy ****)
 
 lemma normalize_field [simp]: "normalize (a :: 'a :: {field, semiring_gcd}) = (if a = 0 then 0 else 1)"
   using unit_factor_normalize by fastforce
 
 lemma content_field [simp]: "content (p :: 'a :: {field,semiring_gcd} poly) = (if p = 0 then 0 else 1)"
   by (induct p, auto simp: content_def)
 
 lemma primitive_part_field [simp]: "primitive_part (p :: 'a :: {field,semiring_gcd} poly) = p"
   by (cases "p = 0", auto intro!: primitive_part_prim)
 
 lemma primitive_part_dvd: "primitive_part a dvd a"
   by (metis content_times_primitive_part dvd_def dvd_refl mult_smult_right)
 
 lemma degree_abs [simp]:
   "degree \<bar>p\<bar> = degree p" by (auto simp: abs_poly_def)
 
 lemma degree_gcd1:
   assumes a_not0: "a \<noteq> 0" 
   shows "degree (gcd a b) \<le> degree a"
 proof -
   let ?g = "gcd a b"
   have gcd_dvd_b: "?g dvd a" by simp
   from this obtain c where a_gc: "a = ?g * c" unfolding dvd_def by auto
   have g_not0: "?g \<noteq>0" using a_not0 a_gc by auto
   have c0: "c \<noteq> 0" using a_not0 a_gc by auto
   have "degree ?g \<le> degree (?g * c)" by (rule degree_mult_right_le[OF c0])
   also have "... = degree a" using a_gc by auto
   finally show ?thesis .  
 qed
 
 lemma primitive_part_neg [simp]:
   fixes a::"'a :: {factorial_ring_gcd,factorial_semiring_multiplicative} poly"
   shows "primitive_part (-a) = - primitive_part a"
 proof -
   have "primitive_part (-a) = primitive_part (smult (-1) a)" by auto
   then show ?thesis unfolding primitive_part_smult
     by (simp add: is_unit_unit_factor)
 qed
 
 lemma content_uminus[simp]: 
   fixes f::"int poly"
   shows "content (-f) = content f"
 proof -
   have "-f = - (smult 1 f)" by auto
   also have "... = smult (-1) f" using smult_minus_left by auto
   finally have "content (-f) = content (smult (-1) f)" by auto
   also have "... = normalize (- 1) * content f" unfolding content_smult ..
   finally show ?thesis by auto  
 qed
 
 lemma pseudo_mod_monic:
   fixes f g :: "'a::{comm_ring_1,semiring_1_no_zero_divisors} poly"
   defines "r \<equiv> pseudo_mod f g"
   assumes monic_g: "monic g"
   shows "\<exists>q.  f = g * q + r" "r = 0 \<or> degree r < degree g"
 proof -
   let ?cg = "coeff g (degree g)"
   let ?cge = "?cg ^ (Suc (degree f) - degree g)"
   define a where "a = ?cge"
   from r_def[unfolded pseudo_mod_def] obtain q where pdm: "pseudo_divmod f g = (q, r)"
     by (cases "pseudo_divmod f g") auto
   have g: "g \<noteq> 0" using monic_g by auto
   from pseudo_divmod[OF g pdm] have id: "smult a f = g * q + r" and "r = 0 \<or> degree r < degree g"
     by (auto simp: a_def)
   have a1: "a = 1" unfolding a_def using monic_g by auto
   hence id2: "f = g * q + r" using id by auto  
   show "r = 0 \<or> degree r < degree g" by fact  
   from g have "a \<noteq> 0"
     by (auto simp: a_def)  
   with id2 show "\<exists>q. f = g * q + r"
     by auto
 qed
 
 lemma monic_imp_div_mod_int_poly_degree: 
   fixes p :: "'a::{comm_ring_1,semiring_1_no_zero_divisors} poly"
   assumes m: "monic u"
   shows "\<exists>q r. p = q*u + r \<and> (r = 0 \<or> degree r < degree u)" 
   using pseudo_mod_monic[OF m] using mult.commute by metis
 
 corollary monic_imp_div_mod_int_poly_degree2: 
   fixes p :: "'a::{comm_ring_1,semiring_1_no_zero_divisors} poly"
   assumes m: "monic u" and deg_u: "degree u > 0"
   shows "\<exists>q r. p = q*u + r \<and> (degree r < degree u)"
 proof -  
   obtain q r where "p = q * u + r" and r: "(r = 0 \<or> degree r < degree u)" 
       using monic_imp_div_mod_int_poly_degree[OF m, of p] by auto
     moreover have "degree r < degree u" using deg_u r by auto  
   ultimately show ?thesis by auto
 qed
 (**** End of the lemmas that could be moved to Computational_Algebra/Polynomial.thy ****)
 
 
 (* To be categorized *)
 lemma (in zero_hom) hom_upper_triangular:
   "A \<in> carrier_mat n n \<Longrightarrow> upper_triangular A \<Longrightarrow> upper_triangular (map_mat hom A)"
   by (auto simp: upper_triangular_def)
 
 end
diff --git a/thys/Store_Buffer_Reduction/Text.thy b/thys/Store_Buffer_Reduction/Text.thy
--- a/thys/Store_Buffer_Reduction/Text.thy
+++ b/thys/Store_Buffer_Reduction/Text.thy
@@ -1,1066 +1,1066 @@
 (*<*)
 theory Text
 imports Variants 
 begin
 (*>*)
 section \<open>Programming discipline \label{sec:discipline}\<close>
 
 text \<open>
 For sequential code on a single processor the store buffer is invisible, since reads respect outstanding writes in the buffer. 
 This argument can be extended to thread local memory in the context of a multiprocessor architecture. 
 Memory typically becomes temporarily thread local by means of locking. 
 The C-idiom to identify shared portions of the memory is the \texttt{volatile} 
 tag on variables and type declarations. 
 Thread local memory can be accessed non-volatilely, whereas accesses to shared memory are tagged as volatile. 
 This prevents the compiler from applying certain optimizations to those accesses which could cause undesired behavior, \eg to store intermediate values in registers instead of writing them to the memory.
 
   The basic idea behind the programming discipline is, that before gathering new information about the shared state (via reading) the thread has to make its outstanding changes to the shared state visible to others (by flushing the store buffer). 
 This allows to sequentialize the reads and writes to obtain a sequentially consistent execution of the global system. 
 In this sequentialization a write to shared memory happens when the write instruction exits the store buffer, and a read from the shared memory happens when all preceding writes have exited. 
 
 We distinguish thread local and shared memory by an ownership model. 
 Ownership is maintained in ghost state and can be transferred as side effect of write operations and by a dedicated ghost operation.
 Every thread has a set of owned addresses. Owned addresses of different threads are disjoint. 
 Moreover, there is a global set of shared addresses which can additionally be marked as read-only. 
 Unowned addresses --- addresses owned by no thread --- can be accessed concurrently by all threads. They are a subset of the shared addresses. The read-only addresses are a subset of the unowned addresses (and thus of the shared addresses).
 We only allow a thread to write to owned addresses and unowned, read-write addresses.
 We only allow a thread to read from owned addresses and from shared addresses (even if they are owned by another thread).
 
 All writes to shared memory have to be volatile. Reads from shared addresses also have to be volatile, except if the address is owned (\ie single writer, multiple readers) or if the address is read-only. Moreover, non-volatile writes are restricted to owned, unshared memory.
 As long as a thread owns an address it is guaranteed that it is the only one writing to that address. Hence this thread can safely perform non-volatile reads to that address without missing any write. Similar it is safe for any thread to access read-only memory via non-volatile reads since there are no outstanding writes at all.
 
 
 Recall that a volatile read is \Def{clean} if it is guaranteed that there is no outstanding volatile write (to any address) in the store buffer. Moreover every non-volatile read is clean.
 To regain sequential consistency under the presence of store buffers every thread has to make sure that every read is clean, by flushing the store buffer when necessary. To check the flushing policy of a thread, we keep track of clean reads by means of ghost state. For every thread we maintain a dirty flag. It is reset as the store buffer gets flushed. Upon a volatile write the dirty flag is set. The dirty flag is considered to guarantee that a volatile read is clean.  
 
 
 
 Table \ref{tab:access-grid} summarizes the access policy and Table \ref{tab:flushing} the associated flushing policy of the programming discipline.
 The key motivation is to improve performance by minimizing the number of store buffer flushes, 
 while staying sequentially consistent.
 The need for flushing the store buffer decreases from interlocked accesses (where flushing is a side-effect) over volatile accesses to non-volatile accesses. From the viewpoint of access rights there is no difference between interlocked and volatile accesses. However, keep in mind that some interlocked operations can read from, modify and write to an address in a single atomic step of the underlying hardware and are typically used in lock-free algorithms or for the implementation of locks.
 
 
 
 \begin{table}
 \centering
 \caption{Programming discipline.}
 \captionsetup[table]{position=top}
 \captionsetup[subtable]{position=top}
 \newcommand{\mycomment}[1]{}
 \subfloat[Access policy\label{tab:access-grid}]{
 \begin{tabular}{m{1.2cm}@ {\hspace{2mm}}m{1.7cm}@ {\hspace{3mm}}m{1.8cm}m{2.2 cm}}
 \toprule
                &     shared        &   shared   &  unshared            \\
                &     (read-write)  &   (read-only)   &                 \\
 \midrule
 unowned        & \mycomment{iRW, iR, iW,} vR, vW         & \mycomment{iR,} vR, R              &  unreachable\\
 owned          & \mycomment{iRW, iR, iW,} vR, vW, R      & unreachable            &  \mycomment{iRW, iR, iW,} vR, vW, R, W \\
 owned \mbox{by other} & \mycomment{iR,}       vR                & unreachable            &                           \\
 
 \bottomrule
 \multicolumn{4}{l}{(v)olatile, (R)ead, (W)rite}\\
 \multicolumn{4}{l}{all reads have to be clean }
 \end{tabular}
 %\caption{Access policy \label{tab:access-grid}}
 }\hspace{0.3cm}
 %
 %\end{table}
 %
 %\begin{table}
 %
 \subfloat[Flushing policy\label{tab:flushing}]{
 \begin{tabular}{lc}
 \toprule
                 & flush (before)          \\     
 \midrule
 interlocked     & as side effect                 \\
 vR            & if not clean               \\
 R, vW, W           & never                  \\
 \bottomrule
 \end{tabular}
 %\caption{Flushing policy \label{tab:flushing}}
 }
 
 \end{table}
 
 
 \<close>
 section \<open>Formalization \label{sec:formalization}\<close>
 
 text \<open>
 
 In this section we go into the details of our formalization. In our model, we distinguish the plain `memory system' from the 
 `programming language semantics' which we both describe as a small-step transition relation. 
 During a computation the programming language issues memory instructions (read / write) to the memory system, 
 which itself returns the results in temporary registers. 
 This clean interface allows us to parameterize the program semantics over the 
 memory system. Our main theorem allows us to simulate a computation step in the semantics based on a 
 memory system with store buffers by @{term "n"} steps in the semantics based on a   
 sequentially consistent memory system. 
 We refer to the former one as \Def{store buffer machine}  and to the latter one as \Def{virtual machine}. The simulation theorem is independent of the programming language.
 
 We continue with introducing the common parts of both machines. 
 In Section \ref{sec:storebuffermachine} we describe the store buffer machine and in Section \ref{sec:virtualmachine} we then describe the virtual machine. The main reduction theorem is presented in \ref{sec:reduction}.
 
 \medskip
 Addresses @{term "a"}, values @{term "v"} and temporaries @{term "t"} are natural numbers. 
 Ghost annotations for manipulating the ownership information are the following sets of addresses: the acquired addresses @{term "A"}, the unshared (local) fraction @{term "L"} of the acquired addresses, the released addresses @{term "R"} and the writable fraction @{term "W"} of the released addresses (the remaining addresses are considered read-only). 
 These ownership annotations are considered as side-effects on volatile writes and interlocked operations (in case a write is performed). 
 Moreover, a special ghost instruction allows to transfer ownership.
 The possible status changes of an address due to these ownership transfer operations are depicted in Figure \ref{fig:ownership-transfer}. Note that ownership of an address is not directly transferred between threads, but is first released by one thread and then can be acquired by another thread.
 %
 \begin{figure}
 \begin{center}
 \begin{tikzpicture}
 [auto,
  outernode/.style    = {rectangle, rounded corners, draw, text centered, minimum height=3cm, minimum width=2.7cm, fill=gray!20},
  innernode/.style  = {rectangle, rounded corners, draw, text centered, minimum height=1cm, minimum width=1cm, text width=1.5cm, fill=white}
 ]
 \node[outernode] (owned) {};
 \node[innernode] (oshared)  [below] at ($ (owned.north) -(0,0.2cm) $) {shared read-write};
 \node[innernode] (onshared) [above] at ($ (owned.south) +(0,0.2cm) $) {unshared};
 \node[above] at (owned.north) {owned};
 
 \node[outernode] (unowned) [right] at ($ (owned.east) +(1.5cm,0cm) $) {};
 \node[innernode] (rwshared)  [below] at ($ (unowned.north) -(0,0.2cm) $) {shared read-write};
 \node[innernode] (roshared) [above] at ($ (unowned.south) +(0,0.2cm) $) {shared read-only};
 \node[above] at (unowned.north) {unowned};
 
 \path (rwshared.east) -- coordinate (middlex) (oshared.west);
 
 \draw[->] (owned.east |- rwshared.170) -- (rwshared.170); 
   \node [above] at (rwshared.170 -| middlex) {@{term "R \<inter> W"}};
 
 \draw[->] (unowned.west |- oshared.350) -- (oshared.350);
   \node [below] at (oshared.350 -| middlex) {@{term "A \<inter> - L"}};
 
 \draw[->] (unowned.west |- onshared.350) -- (onshared.350);
   \node [below] at (onshared.350 -| middlex) {@{term "A \<inter> L"}};
 
 \draw[->] (owned.east |- roshared.170) -- (roshared.170);
   \node [above] at (roshared.170 -| middlex) {@{term "R \<inter> - W"}};
 
 
 \draw[->] (oshared.292) -- node {@{term "A \<inter> L"}} (onshared.68);
 \draw[->] (onshared.84) -- node {@{term "A \<inter> - L"}} (oshared.276);
 
 \node (legende) [below right] at (owned.south west) {(A)cquire, keep (L)ocal; (R)elease, mark (W)riteable };
 \end{tikzpicture}
 \end{center}
 
 \caption{Ownership transfer \label{fig:ownership-transfer}}
 \end{figure}
 %
 A memory instruction is a datatype with the following constructors:
 \begin{itemize}
 \item @{term "Read volatile a t"} for reading from address @{term "a"} to temporary @{term "t"}, where the Boolean @{term "volatile"} determines whether the access is volatile or not.
 \item @{term "Write volatile a sop A L R W"} to write the result of evaluating the store operation @{term "sop"} at address @{term "a"}. A store operation is a pair @{term "(D,f)"}, with the domain @{term "D"} and the function @{term "f"}.
 The function @{term "f"} takes temporaries @{term "\<theta>"} as a parameter, which maps a temporary to a value. 
 The subset of temporaries that is considered by function @{term "f"} is specified by the domain @{term "D"}.
 We consider store operations as valid when they only depend on their domain: 
 @{thm [display]"valid_sop_def" [simplified conj_to_impl [symmetric], no_vars]}
 Again the Boolean @{term "volatile"} specifies the kind of memory access.
 \item @{term "RMW a t sop cond ret A L R W"}, for atomic interlocked `read-modify-write' instructions (flushing the store buffer). First the value at address @{term "a"} is loaded to temporary @{term "t"}, and then the condition @{term "cond"} on the temporaries is considered to decide whether a store operation is also executed. In case of a store the function @{term "ret"}, depending on both the old value at address @{term "a"} and the new value (according to store operation @{term "sop"}), specifies the final result stored in temporary @{term "t"}. With a trivial condition @{term "cond"} this instruction also covers interlocked reads and writes.
 \item @{term "Fence"}, a memory fence that flushes the store buffer. %todo: rename to flush?
 \item @{term "Ghost A L R W"} for ownership transfer.
 \end{itemize}
 
 \<close>
 
 subsection \<open>Store buffer machine \label{sec:storebuffermachine}\<close>
 
 text (in program) \<open>
 For the store buffer machine the configuration of a single thread is a tuple @{term "(p, is, \<theta>, sb)"} consisting of the program state @{term "p"}, a memory instruction list @{term "is"}, the map of temporaries @{term "\<theta>"} and the store buffer @{term "sb"}. A global configuration of the store buffer machine @{term "(ts, m)"} consists of a list of thread configurations @{term "ts"} and the memory @{term "m"}, which is a function from addresses to values. 
 
 
 We describe the computation of the global system by the non-deterministic transition relation @{term "(ts, m, ()) \<Rightarrow>\<^sub>s\<^sub>b (ts', m',())"} defined in Figure~\ref{fig:global-transitions}. 
 
 \begin{figure}[H]
 \begin{center}
 @{thm [mode=Rule] store_buffer.concurrent_step.Program 
                     [where \<D>="()" and \<O>="()" and \<R>="()" and \<S>="()",no_vars]}\\[0.5\baselineskip]
 @{thm [mode=Rule] store_buffer.concurrent_step.Memop [where \<D>="()" and \<O>="()" and \<R>="()" and \<S>="()"
                 and \<D>'="()" and \<O>'="()" and \<R>'="()" and \<S>'="()",no_vars]}\\[0.5\baselineskip]
 @{thm [mode=Rule] store_buffer.concurrent_step.StoreBuffer [where \<D>="()" and \<O>="()" and \<R>="()" and \<S>="()" and  \<O>'="()" and \<R>'="()" and \<S>'="()",no_vars]}
 \end{center}
 \caption{Global transitions of store buffer machine\label{fig:global-transitions}}
 \end{figure}
 
 A transition selects a thread @{term "ts!i = (p,is,\<theta>,sb,(),())"} and either the `program' the `memory'  or the `store buffer' makes a step defined by sub-relations. 
 
 The program step relation is a parameter to the global 
 transition relation. A program step @{thm (prem 3) "store_buffer.concurrent_step.Program" [no_vars]} takes the temporaries @{term "\<theta>"} and the current program state @{term "p"} and makes a step by returning a new program state @{term "p'"} and an instruction list @{term "is'"} which is appended to the remaining instructions. 
 
 A memory step @{thm (prem 3) "store_buffer.concurrent_step.Memop" [where \<D>="()" and \<O>="()" and \<R>="()" and \<S>="()"
                 and \<D>'="()" and \<O>'="()" and \<R>'="()" and \<S>'="()",no_vars]} of a machine with store buffer may only fill its store buffer with new writes.
 
 In a store buffer step @{thm (prem 3) "store_buffer.concurrent_step.StoreBuffer" [where \<D>="()" and \<O>="()" and \<R>="()" and \<S>="()" and  \<O>'="()" and \<R>'="()" and \<S>'="()",no_vars]} the store buffer may release outstanding writes to the memory.
 
 The store buffer maintains the list of outstanding memory writes. 
 Write instructions are appended to the end of the store buffer and emerge to memory from the front of the list. A read instructions is satisfied from the store buffer if possible. 
 An entry in the store buffer is of the form @{term "Write\<^sub>s\<^sub>b volatile a sop v"} for an outstanding write (keeping the volatile flag), where operation @{term "sop"} evaluated to value @{term "v"}.
 
 As defined in Figure \ref{fig:store-buffer-transition} a write updates the memory when it exits the store buffer.
 %
 \begin{figure}
 \begin{center}
 @{thm [mode=Axiom] SBWrite\<^sub>s\<^sub>b [where rs=sb and \<O>="()" and \<R>="()" and \<S>="()", no_vars]}\\[0.5\baselineskip]
 \end{center}
 \caption{Store buffer transition \label{fig:store-buffer-transition}}
 \end{figure}
 %
 
 The memory transition are defined in Figure \ref{fig:store-buffer-memory}.
 %
 \begin{figure}
 \begin{center}
 @{thm [mode=Rule] SBRead [where ghst="((),(),(),())",no_vars]}\\[0.5\baselineskip]
 @{thm [mode=Rule] SBWrite' [where ghst="((),(),(),())",no_vars]}\\[0.5\baselineskip]
 @{thm [mode=Rule] SBRMWReadOnly' [where ghst="((),(),(),())",no_vars]}\\[0.5\baselineskip]
 @{thm [mode=Rule] SBRMWWrite' [where ghst="((),(),(),())",no_vars]}\\[-0.3\baselineskip]
 @{thm [mode=Axiom] sb_memop_step.SBFence [where \<D>="()" and \<O>="()" and \<R>="()" and \<S>="()",no_vars]}\\[-0.3\baselineskip]
 @{thm [mode=Axiom] sb_memop_step.SBGhost [where \<D>="()" and \<O>="()" and \<R>="()" and \<S>="()",no_vars]}
 \end{center}
 \caption{Memory transitions of store buffer machine\label{fig:store-buffer-memory}}
 \end{figure}
 %
 With @{term "buffered_val sb a"} we obtain the value of the last write to address @{term "a"} which is still pending in the store buffer. 
 In case no outstanding write is in the store buffer we read from the memory. 
 Store operations have no immediate effect on the memory but are queued in the store buffer instead. 
 Interlocked operations and the fence operation require an empty store buffer, which means that it has to be flushed before the action can take place. 
 The read-modify-write instruction first adds the current value at address @{term "a"} to temporary @{term "t"} and then checks the store condition @{term "cond"} on the temporaries. 
 If it fails this read is the final result of the operation. 
 Otherwise the store is performed. 
 The resulting value of the temporary @{term "t"} is specified by the function @{term "ret"} which considers both the old and new value as input. 
 The fence and the ghost instruction are just skipped.
 
 
 
 \<close>
 subsection \<open>Virtual machine \label{sec:virtualmachine}\<close>
 text (in program) \<open>
 The virtual machine is a sequentially consistent machine without store buffers, maintaining additional ghost state to check for the programming discipline.
 A thread configuration is a tuple @{term "(p, is, \<theta>, (), \<D>, \<O>,())"}, with a dirty flag @{term "\<D>"} indicating whether there may be an outstanding volatile write in the store buffer and the set of owned addresses @{term "\<O>"}. 
 The dirty flag @{term "\<D>"} is considered to specify if a read is clean: for \emph{all} volatile reads the dirty flag must not be set.
 The global configuration of the virtual machine @{term "(ts, m,\<S>)"} maintains a Boolean map of shared addresses @{term "\<S>"} (indicating write permission).
 Addresses in the domain of mapping @{term "\<S>"} are considered shared and the set of read-only addresses is obtained  from @{term "\<S>"} by: @{thm "read_only_def" [no_vars]}
 
 According to the rules in Fig \ref{fig:global-virtual-step} a global transition of the virtual machine 
 @{term "(ts, m, \<S>) \<Rightarrow>\<^sub>v (ts', m', \<S>')"} is either a program or a memory step.
 %
 \begin{figure}
 \begin{center}
 @{thm [mode=Rule] virtual.concurrent_step.Program [where sb="()" and \<R>="()", no_vars]}\\[0.5\baselineskip]
 @{thm [mode=Rule] virtual.concurrent_step.Memop [where sb="()" and sb'="()" and \<R>="()" and \<R>'="()",no_vars]}
 \end{center}
 \caption{Global transitions of virtual machine \label{fig:global-virtual-step}}
 \end{figure}
 The transition rules for its memory system are defined in Figure~\ref{fig:virtual-memory}.
 %
 \begin{figure}
 \begin{center}
 @{thm [mode=Axiom] VRead [no_vars]}\\[-0.3\baselineskip]
 @{thm [mode=Axiom] VWriteNonVolatile [no_vars]}\\[0.5\baselineskip]
 @{thm [mode=Rule] VWriteVolatile [where \<R>="()",no_vars]}\\[0.5\baselineskip]
 @{thm [mode=Rule] VRMWReadOnly [where \<R>="()",no_vars]}\\[0.5\baselineskip]
 @{thm [mode=Rule] VRMWWrite [where \<R>="()",no_vars]}\\[0.5\baselineskip]
 @{thm [mode=Rule] VFence [where \<R>="()",no_vars]}\\[0.5\baselineskip]
 @{thm [mode=Rule] VGhost [where \<R>="()", no_vars]}\\[0.1\baselineskip]
 \end{center}
 \caption{Memory transitions of the virtual machine \label{fig:virtual-memory}}
 \end{figure}
 %
 In addition to the transition rules for the virtual machine we introduce the \emph{safety} judgment @{term "\<O>s,i\<turnstile> (is, \<theta>, m, \<D>, \<O>, \<S>)\<surd>"} in Figure~\ref{fig:safe-virtual-memory}, where @{term "\<O>s"} is the list of ownership sets obtained from the thread list @{term "ts"} and @{term "i"} is the index of the current thread.
 Safety of all reachable states of the virtual machine ensures that the programming discipline is obeyed by the program and is our formal prerequisite for the simulation theorem.
 It is left as a proof obligation to be discharged by means of a proper program logic for sequentially consistent executions.
 %
 \begin{figure}
 \begin{center}
 @{thm [mode=Rule] safe_direct_memop_state.Read [no_vars]}\\[0.5\baselineskip]
 @{thm [mode=Rule] safe_direct_memop_state.WriteNonVolatile [no_vars]}\\[0.5\baselineskip]
 @{thm [mode=Rule] SafeWriteVolatile [no_vars]}\\[0.5\baselineskip]
 @{thm [mode=Rule] SafeRMWReadOnly [no_vars]}\\[0.5\baselineskip]
 @{thm [mode=Rule] SafeRMWWrite [no_vars]}\\[-0.3\baselineskip]
 @{thm [mode=Axiom] safe_direct_memop_state.Fence [no_vars]}\\[0.5\baselineskip]
 @{thm [mode=Rule] safe_direct_memop_state.Ghost [no_vars]}\\[0.1\baselineskip]
 \end{center}
 \caption{Safe configurations of a virtual machine \label{fig:safe-virtual-memory}}
 \end{figure}
 %
 %
 In the following we elaborate on the rules of Figures \ref{fig:virtual-memory} and \ref{fig:safe-virtual-memory} in parallel.
 To read from an address it either has to be owned or read-only or it has to be volatile and shared. Moreover the read has to be clean.
 %TODO: mention the difference distinction of 'single writer' that covered by this: for 'owned and shared' non-volatile read is ok
 The memory content of address @{term "a"} is stored in temporary @{term "t"}. 
 %
 Non-volatile writes are only allowed to owned and unshared addresses. 
 The result is written directly into the memory. 
 %
 A volatile write is only allowed when no other thread owns the address and the address is not marked as read-only.
 Simultaneously with the volatile write we can transfer ownership as specified by the annotations @{term "A"}, @{term "L"}, @{term "R"} and @{term "W"}. 
 The acquired addresses @{term "A"} must not be owned by any other thread and stem from the shared addresses or are already owned.
 Reacquiring owned addresses can be used to change the shared-status via the set of local addresses @{term "L"} which have to be a subset of @{term "A"}. 
 The released addresses @{term "R"} have to be owned and distinct from the acquired addresses @{term "A"}. 
 After the write the new ownership set of the thread is obtained by adding the acquired addresses @{term "A"} and releasing the addresses @{term "R"}: @{term "\<O> \<union> A - R"}. The released addresses @{term "R"} are augmented to the shared addresses @{term "S"} and the local addresses @{term "L"} are removed. We also take care about the write permissions in the shared state: the released addresses in set @{term "W"} as well as the acquired addresses are marked writable: @{term "\<S> \<oplus>\<^bsub>W\<^esub> R \<ominus>\<^bsub>A\<^esub> L"}. The auxiliary ternary operators to augment and subtract addresses from the sharing map are defined as follows:
 
 @{thm [display] augment_shared_def [where S=R, no_vars]}
 @{thm [display,margin=80] restrict_shared_def [no_vars]}
 
 The read-modify-write instruction first adds the current value at address @{term "a"} to temporary @{term "t"} and then checks the store condition @{term "cond"} on the temporaries. 
 If it fails this read is the final result of the operation. 
 Otherwise the store is performed. 
 The resulting value of the temporary @{term "t"} is specified by the function @{term "ret"} which considers both the old and new value as input. 
 As the read-modify-write instruction is an interlocked operation which flushes the store buffer as a side effect the dirty flag @{term "\<D>"} is reset.
 The other effects on the ghost state and the safety sideconditions are the same as for the volatile read and volatile write, respectively.
 
 The only effect of the fence instruction in the system without store buffer is to reset the dirty flag.
 
 The ghost instruction @{term "Ghost A L R W"} allows to transfer ownership when no write is involved \ie when merely reading from memory. It has the same safety requirements as the corresponding parts in the write instructions. 
 \<close>
 
 subsection \<open>Reduction \label{sec:reduction}\<close>
 
 text (in xvalid_program_progress) \<open>
 The reduction theorem we aim at reduces a computation of a machine with store buffers to a sequential consistent computation of the virtual machine. We formulate this as a
  simulation theorem which states that a computation of the store buffer machine @{term "(ts\<^sub>s\<^sub>b,m,()) \<Rightarrow>\<^sub>s\<^sub>b\<^sup>* (ts\<^sub>s\<^sub>b',m',())"} can be simulated by a computation of the virtual machine @{term "(ts,m,\<S>) \<Rightarrow>\<^sub>v\<^sup>* (ts',m',\<S>')"}. 
 The main theorem only considers computations that start in an initial configuration where all store buffers are empty and end in a configuration where all store buffers are empty again. A configuration of the store buffer machine is obtained from a virtual configuration by removing all ghost components and assuming empty store buffers. This coupling relation between the thread configurations is written as @{term "ts\<^sub>s\<^sub>b \<sim>\<^sub>d ts"}. Moreover, the precondition  @{term "initial\<^sub>v ts \<S> valid"} ensures that the ghost state of the initial configuration of the virtual machine is properly initialized: the ownership sets of the threads are distinct, an address marked as read-only (according to @{term \<S>}) is unowned and every unowned address is shared. %TODO (ommit): and the instruction lists are empty. 
 Finally with @{term [names_short] "safe_reach_virtual_free_flowing (ts,m,S)"} we ensure conformance to the programming discipline by assuming that all reachable configuration in the virtual machine are safe (according to the rules in Figure~\ref{fig:safe-virtual-memory}). 
 %
 \begin{theorem}[Reduction]\label{thm:reduction}
 @{thm [display,   mode=compact, mode=holimplnl, margin=90,names_short]  store_buffer_execution_result_sequential_consistent'_hol [where x="()" and x'="()",no_vars]}
 \end{theorem}
 %
 This theorem captures our intiution that every result that can be obtained from a computation of the store buffer machine can also be obtained by a sequentially consistent computation. However, to prove it we need some generalizations that we sketch in the following sections. First of all the theorem is not inductive as we do not consider arbitrary intermediate configurations but only those where all store buffers are empty. For intermediate confiugrations the coupling relation becomes more involved. The major obstacle is that a volatile read (from memory) can overtake non-volatile writes that are still in the store-buffer and have not yet emerged to memory. Keep in mind that our programming discipline only ensures that no \emph{volatile} writes can be in the store buffer the moment we do a volatile read, outstanding non-volatile writes are allowed. This reordering of operations is reflected in the coupling relation for intermediate configurations as discussed in the following section.
 \<close>
 
 section \<open>Building blocks of the proof \label{sec:buildingblocks}\<close>
 
 text (in program) \<open>
 A corner stone of the proof is a proper coupling relation between an \emph{intermediate} configuration of a machine with store buffers and the virtual machine without store buffers. 
 It allows us to simulate every computation step of the store buffer machine by a sequence of steps (potentially empty) on the virtual machine. 
 This transformation is essentially a sequentialization of the trace of the store buffer machine. 
 When a thread of the store buffer machine executes a non-volatile operation, it only accesses memory which is not modified by any other thread (it is either owned or read-only). 
 Although a non-volatile store is buffered, we can immediately execute it on the virtual machine, as there is no competing store of another thread. 
 However, with volatile writes we have to be careful, since concurrent threads may also compete with some volatile write to the same address. 
 At the moment the volatile write enters the store buffer we do not yet know when it will be issued to memory and how it is ordered relatively to other outstanding writes of other threads.
 We therefore have to suspend the write on the virtual machine from the moment it enters the store buffer to the moment it is issued to memory.
 For volatile reads our programming discipline guarantees that there is no volatile write in the store buffer by flushing the store buffer if necessary. 
 So there are at most some outstanding non-volatile writes in the store buffer, which are already executed on the virtual machine, as described before.
 One simple coupling relation one may think of is to suspend the whole store buffer as not yet executed intructions of the virtual machine. However, consider the following scenario. A thread is reading from a volatile address. 
 It can still have non-volatile writes in its store buffer. 
 Hence the read would be suspended in the virutal machine, and other writes to the address (e.g. interlocked or volatile writes of another thread) could invalidate the value.
 Altogether this suggests the following refined coupling relation: the state of the virtual machine is obtained from the state of the store buffer machine, by executing each store buffer until we reach the first volatile write. 
 The remaining store buffer entries are suspended as instructions. As we only execute non volatile writes the order in which we execute the store buffers should be irrelevant.
 This coupling relation allows a volatile read to be simulated immediately on the virtual machine as it happens on the store buffer machine. 
  
 From the viewpoint of the memory the virtual machine is ahead of the store buffer machine, as leading non-volatile writes already took effect on the memory of the virtual machine while they are still pending in the store buffer. 
 However, if there is a volatile write in the store buffer the corresponding thread in the virtual machine is suspended until the write leaves the store buffer. 
 So from the viewpoint of the already executed instructions the store buffer machine is ahead of the virtual machine. To keep track of this delay we introduce a variant of the store buffer machine below, which maintains the history of executed instructions in the store buffer (including reads and program steps). Moreover, the intermediate machine also maintains the ghost state of the virtual machine to support the coupling relation. We also introduce a refined version of the virutal machine below, which we try to motivate now.
 Esentially the programming discipline only allows races between volatile (or interlocked) operations. By race we mean two competing memory accesses of different threads of which at least one is a write. 
 For example the discipline guarantees that a volatile read may not be invalidated by a non-volatile write of another thread. 
 While proving the simulation theorem this manifests in the argument that a read of the store-buffer machine and the virtual machine sees the same value in both machines: the value seen by a  read in the store buffer machine stays valid as long as it has not yet made its way out in the virtual machine. 
 To rule out certain races from the execution traces we make use of the programming discipline, which is formalized in the safety of all reachable configurations of the virtual machine. Some races can be ruled out by continuing the computation of the virtual machine until we reach a safety violation. 
 However, some cannot be ruled out by the future computation of the current trace, but can be invalidated by a safety violation of another trace that deviated from the current one at some point in the past. Consider two threads. 
 Thread 1 attempts to do a volatile read from address @{term a} which is currently owned (and not shared) by thread 2, which attempts to do a non-volatile write on @{term a} with value @{term "42::nat"} and then release the address. 
 In this configuration there is already a safety violation. Thread 1 is not allowed to perform a volatile read from an address that is not shared. 
 However, when Thread 2 has executed his update and has released ownership (both are non-volatile operations) there is no safety violation anymore. 
 Unfortunately this is the state of the virtual machine when we consider the instructions of Thread 2 to be in the store buffer. The store buffer machine and the virtual machine are out of sync. 
 Whereas in the virtual machine Thread 1 will already read @{term "42::nat"} (all non-volatile writes are already executed in the virtual machine), the non-volatile write may still be pending in the store buffer of Thread 2 and hence Thread 1 reads the old value in the store buffer machine.
 This kind of issues arise when a thread has released ownership in the middle of non-volatile operations of the virtual machine, but the next volatile write of this thread has not yet made its way out of the store buffer. 
 When another thread races for the released address in this situation there is always another scheduling of the virtual machine where the release has not yet taken place and we get a safety violation. 
 To make these safety violations visible until the next volatile write we introduce another ghost component that keeps track of the released addresses. 
 It is augmented when an ghost operation releases an address and is reset as the next volatile write is reached.
 Moreover, we refine our rules for safety to take these released addresses into account. 
 For example, a write to an released address of another thread is forbidden. 
 We refer to these refined model as \emph{delayed releases} (as no other thread can acquire the address as long as it is still in the set of released addresses) and to our original model as \emph{free flowing releases} (as the effect of a release immediate takes place at the point of the ghost instruction). 
 Note that this only affects ownership transfer due to the @{term Ghost} instruction. 
 Ownership transfer together with volatile (or interlocked) writes happen simultaneously in both models.
 
 Note that the refined rules for delayed releases are just an intermediate step in our proof. 
 They do not have to be considered for the final programming discipline. As sketched above we can show in a separate theorem that a safety violation in a trace with respect to delayed releases implies a safety violation of a (potenitally other) trace with respect to free flowing releases. Both notions of safety collaps in all configurations where there are no released addresses, like the initial state. So if all reachable configurations are safe with respect to free flowing releases they are also safe with respect to delayed releases. This allows us to use the stricter policy of delayed releases for the simulation proof.
 Before continuing with the coupling relation, we introduce the refined intermediate models for delayed releases and store buffers with history information. 
 
 \<close>
 
 subsection \<open>Intermediate models\<close>
 
 text (in program) \<open>
 We begin with the virtual machine with delayed releases, for which the memory transitions 
 @{term "(is,\<theta>,(),m,\<D>,\<O>,\<R>,\<S>) \<rightarrow> (is',\<theta>',(),m',\<D>',\<O>',\<R>',\<S>')"}
 are defined Figure \ref{fig:virtual-delayed-memory}.
 %
 \begin{figure}
 \begin{center}
 @{thm [mode=Axiom] DRead [where x="()",no_vars]}\\[-0.3\baselineskip]
 @{thm [mode=Axiom] DWriteNonVolatile [where x="()",no_vars]}\\[0.5\baselineskip]
 @{thm [mode=Rule,names_short] DWriteVolatile [where x="()",no_vars]}\\[0.5\baselineskip]
 @{thm [mode=Rule,names_short] DRMWReadOnly [where x="()",no_vars]}\\[0.5\baselineskip]
 @{thm [mode=Rule,names_short] DRMWWrite [where x="()",no_vars]}\\[-0.3\baselineskip]
 @{thm [mode=Axiom,names_short] direct_memop_step.Fence [where x="()",no_vars]}\\[0.5\baselineskip]
 @{thm [mode=Rule] DGhost [where x="()",no_vars]}\\[0.1\baselineskip]
 \end{center}
 \caption{Memory transitions of the virtual machine with delayed releases\label{fig:virtual-delayed-memory}}
 \end{figure}
 %
 The additional ghost component @{term "\<R>"} is a mapping from addresses to a Boolean flag. If an address is in the domain of @{term \<R>} it was released. The boolean flag is considered to figure out if the released address was previously shared or not. In case the flag is @{term True} it was shared otherwise not. This subtle distinction is necessary to properly handle volatile reads. A volatile read from an address owned by another thread is fine as long as it is marked as shared. The released addresses @{term \<R>} are reset at every volatile write as well as interlocked operations and the fence instruction. They are augmented at the ghost instruction taking the sharing information into account:
 
 @{thm [display] augment_rels_def [where S="dom \<S>", no_vars]}
 
 If an address is freshly released (@{term "a \<in> R"} and @{term "\<R> a = None"}) the flag is set according to @{term "dom \<S>"}. Otherwise the flag becomes @{term "Some False"} in case the released address is currently unshared.
 Note that with this definition @{term "\<R> a = Some False"} stays stable upon every new release and we do not loose information about a release of an unshared address.
 
 The global transition @{term "(ts, m, s) \<Rightarrow>\<^sub>d (ts',m',s')"} are analogous to the rules in Figure \ref{fig:global-virtual-step} replacing the memory transtions with the refined version for delayed releases.
 
 The safety judgment for delayed releases @{term "\<O>s,\<R>s,i\<turnstile> (is, \<theta>, m, \<D>, \<O>, \<S>)\<surd>"} is defined in Figure \ref{fig:safe-delayed}. Note the additional component @{term \<R>s} which is the list of release maps of all threads.
 %
 \begin{figure}
 \begin{center}
 @{thm [mode=Rule] safe_delayed_direct_memop_state.Read [no_vars]}\\[0.5\baselineskip]
 @{thm [mode=Rule] safe_delayed_direct_memop_state.WriteNonVolatile [no_vars]}\\[0.5\baselineskip]
 @{thm [mode=Rule] SafeDelayedWriteVolatile [no_vars]}\\[0.5\baselineskip]
 @{thm [mode=Rule] SafeDelayedRMWReadOnly [no_vars]}\\[0.5\baselineskip]
 @{thm [mode=Rule] SafeDelayedRMWWrite [no_vars]}\\[-0.3\baselineskip]
 @{thm [mode=Axiom] safe_delayed_direct_memop_state.Fence [no_vars]}\\[0.5\baselineskip]
 @{thm [mode=Rule] safe_delayed_direct_memop_state.Ghost [no_vars]}\\[0.1\baselineskip]
 @{thm [mode=Rule] safe_delayed_direct_memop_state.Nil [no_vars]}\\[0.1\baselineskip]
 \end{center}
 \caption{Safe configurations of a virtual machine (delayed-releases) \label{fig:safe-delayed}}
 \end{figure}
 %
 The rules are strict extensions of the rules in Figure \ref{fig:safe-virtual-memory}: writing or acquiring an address @{term a} is only allowed if the address is not in the release set of another thread (@{term "a \<notin> dom (\<R>s!j)"}); reading from an address is only allowed if it is not released by another thread while it was unshared (@{term "(\<R>s!j) a \<noteq> Some False"}). 
 
 For the store buffer machine with history information we not only put writes into the store buffer but also record reads, program steps and ghost operations. 
 This allows us to restore the necessary computation history of the store buffer machine and relate it to the virtual machine which may fall behind the store buffer machine during execution. 
 Altogether an entry in the store buffer is either a
 \begin{itemize}
 \item @{term "Read\<^sub>s\<^sub>b volatile a t v"}, recording a corresponding read from address @{term "a"} which loaded the value @{term "v"} to temporary @{term "t"}, or a 
 \item @{term "Write\<^sub>s\<^sub>b volatile a sop v"} for an outstanding write, where operation @{term "sop"} evaluated to value @{term "v"}, or of the form
 
 \item @{term "Prog\<^sub>s\<^sub>b p p' is'"}, recording a program transition from @{term "p"} to @{term "p'"} which issued instructions @{term "is'"}, or of the form
 \item @{term "Ghost\<^sub>s\<^sub>b A L R W"}, recording a corresponding ghost operation.
 \end{itemize}
 As defined in Figure \ref{fig:store-buffer-transitions} a write updates the memory when it exits the store buffer, all other store buffer entries may only have an effect on the ghost state. The effect on the ownership information is analogous to the corresponding operations in the virtual machine.
 %
 \begin{figure}
 \begin{center}
 @{thm [mode=Axiom] Write\<^sub>s\<^sub>bNonVolatile [where rs=sb, no_vars]}\\[0.5\baselineskip]
 @{thm [mode=Rule, names_short] Write\<^sub>s\<^sub>bVolatile [where rs=sb,  no_vars]}\\[-0.3\baselineskip]
 @{thm [mode=Axiom] flush_step.Read\<^sub>s\<^sub>b [where rs=sb, no_vars]}\\[-0.3\baselineskip]
 @{thm [mode=Axiom] flush_step.Prog\<^sub>s\<^sub>b [where rs=sb, no_vars]}\\[0.5\baselineskip]
 @{thm [mode=Rule] Ghost\<^sub>s\<^sub>b [where rs=sb, no_vars]} 
 \end{center}
 \caption{Store buffer transitions with history\label{fig:store-buffer-transitions}}
 \end{figure}
 %
 The memory transitions defined in Figure \ref{fig:store-buffer-history-memory} are straightforward extensions 
 of the store buffer transitions of Figure \ref{fig:store-buffer-history-memory} augmented with ghost state 
 and recording history information in the store buffer. Note how we deal with the ghost state. 
 Only the dirty flag is updated when the instruction enters the store buffer, the ownership transfer 
 takes effect when the instruction leaves the store buffer.
 %
 \begin{figure}
 \begin{center}
 @{thm [mode=Rule] SBHRead [no_vars]}\\[0.5\baselineskip]
 @{thm [mode=Rule] SBHWriteNonVolatile' [no_vars]}\\[0.5\baselineskip]
 @{thm [mode=Rule] SBHWriteVolatile' [no_vars]}\\[0.5\baselineskip]
 @{thm [mode=Rule,names_short] SBHRMWReadOnly' [no_vars]}\\[0.5\baselineskip]
 @{thm [mode=Rule,names_short] SBHRMWWrite' [no_vars]}\\[-0.3\baselineskip]
 @{thm [mode=Axiom,names_short] sbh_memop_step.SBHFence [no_vars]}\\[-0.3\baselineskip]
 @{thm [mode=Axiom] SBHGhost' [no_vars]}
 \end{center}
 \caption{Memory transitions of store buffer machine with history\label{fig:store-buffer-history-memory}}
 \end{figure}
 %
 The global transitions @{term "(ts\<^sub>s\<^sub>b\<^sub>h, m, \<S>) \<Rightarrow>\<^sub>s\<^sub>b\<^sub>h (ts\<^sub>s\<^sub>b\<^sub>h',m',\<S>')"} are analogous to the rules in Figure \ref{fig:global-transitions} replacing the memory transtions and store buffer transtiontions accordingly.
 \<close>
 
 subsection \<open>Coupling relation \label{sec:couplingrelation}\<close>
 
 text (in program) \<open>
 After this introduction of the immediate models we can proceed to the details of the coupling relation, which relates configurations of the store buffer machine with histroy and the virtual machine with delayed releases.
 Remember the basic idea of the coupling relation: the state of the virtual machine is obtained from the state of the store buffer machine, by executing each store buffer until we reach the first volatile write. The remaining store buffer entries are suspended as instructions. The instructions now also include the history entries for reads, program steps and ghost operations.
 The suspended reads are not yet visible in the temporaries of the virtual machine. 
 Similar the ownership effects (and program steps) of the suspended operations are not yet visible in the virtual machine.
 The coupling relation between the store buffer machine and the virtual machine is illustrated in Figure~\ref{fig:coupling-relation-pic}. The threads issue instructions to the store buffers from the right and the instructions emerge from the store buffers to main memory from the left. The dotted line illustrates the state of the virtual machines memory. It is obtained from the memory of the store buffer machine by executing the purely non-volatile prefixes of the store buffers. The remaining entries of the store buffer are still (suspended) instructions in the virtual machine.
 
 \begin{figure}
 \centering
 \begin{tikzpicture}
 \tikzstyle{sbnodel}=[shape=rectangle, draw=black, text badly centered,  outer sep=0cm]
 \tikzstyle{sbnoder}=[shape=rectangle, draw=black, text ragged, outer sep=0cm]
 \tikzstyle{nonvolatile}=[fill=gray!10]
 \tikzstyle{virtual}=[dotted]
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % Store buffers and instructions %
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \node (sbl0) [style=sbnodel,style=nonvolatile,text width=1.3cm] {nv};
 \node (sbr0) [style=sbnoder,text width=1.7cm, right] at(sbl0.east) {v};
 \node (ins0) [right] at ($ (sbr0.east) $) {thread $0$: $i_0^0$, $i_0^1$, $\dots$};
 
 \node (sbl1) [style=sbnodel,style=nonvolatile,text width=2.0cm,below right] at ($ (sbl0.south west) -(0,0.6cm) $) {nv};
 \node (sbr1) [style=sbnoder,text width=1.0cm, right] at(sbl1.east) {v};
 \node (ins1) [right] at ($ (sbr1.east) $) {thread $i$: $i_i^0$, $i_i^1$, $\dots$};
 
 
 \node (sbl2) [style=sbnodel,style=nonvolatile,text width=1.7cm,below right] at ($ (sbl1.south west) -(0,0.6cm) $) {nv};
 \node (sbr2) [style=sbnoder,text width=1.3cm, right] at(sbl2.east) {v};
 \node (ins2) [right] at ($ (sbr2.east) $) {thread $j$: $i_j^0$, $i_j^1$, $\dots$};
 
 \node (sbl3) [style=sbnodel,style=nonvolatile,text width=1.4cm,below right] at ($ (sbl2.south west) -(0,0.6cm) $) {nv};
 \node (sbr3) [style=sbnoder,text width=1.6cm, right] at(sbl3.east) {v};
 \node (ins3) [right] at ($ (sbr3.east) $) {thread $n$: $i_n^0$, $i_n^1$, $\dots$};
 
 \path (sbr1.north east) to node [near end,left] {$\vdots$} (sbr0.south east);
 \path (sbr2.north east) to node [near end,left] {$\vdots$} (sbr1.south east);
 \path (sbr3.north east) to node [near end,left] {$\vdots$} (sbr2.south east);
 
 \node (sblabel)[above]  at ($ (sbr0.north west) +(0,0.6cm)$) {$\leftarrow$ store buffers};
 \node (inslabel)[above]  at ($ (sbr0.north east) +(1.5cm,0.6cm)$) {$\leftarrow$ instructions};
 
 %%%%%%%%%%
 % Memory %
 %%%%%%%%%%
 \coordinate (memNorthWest) at ($ (sbl0.north west) -(2.0cm,0cm) $);
 \coordinate (memSouthEast) at ($ (sbl3.south west) -(0.5cm,0cm) $);
 \filldraw[style=nonvolatile,rounded corners]  (memNorthWest) rectangle  (memSouthEast) node [midway] {@{term "m\<^sub>s\<^sub>b\<^sub>h"}};
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % Virtual memory boundaries %
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \draw [style=virtual,out=90,in=-90](sbr1.north west) to (sbr0.south west);
 \draw [style=virtual,out=90,in=-90](sbr2.north west) to (sbr1.south west);
 \draw [style=virtual,out=90,in=-90](sbr3.north west) to (sbr2.south west);
 
 \draw [style=virtual] ($ (memNorthWest) +(0,0.4cm) $) to ($ (sbr0.north west) + (-0.3,0.4)$)[out=0,in=90] to ($ (sbr0.north west)$);
 \draw [style=virtual]($ (memNorthWest |- memSouthEast) +(0,-0.8cm) $) to node[midway,above]{@{term m}} ($ (sbr3.south west) + (-0.3,-0.8)$)[out=0,in=90]
   to ($ (sbr3.south west)$);
 
 \node (execslabel)[below]  at ($ (sbl3.south)$) {executed};
 \node (suspendslabel)[below]  at ($ (sbr3.south)$) {suspended};
 
 \end{tikzpicture}
 
 \caption{Illustration of coupling relation \label{fig:coupling-relation-pic}}
 \end{figure}
 
 
 Consider the following configuration of a thread @{term "ts\<^sub>s\<^sub>b\<^sub>h ! j"} in the store buffer machine, where @{term "i\<^sub>k"} are the instructions and @{term "s\<^sub>k"} the store buffer entries. 
 Let @{term "s\<^sub>v"} be the first volatile write in the store buffer. 
 Keep in mind that new store buffer entries are appended to the end of the list and entries exit the store buffer and are issued to memory from the front of the list.
 %
 \begin{center} 
 @{term "ts\<^sub>s\<^sub>b\<^sub>h ! j = (p,[i\<^sub>1,\<dots>,i\<^sub>n], \<theta>, [s\<^sub>1,\<dots>,s\<^sub>v,s\<^sub>\<vv>,\<dots>,s\<^sub>m], \<D>, \<O>, \<R>)"}
 \end{center} 
 %
 The corresponding configuration @{term "ts ! j"} in the virtual machine is obtained by suspending all store buffer entries beginning at @{term "s\<^sub>v"} to the front of the instructions. 
 A store buffer @{term "Read\<^sub>s\<^sub>b"} / @{term "Write\<^sub>s\<^sub>b"} / @{term "Ghost\<^sub>s\<^sub>b"} is converted to a  @{term "Read"} / @{term "Write"} / @{term "Ghost"} instruction. 
 We take the freedom to make this coercion implicit in the example. 
 The store buffer entries preceding @{term "s\<^sub>v"} have already made their way to memory, whereas the suspended read operations are not yet visible in the temporaries @{term "\<theta>'"}. Similar, the suspended updates to the ownership sets and dirty flag are not yet recorded in @{term "\<O>'"}, @{term "\<R>'"} and @{term "\<D>'"}.
 %
 \begin{center} 
 @{term "ts ! j =(p,[s\<^sub>v,s\<^sub>\<vv>,\<dots>,s\<^sub>m,i\<^sub>1,\<dots>,i\<^sub>n], \<theta>', (), \<D>', \<O>',\<R>')"}
 \end{center} 
 %
 This example illustrates that the virtual machine falls behind the store buffer machine in our simulation, as store buffer instructions are suspended and reads (and ghost operations) are delayed and not yet visible in the temporaries (and the ghost state).
 This delay can also propagate to the level of the programming language, which communicates with the memory system by reading the temporaries and issuing new instructions. 
 For example the control flow can depend on the temporaries, which store the result of branching conditions. 
 It may happen that the store buffer machine already has evaluated the branching condition by referring to the values in the store buffer, whereas the virtual machine still has to wait. 
 Formally this manifests in still undefined temporaries. 
 Now consider that the program in the store buffer machine makes a step from @{term "p"} to @{term "(p',is')"}, which results in a thread configuration where the program state has switched to @{term "p'"}, the instructions @{term "is'"} are appended and the program step is recorded in the store buffer:
 %
 \begin{center} 
 @{term "ts\<^sub>s\<^sub>b\<^sub>h' ! j = (p',[i\<^sub>1,\<dots>,i\<^sub>n]@is', \<theta>, [s\<^sub>1,\<dots>,s\<^sub>v,\<dots>,s\<^sub>m,Prog\<^sub>s\<^sub>b p p' is'], \<D>, \<O>, \<R>)"}
 \end{center} 
 %
 The virtual machine however makes no step, since it still has to evaluate the suspended instructions before making the program step. 
 The instructions @{term "is'"} are not yet issued and the program state is still @{term "p"}. 
 We also take these program steps into account in our final coupling relation @{thm (concl) sim_config' [no_vars]}, defined in Figure~\ref{fig:coupling-relation}.
 %
 \begin{figure}
 \begin{center}
 \begin{minipage}{10cm}
 \inferrule{@{thm (prem 1) sim_config' [no_vars]}\\
            @{thm (prem 2) sim_config' [no_vars]}\\
            @{thm (prem 3) sim_config' [no_vars]}\\
            \parbox{9.8cm}{@{thm [break,mode=letnl,margin=80] (prem 4) sim_config' [simplified restrict_map_inverse, no_vars]}}}
 %
           {@{thm (concl) sim_config' [no_vars]}}
 \end{minipage}
 \end{center}
 \caption{Coupling relation \label{fig:coupling-relation}}
 \end{figure}
 % 
 We denote the already simulated store buffer entries by @{term "Bind execs. execs"} and the suspended ones by @{term "Bind suspends. suspends"}.
 The function @{term "instrs"} converts them back to instructions, which are a prefix of the instructions of the virtual machine. 
 We collect the additional instructions which were issued by program instructions but still recorded in the remainder of the store buffer with function @{term "prog_instrs"}. 
 These instructions have already made their way to the instructions of the store buffer machine but not yet on the virtual machine. 
 This situation is formalized as @{term "Bind suspends is\<^sub>s\<^sub>b\<^sub>h is. instrs suspends @ is\<^sub>s\<^sub>b\<^sub>h = is @ prog_instrs suspends"}, where @{term "Bind is. is"} are the instructions of the virtual machine. 
 The program state of the virtual machine is either the same as in the store buffer machine or the first program state recorded in the suspended part of the store buffer.
 This state is selected by @{const "hd_prog"}. 
 The temporaries of the virtual machine are obtained by removing the suspended reads from @{term "\<theta>"}. 
 The memory is obtained by executing all store buffers until the first volatile write is hit, excluding it. Thereby only non-volatile writes are executed, which are all thread local, and hence could be executed in any order with the same result on the memory. Function @{const "flush_all_until_volatile_write"} executes them in order of appearance.
 Similarly the sharing map of the virtual machine is obtained by executing all store buffers until the first volatile write via the function @{const "share_all_until_volatile_write"}. For the local ownership set @{term "\<O>\<^sub>s\<^sub>b\<^sub>h"} the auxiliary function @{term "acquire"} calculates the outstanding effect of the already simulated parts of the store buffer. Analogously @{term "release"} calculates the effect for the released addresses @{term "\<R>\<^sub>s\<^sub>b\<^sub>h"}.
 
 
 \<close>
 
 subsection \<open>Simulation \label{sec:simulation}\<close>
 
 text (in xvalid_program_progress) \<open>
 Theorem \ref{thm:simulation} is our core inductive simulation theorem. 
 Provided that all reachable states of the virtual machine (with delayed releases) are safe, a step of the store buffer machine (with history) can be simulated by a (potentially empty) sequence of steps on the virtual machine, maintaining the coupling relation and an invariant on the configurations of the store buffer machine.
 %
 \begin{theorem}[Simulation]\label{thm:simulation}
 @{thm [display,  mode=holimplnl,margin=100]  simulation_hol [no_vars]}
 \end{theorem}
 %
 In the following we discuss the invariant @{term [names_short] "invariant ts\<^sub>s\<^sub>b\<^sub>h S\<^sub>s\<^sub>b\<^sub>h m\<^sub>s\<^sub>b\<^sub>h"}, where we commonly refer to a thread configuration @{term "ts\<^sub>s\<^sub>b\<^sub>h!i = (p,is,\<theta>,sb,\<D>,\<O>,\<R>)"} for @{term "i < length ts\<^sub>s\<^sub>b\<^sub>h"}. 
 By outstanding references we refer to read and write operations in the store buffer. 
 The invariant is a conjunction of several sub-invariants grouped by their content:
 
 @{thm [display, names_short, mode=compact, margin=100] invariant_grouped_def [of ts\<^sub>s\<^sub>b\<^sub>h S\<^sub>s\<^sub>b\<^sub>h m\<^sub>s\<^sub>b\<^sub>h]}
 %TODO make grouping formally, hide program step in valid_history
 
 \paragraph{Ownership.} 
 \begin{inparaenum}
 \item \label{inv-ownership:owned-or-read-only} For every thread all outstanding non-volatile references have to be owned or refer to read-only memory.
 \item Every outstanding volatile write is not owned by any other thread. 
 \item Outstanding accesses to read-only memory are not owned.
 \item \label{inv-ownership:distinct-ownership} The ownership sets of every two different threads are distinct.
 \end{inparaenum}
 
 \paragraph{Sharing.}
 \begin{inparaenum}
 \item \label{inv-sharing:non-volatile-writes-unshared} All outstanding non volatile writes are unshared. 
 \item All unowned addresses are shared.
 \item No thread owns read-only memory.
 \item The ownership annotations of outstanding ghost and write operations are consistent (\eg released addresses are owned at the point of release).
 \item \label{inv-sharing:no-write-to-read-only-memory} There is no outstanding write to read-only memory.
 \end{inparaenum}
 
 \paragraph{Temporaries.} Temporaries are modeled as an unlimited store for temporary registers. We require certain distinctness and freshness properties for each thread.
 \begin{inparaenum}
 \item The temporaries referred to by read instructions are distinct.
 \item The temporaries referred to by reads in the store buffer are distinct.
 \item Read and write temporaries are distinct.
 \item Read temporaries are fresh, \ie are not in the domain of @{term "\<theta>"}.
 \end{inparaenum}
 
 \paragraph{Data dependency.} Data dependency means that store operations may only depend on \emph{previous} read operations. For every thread we have:
 \begin{inparaenum}
 \item Every operation @{term "(D, f)"} in a write instruction or a store buffer write is valid according to @{term "valid_sop (D, f)"}, \ie function @{term "f"} only depends on domain @{term "D"}.
 \item For every suffix of the instructions of the form @{term "Write volatile a (D,f) A L R W#is"} the domain @{term "D"} is distinct from the temporaries referred to by future read instructions in @{term "is"}.
 \item The outstanding writes in the store buffer do not depend on the read temporaries still in the instruction list.
 \end{inparaenum}
 
 \paragraph{History.} The history information  of program steps and  read operations we record in the store buffer have to be consistent with the trace. For every thread:
 \begin{inparaenum}
 \item The value stored for a non volatile read is the same as the last write to the same address in the store buffer or the value in memory, in case there is no write in the buffer. 
 \item All reads have to be clean. This results from our flushing policy. Note that the value recorded for a volatile read in the initial part of the store buffer (before the first volatile write), may become stale with respect to the memory. Remember that those parts of the store buffer are already executed in the virtual machine and thus cause no trouble.
 \item For every read the recorded value coincides with the corresponding value in the temporaries.
 \item For every @{term "Write\<^sub>s\<^sub>b volatile a (D,f) v A L R W"} the recorded value @{term "v"} coincides with @{term "f \<theta>"}, and domain @{term "D"} is subset of @{term "dom \<theta>"} and is distinct from the following read temporaries. Note that the consistency of the ownership annotations is already covered by the aforementioned invariants.
 \item For every suffix in the store buffer of the form @{term "Prog\<^sub>s\<^sub>b p\<^sub>1 p\<^sub>2 is'#sb'"}, either @{term "p\<^sub>1 = p"} in case there is no preceding program node in the buffer or it corresponds to the last program state recorded there. 
 Moreover, the program transition @{term "\<theta>|`(- read_tmps sb')\<turnstile> p\<^sub>1 \<rightarrow>\<^sub>p (p\<^sub>2,is')"} is possible, \ie it was possible to execute the program transition at that point.
 \item The program configuration @{term "p"} coincides with the last program configuration recorded in the store buffer.
 \item As the instructions from a program step are at the one hand appended to the instruction list and on the other hand recorded in the store buffer, we have for every suffix @{term "sb'"} of the store buffer: @{term "\<exists>is'. instrs sb' @ is = is' @ prog_instrs sb'"}, \ie the remaining instructions @{term "is"} correspond to a suffix of the recorded instructions @{term "prog_instrs sb'"}.
 \end{inparaenum}
 
 \paragraph{Flushes.} If the dirty flag is unset there are no outstanding volatile writes in the store buffer.
 
 \paragraph{Program step.} The program-transitions are still a parameter of our model. 
 In order to make the proof work, we have to assume some of the invariants also for the program steps. 
 We allow the program-transitions to employ further invariants on the configurations, these are modeled by the parameter @{term "valid"}. 
 For example, in the instantiation later on the program keeps a counter for the temporaries, for each thread. 
 We maintain distinctness of temporaries by restricting all temporaries occurring in the memory system to be below that counter, which is expressed by instantiating @{term "valid"}. 
 Program steps, memory steps and store buffer steps have to maintain @{term "valid"}. 
 Furthermore we assume the following properties of a program step:
 \begin{inparaenum}
 \item The program step generates fresh, distinct read temporaries, that are neither in @{term "\<theta>"} nor in the store buffer temporaries of the memory system.
 \item The generated memory instructions respect data dependencies, and are valid according to @{term "valid_sop"}.
 
 %TODO: maybe we can omit the formal stuff, intuition should be clear, depends on what we write on PIMP.
 \end{inparaenum}
 
 \paragraph{Proof sketch.} We do not go into details but rather first sketch the main arguments for simulation of a step in the store buffer machine by a potentially empty sequence of steps in the virtual machine, maintaining the coupling relation. Second we exemplarically focus on some cases to illustrate common arguments in the proof.
 The first case distinction in the proof is on the global transitions in Figure~\ref{fig:global-transitions}. 
 %
 \begin{inparaenum}
 \item \emph{Program step}: 
 we make a case distinction whether there is an outstanding volatile write in the store buffer or not. 
 If not the configuration of the virtual machine corresponds to the executed store buffer and we can make the same step. 
 Otherwise the virtual machine makes no step as we have to wait until all volatile writes have exited the store buffer.
 %
 \item \emph{Memory step}: 
 we do case distinction on the rules in Figure~\ref{fig:store-buffer-history-memory}. 
 For read, non volatile write and ghost instructions we do the same case distinction as for the program step. 
 If there is no outstanding volatile write in the store buffer we can make the step, otherwise we have to wait. 
 When a volatile write enters the store buffer it is suspended until it exists the store buffer. Hence we do no step in the virtual machine.
 The read-modify-write and the fence instruction can all be simulated immediately since the store buffer has to be empty.
 %
 \item \emph{Store Buffer step}:
 we do case distinction on the rules in Figure~\ref{fig:store-buffer-transitions}. 
 When a read, a non volatile write, a ghost operation or a program history node exits the store buffer, the virtual machine does not have to do any step since these steps are already visible. 
 When a volatile write exits the store buffer, we execute all the suspended operations (including reads, ghost operations and program steps) until the next suspended volatile write is hit. This is possible since all writes are non volatile and thus memory modifications are thread local. 
 \end{inparaenum}
 
 In the following we exemplarically describe some cases in more detail to give an impression on the typical arguments in the proof.
 We start with a configuration @{term "c\<^sub>s\<^sub>b\<^sub>h=(ts\<^sub>s\<^sub>b\<^sub>h,m\<^sub>s\<^sub>b\<^sub>h,\<S>\<^sub>s\<^sub>b\<^sub>h)"} of the store buffer machine, where the next instruction to be executed is a 
 read of thread @{term i}: @{term "Read\<^sub>s\<^sub>b volatile a t"}. The configuration of the virtual machine is @{term "cfg=(ts,m,\<S>)"}. 
 We have to simulate this step on the virtual machine and can make use of 
 the coupling relations @{term "(ts\<^sub>s\<^sub>b\<^sub>h,m\<^sub>s\<^sub>b\<^sub>h,\<S>\<^sub>s\<^sub>b\<^sub>h) \<sim> (ts,m,\<S>)"},  the invariants  @{term "invariant ts\<^sub>s\<^sub>b\<^sub>h \<S>\<^sub>s\<^sub>b\<^sub>h m\<^sub>s\<^sub>b\<^sub>h"} and the safety of all reachable states of the virtual machine: @{term "safe_reach_direct_delayed (ts,m,\<S>)"}. The state of the store buffer machine and the coupling with the volatile machine is depicted in Figure~\ref{fig:coupling-i-read}. Note that if there are some suspended instructions in thread @{term i}, we cannot directly exploit the 'safety of the read', as the virtual machine has not yet reached the state where thread @{term i} is poised to do the read. But fortunately we have safety of the virtual machien of all reachable states. Hence we can just  execute all suspended instructions of thread @{term i} until we reach the read. We refer to this configuration of the virtual machine as @{term "cfg''=(ts'',m'',\<S>'')"}, which is depicted in Figure~\ref{fig:coupling-i-read-forward}.
 
 \begin{figure}
 \centering
 \begin{tikzpicture}
 \tikzstyle{sbnodel}=[shape=rectangle, draw=black, text badly centered,  outer sep=0cm]
 \tikzstyle{sbnoder}=[shape=rectangle, draw=black, text ragged, outer sep=0cm]
 \tikzstyle{nonvolatile}=[fill=gray!10]
 \tikzstyle{virtual}=[dotted]
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % Store buffers and instructions %
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \node (sbl0) [style=sbnodel,style=nonvolatile,text width=1.3cm] {nv};
 \node (sbr0) [style=sbnoder,text width=1.7cm, right] at(sbl0.east) {v};
 \node (ins0) [right] at ($ (sbr0.east) $) {thread $0$: $i_0^0$, $i_0^1$, $\dots$};
 
 \node (sbl1) [style=sbnodel,style=nonvolatile,text width=2.0cm,below right] at ($ (sbl0.south west) -(0,0.6cm) $) {nv};
 \node (sbr1) [style=sbnoder,text width=1.0cm, right] at(sbl1.east) {v};
 \node (ins1) [right] at ($ (sbr1.east) $) {thread $i$: @{term "Read\<^sub>s\<^sub>b volatile a t"},$\dots$};
 
 
 \node (sbl2) [style=sbnodel,style=nonvolatile,text width=1.7cm,below right] at ($ (sbl1.south west) -(0,0.6cm) $) {nv};
 \node (sbr2) [style=sbnoder,text width=1.3cm, right] at(sbl2.east) {v};
 \node (ins2) [right] at ($ (sbr2.east) $) {thread $j$: $i_j^0$, $i_j^1$, $\dots$};
 
 \node (sbl3) [style=sbnodel,style=nonvolatile,text width=1.4cm,below right] at ($ (sbl2.south west) -(0,0.6cm) $) {nv};
 \node (sbr3) [style=sbnoder,text width=1.6cm, right] at(sbl3.east) {v};
 \node (ins3) [right] at ($ (sbr3.east) $) {thread $n$: $i_n^0$, $i_n^1$, $\dots$};
 
 \path (sbr1.north east)  to node [near end,left] {$\vdots$} (sbr0.south east);
 \path (sbr2.north east)  to node [near end,left] {$\vdots$} (sbr1.south east);
 \path (sbr3.north east)  to node [near end,left] {$\vdots$} (sbr2.south east);
 
 \node (sblabel)[above]  at ($ (sbr0.north west) +(0,0.6cm)$) {$\leftarrow$ store buffers};
 \node (inslabel)[above]  at ($ (sbr0.north east) +(1.5cm,0.6cm)$) {$\leftarrow$ instructions};
 
 %%%%%%%%%%
 % Memory %
 %%%%%%%%%%
 \coordinate (memNorthWest) at ($ (sbl0.north west) -(2.0cm,0cm) $);
 \coordinate (memSouthEast) at ($ (sbl3.south west) -(0.5cm,0cm) $);
 \filldraw[style=nonvolatile,rounded corners]  (memNorthWest) rectangle  (memSouthEast) node [midway] {@{term "m\<^sub>s\<^sub>b\<^sub>h"}};
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % Virtual memory boundaries %
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \draw [style=virtual,out=90,in=-90](sbr1.north west) to (sbr0.south west);
 \draw [style=virtual,out=90,in=-90](sbr2.north west) to (sbr1.south west);
 \draw [style=virtual,out=90,in=-90](sbr3.north west) to (sbr2.south west);
 
 \draw [style=virtual] ($ (memNorthWest) +(0,0.4cm) $) to ($ (sbr0.north west) + (-0.3,0.4)$)[out=0,in=90] to ($ (sbr0.north west)$);
 \draw [style=virtual]($ (memNorthWest |- memSouthEast) +(0,-0.8cm) $) to node[midway,above]{@{term m}} ($ (sbr3.south west) + (-0.3,-0.8)$)[out=0,in=90]
   to ($ (sbr3.south west)$);
 
 \node (execslabel)[below]  at ($ (sbl3.south)$) {executed};
 \node (suspendslabel)[below]  at ($ (sbr3.south)$) {suspended};
 
 \end{tikzpicture}
 
 \caption{Thread @{term i} poised to read \label{fig:coupling-i-read}}
 \end{figure}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \begin{figure}
 \centering
 \begin{tikzpicture}
 \tikzstyle{sbnodel}=[shape=rectangle, draw=black, text badly centered,  outer sep=0cm]
 \tikzstyle{sbnoder}=[shape=rectangle, draw=black, text ragged, outer sep=0cm]
 \tikzstyle{nonvolatile}=[fill=gray!10]%todo rename to executed?
 \tikzstyle{virtual}=[dotted]
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % Store buffers and instructions %
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \node (sbl0) [style=sbnodel,style=nonvolatile,text width=1.3cm] {nv};
 \node (sbr0) [style=sbnoder,text width=1.7cm, right] at(sbl0.east) {v};
 \node (ins0) [right] at ($ (sbr0.east) $) {thread $0$: $i_0^0$, $i_0^1$, $\dots$};
 
 \node (sbl1) [style=sbnodel,style=nonvolatile,text width=2.0cm,below right] at ($ (sbl0.south west) -(0,0.6cm) $) {nv};
 \node (sbr1) [style=sbnoder,style=nonvolatile,text width=1.0cm, right] at(sbl1.east) {v};
 \node (ins1) [right] at ($ (sbr1.east) $) {thread $i$: @{term "Read\<^sub>s\<^sub>b volatile a t"},$\dots$};
 
 
 \node (sbl2) [style=sbnodel,style=nonvolatile,text width=1.7cm,below right] at ($ (sbl1.south west) -(0,0.6cm) $) {nv};
 \node (sbr2) [style=sbnoder,text width=1.3cm, right] at(sbl2.east) {v};
 \node (ins2) [right] at ($ (sbr2.east) $) {thread $j$: $i_j^0$, $i_j^1$, $\dots$};
 
 \node (sbl3) [style=sbnodel,style=nonvolatile,text width=1.4cm,below right] at ($ (sbl2.south west) -(0,0.6cm) $) {nv};
 \node (sbr3) [style=sbnoder,text width=1.6cm, right] at(sbl3.east) {v};
 \node (ins3) [right] at ($ (sbr3.east) $) {thread $n$: $i_n^0$, $i_n^1$, $\dots$};
 
 \path (sbr1.north east)  to node [near end,left] {$\vdots$} (sbr0.south east);
 \path (sbr2.north east)  to node [near end,left] {$\vdots$} (sbr1.south east);
 \path (sbr3.north east)  to node [near end,left] {$\vdots$} (sbr2.south east);
 
 \node (sblabel)[above]  at ($ (sbr0.north west) +(0,0.6cm)$) {$\leftarrow$ store buffers};
 \node (inslabel)[above]  at ($ (sbr0.north east) +(1.5cm,0.6cm)$) {$\leftarrow$ instructions};
 
 %%%%%%%%%%
 % Memory %
 %%%%%%%%%%
 \coordinate (memNorthWest) at ($ (sbl0.north west) -(2.0cm,0cm) $);
 \coordinate (memSouthEast) at ($ (sbl3.south west) -(0.5cm,0cm) $);
 \filldraw[style=nonvolatile,rounded corners]  (memNorthWest) rectangle  (memSouthEast) node [midway] {@{term "m\<^sub>s\<^sub>b\<^sub>h"}};
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % Virtual memory boundaries %
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \draw [style=virtual,out=90,in=-90](sbr1.north east) to (sbr0.south west);
 \draw [style=virtual,out=90,in=-90](sbr2.north west) to (sbr1.south east);
 \draw [style=virtual,out=90,in=-90](sbr3.north west) to (sbr2.south west);
 
 \draw [style=virtual] ($ (memNorthWest) +(0,0.4cm) $) to ($ (sbr0.north west) + (-0.3,0.4)$)[out=0,in=90] to ($ (sbr0.north west)$);
 \draw [style=virtual]($ (memNorthWest |- memSouthEast) +(0,-0.8cm) $) to node[midway,above]{@{term m}} ($ (sbr3.south west) + (-0.3,-0.8)$)[out=0,in=90]
   to ($ (sbr3.south west)$);
 
 \node (execslabel)[below]  at ($ (sbl3.south)$) {executed};
 \node (suspendslabel)[below]  at ($ (sbr3.south)$) {suspended};
 
 \end{tikzpicture}
 
 \caption{Forwarded computation of virtual machine  \label{fig:coupling-i-read-forward}}
 \end{figure}
 
 
 
 For now we want to consider the case where the read goes to memory and is not forwarded from the store buffer. The value read is @{term "v=m\<^sub>s\<^sub>b\<^sub>h a"}. Moreover, we make a case distinction wheter there is an outstanding volatile write in the store buffer of thread @{term i} or not. This determines if there are suspended instructions in the virtual machine or not. We start with the case where there is no such write. This means that there are no suspended instructions in thread @{term i} and therefore @{term "cfg''=cfg"}. 
 We have to show that the virtual machine reads the same value from memory: @{term "v = m a"}. So what can go wrong? When can the the memory of the virtual machine hold a different value? The memory of the virtual machine is obtained from the memory of the store buffer machine by executing all store buffers until we hit the first volatile write. So if there is a discrepancy in the value this has to come from a non-volatile write in the executed parts of another thread, let us say thread @{term j}. This write is marked as x in Figure~\ref{fig:coupling-i-read-conflict}.
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \begin{figure}
 \centering
 \begin{tikzpicture}
 \tikzstyle{sbnodel}=[shape=rectangle, draw=black, text badly centered,  outer sep=0cm]
 \tikzstyle{sbnoder}=[shape=rectangle, draw=black, text ragged, outer sep=0cm]
 \tikzstyle{nonvolatile}=[fill=gray!10]%todo rename to executed?
 \tikzstyle{virtual}=[dotted]
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % Store buffers and instructions %
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \node (sbl0) [style=sbnodel,style=nonvolatile,text width=1.3cm] {nv};
 \node (sbr0) [style=sbnoder,text width=1.7cm, right] at(sbl0.east) {v};
 \node (ins0) [right] at ($ (sbr0.east) $) {thread $0$: $i_0^0$, $i_0^1$, $\dots$};
 
 \node (sbl1) [style=sbnodel,style=nonvolatile,text width=2.0cm,below right] at ($ (sbl0.south west) -(0,0.6cm) $) {nv};
 \node (sbr1) [style=sbnoder,style=nonvolatile,text width=1.0cm, right] at(sbl1.east) {v};
 \node (ins1) [right] at ($ (sbr1.east) $) {thread $i$: @{term "Read\<^sub>s\<^sub>b volatile a t"},$\dots$};
 
 
 \node (sbl2) [style=sbnodel,style=nonvolatile,text width=1.7cm,below right] at ($ (sbl1.south west) -(0,0.6cm) $) {x};
 \node (sbr2) [style=sbnoder,text width=1.3cm, right] at(sbl2.east) {v};
 \node (ins2) [right] at ($ (sbr2.east) $) {thread $j$: $i_j^0$, $i_j^1$, $\dots$};
 
 \node (sbl3) [style=sbnodel,style=nonvolatile,text width=1.4cm,below right] at ($ (sbl2.south west) -(0,0.6cm) $) {nv};
 \node (sbr3) [style=sbnoder,text width=1.6cm, right] at(sbl3.east) {v};
 \node (ins3) [right] at ($ (sbr3.east) $) {thread $n$: $i_n^0$, $i_n^1$, $\dots$};
 
 \path (sbr1.north east)  to node [near end,left] {$\vdots$} (sbr0.south east);
 \path (sbr2.north east)  to node [near end,left] {$\vdots$} (sbr1.south east);
 \path (sbr3.north east)  to node [near end,left] {$\vdots$} (sbr2.south east);
 
 \node (sblabel)[above]  at ($ (sbr0.north west) +(0,0.6cm)$) {$\leftarrow$ store buffers};
 \node (inslabel)[above]  at ($ (sbr0.north east) +(1.5cm,0.6cm)$) {$\leftarrow$ instructions};
 
 %%%%%%%%%%
 % Memory %
 %%%%%%%%%%
 \coordinate (memNorthWest) at ($ (sbl0.north west) -(2.0cm,0cm) $);
 \coordinate (memSouthEast) at ($ (sbl3.south west) -(0.5cm,0cm) $);
 \filldraw[style=nonvolatile,rounded corners]  (memNorthWest) rectangle  (memSouthEast) node [midway] {@{term "m\<^sub>s\<^sub>b\<^sub>h"}};
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % Virtual memory boundaries %
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \draw [style=virtual,out=90,in=-90](sbr1.north east) to (sbr0.south west);
 \draw [style=virtual,out=90,in=-90](sbr2.north west) to (sbr1.south east);
 \draw [style=virtual,out=90,in=-90](sbr3.north west) to (sbr2.south west);
 
 \draw [style=virtual] ($ (memNorthWest) +(0,0.4cm) $) to ($ (sbr0.north west) + (-0.3,0.4)$)[out=0,in=90] to ($ (sbr0.north west)$);
 \draw [style=virtual]($ (memNorthWest |- memSouthEast) +(0,-0.8cm) $) to node[midway,above]{@{term m}} ($ (sbr3.south west) + (-0.3,-0.8)$)[out=0,in=90]
   to ($ (sbr3.south west)$);
 
 \node (execslabel)[below]  at ($ (sbl3.south)$) {executed};
 \node (suspendslabel)[below]  at ($ (sbr3.south)$) {suspended};
 
 \end{tikzpicture}
 
 \caption{Conflicting write in thread j (marked x)  \label{fig:coupling-i-read-conflict}}
 \end{figure}
 
 We refer to x both for the write operation itself and to characterize the point in time in the computation of the virtual machine where the write was executed. At the point x the write was safe according to rules in Figure~\ref{fig:safe-delayed} for non-volatile writes. So it was owned by thread @{term j} and unshared. This knowledge about the safety of write x is preserved in the invariants, namely (Ownership.\ref{inv-ownership:owned-or-read-only})
 and (Sharing.\ref{inv-sharing:non-volatile-writes-unshared}). Additionally from invariant (Sharing.\ref{inv-sharing:no-write-to-read-only-memory}) we know that address @{term a} was not read-only at point x. Now we combine this information with the safety of the read of thread @{term i} in the current configuration @{term "cfg"}: address @{term a} either has to be owned by thread @{term i}, or has to be read-only or the read is volatile and @{term a} is shared. Additionally there are the constraints on the released addresses which we will exploit below. Let us address all cases step by step.
 First, we consider that address @{term a} is currently owned by thread @{term i}. As it was owned by thread @{term j} at time x there has to be an release of @{term a} in the executed prefix of the store buffer of thread @{term j}. This release is recorded in the release set, 
 so we know @{term "a \<in> dom (\<R>s!j)"}. This contradicts the safety of the read. Second, we consider that address @{term a} is currently read-only.
 At time x address @{term a} was owned by thread @{term j}, unshared and not read-only. Hence there was a release of address @{term a} in the executed prefix of the store buffer of @{term j}, where it made a transition unshared and owned to shared. With the monotonicity of the release sets this means 
 @{term "a \<in> dom (\<R>s!j)"}, even more precisely @{term "(\<R>s!j) a = Some False"}. Hence there is no chance to get the read safe (neiter a volatile nor a non-volatile). Third, consider a volatile read and that address @{term a} is currently shared. This is ruled out by the same line of reasoning as in the previous case.
 So ultimately we have ruled out all races that could destroy the value at address @{term a} and have shown that we can simulate the step on the virtual machine.
 This completes the simulation of the case where there is no store buffer forwarding and no volatile write in the store buffer of thread @{term i}. The other cases are handled similar. The main arguments are obtained by arguing about safety of configuration @{term cfg''} and exploiting the invariants to rule out conflicting operations in other store buffers. When there is a volatile write in he store buffer of thread @{term i} there are still pending suspended instructions in the virtual machine. Hence the virtual machine makes no step and we have to argue that the simulation relation as well as all invariants still hold.
 
 Up to now we have focused on how to simulate the read and in particular on how to argue that the value read in the store buffer machine is the same as the value read in the virtual machine. Besided these simulation properties another major part of the proof is to show that all invariants are maintained. For example if the non-volatile read enters the store buffer we have to argue that this new entry is either owned or refers to an read-only address (Ownership.\ref{inv-ownership:owned-or-read-only}). As for the simulation above this follows from safety of the virtual machine in configuration @{term "cfg''"}. However, consider an ghost operation that acquires an address @{term a}. From safety of the configuration @{term "cfg''"} we can only infer that there is no conflicting acquire in the non-volaitle prefixes of the other store buffers. In case an conflicting acquire is in the suspended part of a store buffer of thread @{term j} safety of configuration @{term "cfg''"} is not enough. But as we have safety of all reachable states we can forward the computation of thread @{term j} until the conflicting acquire is about to be executed and construct an unsafe state which rules out the conflict.
 
 Last we want to comment on the case where the store buffer takes a step. The major case destinction is wheter a volatile write leaves the store buffer or not. In the former case the virtual machine has to simulate a whole bunch of instructions at once to simulate the store buffer machine up to the next volatile write in the store buffer. In the latter case the virtual machine does no step at all, since the instruction leaving the store buffer is already simulated. In both cases one key argument is commutativity of non-volatile operations with respect to global effects on the memory or the sharing map. Consider a non-volatile store buffer step of thread @{term i}. In the configuration of the virtual machine before the store buffer step of thread @{term i}, the simulation relation applies the update to the memory and the sharing map of the store buffer machine, within the operations @{term "flush_all_until_volatile_write"} and @{term "share_all_until_volatile_write"} `somewhere in the middle' to obtain the memory and the sharing map of the virtual machine. After the store buffer step however, when the non-volatile operations has left the store buffer, the effect is applied to the memory and the sharing map right in the beginning. The invariants and safety sideconditions for non-volatile operations guarantee `locality' of the operation which manifests in commutativity properties. For example, a non-volatile write is thread local. There is no conflicting write in any other store buffer and hence the write can be safely moved to the beginning.
 
 This conludes the discussion on the proof of Theorem~\ref{thm:simulation}.\qed
 \<close>
 
 text (in xvalid_program_progress) \<open>
 \bigskip
 The simulation theorem for a single step is inductive and can therefor be extended to arbitrary long computations.
 Moreover, the coupling relation as well as the invariants become trivial for a initial configuration where all store buffers are empty and the ghost state is setup appropriately. To arrive at our final Theorem \ref{thm:reduction} we need the following steps:
 \begin{enumerate}
 \item \label{sim:sb-sbh} simulate the computation of the store buffer machine @{term "(ts\<^sub>s\<^sub>b,m,()) \<Rightarrow>\<^sub>s\<^sub>b\<^sup>* (ts\<^sub>s\<^sub>b',m',())"} by a computation of a store buffer machine with history @{term "(ts\<^sub>s\<^sub>b\<^sub>h,m,\<S>) \<Rightarrow>\<^sub>s\<^sub>b\<^sub>h\<^sup>* (ts\<^sub>s\<^sub>b\<^sub>h',m',\<S>')"},
 
 \item \label{sim:sbh-delayed} simulate the computation of the store buffer machine with history by a computation of the virtual machine 
  with delayed releases @{term "(ts,m,\<S>) \<Rightarrow>\<^sub>d\<^sup>* (ts',m',\<S>')"} by Theorem \ref{thm:simulation} (extended to the reflexive transitive closure),
 \item \label{sim:delayed-free-flowing} simulate the computation of the virtual machine with delayed releases by a computation of the virtual machine with free flowing releases @{term "(ts,m,\<S>) \<Rightarrow>\<^sub>v\<^sup>* (ts',m',\<S>')"}\footnote{Here we are sloppy with @{term ts}; strictly we would have to distinguish the thread configurations without the @{term \<R>} component form the ones with the @{term \<R>} component used for delayed releases}.
 \end{enumerate} 
 
 Step \ref{sim:sb-sbh} is trivial since the bookkeeping within the additional ghost and history state does not affect the control flow of the transition systems and can be easily removed. Similar the additional @{term \<R>} ghost component can be ignored in Step \ref{sim:delayed-free-flowing}. However, to apply Theorem \ref{thm:simulation} in Step \ref{sim:sbh-delayed} we have to convert from @{term [names_short] "safe_reach_virtual_free_flowing (ts, m, \<S>)"} provided by the preconditions of Theorem \ref{thm:reduction} to the required @{term [names_short] "safe_reach_direct_delayed (ts, m, \<S>)"}. This argument is more involved and we only give a short sketch here. 
-The other direction is trival as every single case for delayed releases (cf. Figure \ref{fig:safe-delayed}) immediately implies the corresponding case for free flowing releases (cf. Figure \ref{fig:safe-virtual-memory}).
+The other direction is trivial as every single case for delayed releases (cf. Figure \ref{fig:safe-delayed}) immediately implies the corresponding case for free flowing releases (cf. Figure \ref{fig:safe-virtual-memory}).
 
 First keep in mind that the predicates ensure that \emph{all} reachable configurations starting from @{term "(ts,m,\<S>)"} are safe, according to the rules for free flowing releases or delayed releases respectively. We show the theorem by contraposition and start with a computation which reaches a configuration @{term c} that is unsafe according to the rules for delayed releases and want to show that there has to be a (potentially other) computation (starting from the same initial state) that leads to an unsafe configuration @{term c'} accroding to free flowing releases. 
 If @{term c} is already unsafe according to free flowing releases we have @{term "c'=c"} and are finished. 
 Otherwise we have to find another unsafe configuration. 
 Via induction on the length of the global computation we can also assume that for all shorter computations both safety notions coincide. 
 A configuration can only be unsafe with respect to delayed releases and safe with respect to free flowing releases if there is a race between two distinct Threads @{term i} and @{term j} on an address @{term a} that is in the release set @{term "\<R>"} of one of the threads, lets say Thread @{term i}. 
 For example Thread @{term j} attempts to write to an address @{term a} which is in the release set of Thread @{term i}. 
 If the release map would be empty there cannot be such an race (it would simulataneously be unsafe with respect to free flowing releases). 
 Now we aim to find a configuration @{term c'} that is also reachable from the initial configuration and is unsafe with respect to free flowing releases. 
 Intuitively this is a configuration where Thread @{term i} is rewinded to the state just before the release of address @{term a} and Thread @{term j} is in the same state as in configuration @{term c}. 
 Before the release of @{term a} the address has to be owned by Thread @{term i}, which is unsafe according to free flowing releases as well as delayed releases.
 So we can argue that either Thread @{term j} can reach the same state although Thread @{term i} is rewinded or we even hit an unsafe configuration before. 
 What kind of steps can Thread @{term i} perform between between the free flowing release point (point of the ghost instruction) and the delayed release point (point of next volatile write, interlocked operation or fence at which the release map is emptied)? How can these actions affect Thread @{term j}? 
 Note that the delayed release point is not yet reached as this would empty the release map (which we know not to be empty). 
 Thus Thread @{term i} does only perform reads, ghost instructions, program steps or non-volatile writes.
 All of these instructions of Thread @{term i} either have no influence on the computation of Thread @{term j} at all (e.g. a read, program step, non-volatile write or irrelevant ghost operation) or may cause a safety violation already in a shorter computation (e.g. acquiring an address that another thread holds). This is fine for our inductive argument. So either we can replay every step of Thread @{term j} and reach 
 the final configuration @{term c'} which is now also unsafe according to free flowing releases, or we hit a configuration @{term c''} in a shorter computation which violates the rules of delayed as well as free flowing releases (using the induction hypothesis).
 \<close>
 
 section \<open>PIMP \label{sec:pimp}\<close>
 text \<open>
 PIMP is a parallel version of IMP\cite{Nipkow-FSTTCS-96}, a canonical WHILE-language. 
 
 
 An expression @{term "e"} is either 
 \begin{inparaenum}
 \item @{term "Const v"}, a constant value,
 \item @{term "Mem volatile a"}, a (volatile) memory lookup at address @{term "a"},
 \item @{term "Tmp sop"}, reading from the temporaries with a operation @{term "sop"} which is an intermediate expression occurring in the transition rules for statements,
 \item @{term "Unop f e"}, a unary operation where @{term "f"} is a unary function on values, and finally
 \item @{term "Binop f e\<^sub>1 e\<^sub>2"}, a binary operation where @{term "f"} is a binary function on values.
 \end{inparaenum}
 
  
 A statement @{term "s"} is either
 \begin{inparaenum}
 \item @{term "Skip"}, the empty statement,
 \item @{term "Assign volatile a e A L R W"}, a (volatile) assignment of expression @{term "e"} to address expression @{term "a"},
 \item @{term "CAS a c\<^sub>e s\<^sub>e A L R W"}, atomic compare and swap at address expression @{term "a"} with compare expression 
   @{term "c\<^sub>e"} and swap expression @{term "s\<^sub>e"},
 \item @{term "Seq s\<^sub>1 s\<^sub>2"}, sequential composition,
 \item @{term "Cond e s\<^sub>1 s\<^sub>2"}, the if-then-else statement,
 \item @{term "While e s"}, the loop statement with condition @{term "e"},
 \item @{term "SGhost"}, and @{term "SFence"} as stubs for the corresponding memory instructions.
 \end{inparaenum}
 
 The key idea of the semantics is the following: expressions are evaluated by issuing instructions to the memory system, then the program waits until the memory system has made all necessary results available in the temporaries, which allows the program to make another step. Figure~\ref{fig:expression-evaluation} defines expression evaluation.
 %
 \begin{figure}
 \begin{tabularx}{\textwidth}{l@ {~~\<open>=\<close>~~}X}
 @{thm (lhs) issue_expr.simps (1) [no_vars]} & @{thm (rhs) issue_expr.simps (1) [no_vars]}\\
 @{thm (lhs) issue_expr.simps (2) [no_vars]} & @{thm (rhs) issue_expr.simps (2) [no_vars]}\\
 @{thm (lhs) issue_expr.simps (3) [where sop="(D,f)", no_vars]} & @{thm (rhs) issue_expr.simps (3) [where sop="(D,f)", no_vars]}\\
 @{thm (lhs) issue_expr.simps (4) [no_vars]} & @{thm (rhs) issue_expr.simps (4) [no_vars]}\\
 @{thm (lhs) issue_expr.simps (5) [no_vars]} & @{thm [break,margin=50] (rhs) issue_expr.simps (5) [no_vars]}\\
 \end{tabularx}\\[2pt]
 
 \begin{tabularx}{\textwidth}{l@ {~~\<open>=\<close>~~}X}
 @{thm (lhs) eval_expr.simps (1) [no_vars]} & @{thm (rhs) eval_expr.simps (1) [no_vars]}\\
 @{thm (lhs) eval_expr.simps (2) [no_vars]} & @{thm (rhs) eval_expr.simps (2) [no_vars]}\\
 @{thm (lhs) eval_expr.simps (3) [where sop="(D,f)", no_vars]} & @{thm (rhs) eval_expr.simps (3) [where sop="(D,f)",simplified fst_conv snd_conv, no_vars]}\\
 @{thm (lhs) eval_expr.simps (4) [no_vars]} & @{thm (rhs) eval_expr.simps (4) [no_vars]}\\
 @{thm (lhs) eval_expr.simps (5) [no_vars]} & @{thm [break,margin=50] (rhs) eval_expr.simps (5) [no_vars]}
 \end{tabularx}
 \caption{Expression evaluation\label{fig:expression-evaluation}}
 \end{figure}
 %
 The function @{term "used_tmps e"} calculates the number of temporaries that are necessary to evaluate expression @{term "e"}, where every @{term "Mem"} expression accounts to one temporary. 
 With @{term "issue_expr t e"} we obtain the instruction list for expression @{term "e"} starting at temporary @{term "t"}, whereas @{term "eval_expr t e"} constructs the operation as a pair of the domain and a function on the temporaries.
 
 The program transitions are defined in Figure~\ref{fig:program-transitions}. We instantiate the program state by a tuple @{term "(s,t)"} containing the statement @{term "s"} and the temporary counter @{term "t"}.
 %
 \begin{figure}
 \begin{center}
 @{thm [mode=Rule] AssignAddr' [no_vars]}\\[0.5\baselineskip]
 @{thm [mode=Rule] Assign' [no_vars]}\\[0.5\baselineskip]
 @{thm [mode=Rule] CASAddr' [no_vars]}\\[0.5\baselineskip]
 @{thm [mode=Rule] CASComp' [no_vars]}\\[0.5\baselineskip]
 @{thm [mode=Rule] CAS' [no_vars]}\\[0.5\baselineskip]
 @{thm [mode=Rule] stmt_step.Seq [no_vars]}\\[-0.3\baselineskip] 
 @{thm [mode=Axiom] stmt_step.SeqSkip [no_vars]} \\[0.5\baselineskip]
 @{thm [mode=Rule] SCond' [no_vars]}\\[0.5\baselineskip]
 @{thm [mode=Rule] stmt_step.CondTrue [no_vars]}\\[0.5\baselineskip]
 @{thm [mode=Rule] stmt_step.CondFalse [no_vars]}\\[-0.3\baselineskip]
 @{thm [mode=Axiom] While [no_vars]}\\[-0.3\baselineskip]
 @{thm [mode=Axiom] SGhost [no_vars]}\\[-0.3\baselineskip]
 @{thm [mode=Axiom] SFence [no_vars]}\\[0.1\baselineskip]
 \end{center}
 \caption{Program transitions\label{fig:program-transitions}}
 \end{figure}
 %
 To assign an expression @{term "e"} to an address(-expression) @{term "a"} we first create the memory instructions for evaluation the address @{term "a"} and transforming the expression to an operation on temporaries. The temporary counter is incremented accordingly. 
 When the value is available in the temporaries we continue by
 creating the memory instructions for evaluation of expression @{term "e"} followed by the corresponding store operation.
 Note that the ownership annotations can depend on the temporaries and thus can take the calculated address into account.
 
 Execution of compare and swap @{term "CAS"} involves evaluation of three expressions, the address @{term "a"} the compare value @{term "c\<^sub>e"} and the swap value @{term "s\<^sub>e"}. 
 It is finally mapped to the read-modify-write instruction @{term "RMW"} of the memory system. 
 Recall that execution of @{term "RMW"} first stores the memory content at address @{term "a"} to the specified temporary. 
 The condition compares this value with the result of evaluating @{term "c\<^sub>e"} and writes swap value @{term "s\<^sub>a"} if successful. 
 In either case the temporary finally returns the old value read.
  
 Sequential composition is straightforward. An if-then-else is computed by first issuing the memory instructions for evaluation of condition @{term "e"} and transforming the condition to an operation on temporaries. 
 When the result is available the transition to the first or second statement is made, depending on the result of @{const "isTrue"}.
 Execution of the loop is defined by stepwise unfolding.
 Ghost and fence statements are just propagated to the memory system.
 %
 
 To instantiate Theorem~\ref{thm:simulation} with PIMP we define the invariant parameter @{term "valid"}, which has to be maintained by all transitions of PIMP, the memory system and the store buffer. 
 Let @{term "\<theta>"} be the valuation of temporaries in the current configuration, for every thread configuration @{term "ts\<^sub>s\<^sub>b!i = ((s,t),is,\<theta>,sb,\<D>,\<O>)"} where @{term "i < length ts\<^sub>s\<^sub>b"} we require:
 %
 \begin{inparaenum}
 \item The domain of all intermediate @{term "Tmp (D,f)"} expressions in statement @{term "s"} is below counter @{term "t"}.
 \item All temporaries in the memory system including the store buffer are below counter @{term "t"}.
 \item All temporaries less than counter @{term "t"} are either already defined in the temporaries @{term "\<theta>"} or are outstanding read temporaries in the memory system.
 \end{inparaenum}
 
 For the PIMP transitions we prove these invariants by rule induction on the semantics.
 For the memory system (including the store buffer steps) the invariants are straightforward. 
 The memory system does not alter the program state and does not create new temporaries, only the PIMP transitions create new ones in strictly  ascending order. 
 \<close>
 
 
 
 (*<*)
 end
 (*>*)