more standard argument order
authornipkow
Fri Apr 26 13:12:14 2013 +0200 (2013-04-26)
changeset 51791c4db685eaed0
parent 51790 22517d04d20b
child 51792 4b3d9b2412b4
more standard argument order
src/HOL/IMP/Abs_Int0.thy
src/HOL/IMP/Abs_Int1.thy
src/HOL/IMP/Abs_Int3.thy
     1.1 --- a/src/HOL/IMP/Abs_Int0.thy	Fri Apr 26 12:09:51 2013 +0200
     1.2 +++ b/src/HOL/IMP/Abs_Int0.thy	Fri Apr 26 13:12:14 2013 +0200
     1.3 @@ -309,27 +309,27 @@
     1.4  assumes h: "m x \<le> h"
     1.5  begin
     1.6  
     1.7 -definition m_s :: "vname set \<Rightarrow> 'av st \<Rightarrow> nat" ("m\<^isub>s") where
     1.8 -"m_s X S = (\<Sum> x \<in> X. m(S x))"
     1.9 +definition m_s :: "'av st \<Rightarrow> vname set \<Rightarrow> nat" ("m\<^isub>s") where
    1.10 +"m_s S X = (\<Sum> x \<in> X. m(S x))"
    1.11  
    1.12 -lemma m_s_h: "finite X \<Longrightarrow> m_s X S \<le> h * card X"
    1.13 +lemma m_s_h: "finite X \<Longrightarrow> m_s S X \<le> h * card X"
    1.14  by(simp add: m_s_def) (metis nat_mult_commute of_nat_id setsum_bounded[OF h])
    1.15  
    1.16 -fun m_o :: "vname set \<Rightarrow> 'av st option \<Rightarrow> nat" ("m\<^isub>o") where
    1.17 -"m_o X (Some S) = m_s X S" |
    1.18 -"m_o X None = h * card X + 1"
    1.19 +fun m_o :: "'av st option \<Rightarrow> vname set \<Rightarrow> nat" ("m\<^isub>o") where
    1.20 +"m_o (Some S) X = m_s S X" |
    1.21 +"m_o None X = h * card X + 1"
    1.22  
    1.23 -lemma m_o_h: "finite X \<Longrightarrow> m_o X opt \<le> (h*card X + 1)"
    1.24 +lemma m_o_h: "finite X \<Longrightarrow> m_o opt X \<le> (h*card X + 1)"
    1.25  by(cases opt)(auto simp add: m_s_h le_SucI dest: m_s_h)
    1.26  
    1.27  definition m_c :: "'av st option acom \<Rightarrow> nat" ("m\<^isub>c") where
    1.28 -"m_c C = listsum (map (m_o (vars C)) (annos C))"
    1.29 +"m_c C = listsum (map (\<lambda>a. m_o a (vars C)) (annos C))"
    1.30  
    1.31  text{* Upper complexity bound: *}
    1.32  lemma m_c_h: "m_c C \<le> size(annos C) * (h * card(vars C) + 1)"
    1.33  proof-
    1.34    let ?X = "vars C" let ?n = "card ?X" let ?a = "size(annos C)"
    1.35 -  have "m_c C = (\<Sum>i<?a. m_o ?X (annos C ! i))"
    1.36 +  have "m_c C = (\<Sum>i<?a. m_o (annos C ! i) ?X)"
    1.37      by(simp add: m_c_def listsum_setsum_nth atLeast0LessThan)
    1.38    also have "\<dots> \<le> (\<Sum>i<?a. h * ?n + 1)"
    1.39      apply(rule setsum_mono) using m_o_h[OF finite_Cvars] by simp
    1.40 @@ -415,13 +415,13 @@
    1.41    show "(\<Sum>x\<in>X. m (S2 x)) < (\<Sum>x\<in>X. m (S1 x))" .
    1.42  qed
    1.43  
    1.44 -lemma m_s2: "finite(X) \<Longrightarrow> S1 = S2 on -X \<Longrightarrow> S1 < S2 \<Longrightarrow> m_s X S1 > m_s X S2"
    1.45 +lemma m_s2: "finite(X) \<Longrightarrow> S1 = S2 on -X \<Longrightarrow> S1 < S2 \<Longrightarrow> m_s S1 X > m_s S2 X"
    1.46  apply(auto simp add: less_fun_def m_s_def)
    1.47  apply(simp add: m_s2_rep le_fun_def)
    1.48  done
    1.49  
    1.50  lemma m_o2: "finite X \<Longrightarrow> top_on_opt o1 (-X) \<Longrightarrow> top_on_opt o2 (-X) \<Longrightarrow>
    1.51 -  o1 < o2 \<Longrightarrow> m_o X o1 > m_o X o2"
    1.52 +  o1 < o2 \<Longrightarrow> m_o o1 X > m_o o2 X"
    1.53  proof(induction o1 o2 rule: less_eq_option.induct)
    1.54    case 1 thus ?case by (auto simp: m_s2 less_option_def)
    1.55  next
    1.56 @@ -431,7 +431,7 @@
    1.57  qed
    1.58  
    1.59  lemma m_o1: "finite X \<Longrightarrow> top_on_opt o1 (-X) \<Longrightarrow> top_on_opt o2 (-X) \<Longrightarrow>
    1.60 -  o1 \<le> o2 \<Longrightarrow> m_o X o1 \<ge> m_o X o2"
    1.61 +  o1 \<le> o2 \<Longrightarrow> m_o o1 X \<ge> m_o o2 X"
    1.62  by(auto simp: le_less m_o2)
    1.63  
    1.64  
    1.65 @@ -442,7 +442,7 @@
    1.66    assume top: "top_on_acom C1 (- vars(strip C2))"  "top_on_acom C2 (- vars(strip C2))"
    1.67    and strip_eq: "strip C1 = strip C2"
    1.68    and 0: "\<forall>i<size(annos C2). annos C1 ! i \<le> annos C2 ! i"
    1.69 -  hence 1: "\<forall>i<size(annos C2). m_o ?X (annos C1 ! i) \<ge> m_o ?X (annos C2 ! i)"
    1.70 +  hence 1: "\<forall>i<size(annos C2). m_o (annos C1 ! i) ?X \<ge> m_o (annos C2 ! i) ?X"
    1.71      apply (auto simp: all_set_conv_all_nth vars_acom_def top_on_acom_def)
    1.72      by (metis (lifting, no_types) finite_cvars m_o1 size_annos_same2)
    1.73    fix i assume i: "i < size(annos C2)" "\<not> annos C2 ! i \<le> annos C1 ! i"
    1.74 @@ -450,11 +450,11 @@
    1.75      using i(1) top(1) by(simp add: top_on_acom_def size_annos_same[OF strip_eq])
    1.76    have topo2: "top_on_opt (annos C2 ! i) (- ?X)"
    1.77      using i(1) top(2) by(simp add: top_on_acom_def size_annos_same[OF strip_eq])
    1.78 -  from i have "m_o ?X (annos C1 ! i) > m_o ?X (annos C2 ! i)" (is "?P i")
    1.79 +  from i have "m_o (annos C1 ! i) ?X > m_o (annos C2 ! i) ?X" (is "?P i")
    1.80      by (metis 0 less_option_def m_o2[OF finite_cvars topo1] topo2)
    1.81    hence 2: "\<exists>i < size(annos C2). ?P i" using `i < size(annos C2)` by blast
    1.82 -  have "(\<Sum>i<size(annos C2). m_o ?X (annos C2 ! i))
    1.83 -         < (\<Sum>i<size(annos C2). m_o ?X (annos C1 ! i))"
    1.84 +  have "(\<Sum>i<size(annos C2). m_o (annos C2 ! i) ?X)
    1.85 +         < (\<Sum>i<size(annos C2). m_o (annos C1 ! i) ?X)"
    1.86      apply(rule setsum_strict_mono_ex1) using 1 2 by (auto)
    1.87    thus ?thesis
    1.88      by(simp add: m_c_def vars_acom_def strip_eq listsum_setsum_nth atLeast0LessThan size_annos_same[OF strip_eq])
     2.1 --- a/src/HOL/IMP/Abs_Int1.thy	Fri Apr 26 12:09:51 2013 +0200
     2.2 +++ b/src/HOL/IMP/Abs_Int1.thy	Fri Apr 26 13:12:14 2013 +0200
     2.3 @@ -108,26 +108,26 @@
     2.4  assumes h: "m x \<le> h"
     2.5  begin
     2.6  
     2.7 -definition m_s :: "vname set \<Rightarrow> 'av st \<Rightarrow> nat" ("m\<^isub>s") where
     2.8 -"m_s X S = (\<Sum> x \<in> X. m(fun S x))"
     2.9 +definition m_s :: "'av st \<Rightarrow> vname set \<Rightarrow> nat" ("m\<^isub>s") where
    2.10 +"m_s S X = (\<Sum> x \<in> X. m(fun S x))"
    2.11  
    2.12 -lemma m_s_h: "finite X \<Longrightarrow> m_s X S \<le> h * card X"
    2.13 +lemma m_s_h: "finite X \<Longrightarrow> m_s S X \<le> h * card X"
    2.14  by(simp add: m_s_def) (metis nat_mult_commute of_nat_id setsum_bounded[OF h])
    2.15  
    2.16 -definition m_o :: "vname set \<Rightarrow> 'av st option \<Rightarrow> nat" ("m\<^isub>o") where
    2.17 -"m_o X opt = (case opt of None \<Rightarrow> h * card X + 1 | Some S \<Rightarrow> m_s X S)"
    2.18 +definition m_o :: "'av st option \<Rightarrow> vname set \<Rightarrow> nat" ("m\<^isub>o") where
    2.19 +"m_o opt X = (case opt of None \<Rightarrow> h * card X + 1 | Some S \<Rightarrow> m_s S X)"
    2.20  
    2.21 -lemma m_o_h: "finite X \<Longrightarrow> m_o X opt \<le> (h*card X + 1)"
    2.22 +lemma m_o_h: "finite X \<Longrightarrow> m_o opt X \<le> (h*card X + 1)"
    2.23  by(auto simp add: m_o_def m_s_h le_SucI split: option.split dest:m_s_h)
    2.24  
    2.25  definition m_c :: "'av st option acom \<Rightarrow> nat" ("m\<^isub>c") where
    2.26 -"m_c C = listsum (map (m_o (vars C)) (annos C))"
    2.27 +"m_c C = listsum (map (\<lambda>a. m_o a (vars C)) (annos C))"
    2.28  
    2.29  text{* Upper complexity bound: *}
    2.30  lemma m_c_h: "m_c C \<le> size(annos C) * (h * card(vars C) + 1)"
    2.31  proof-
    2.32    let ?X = "vars C" let ?n = "card ?X" let ?a = "size(annos C)"
    2.33 -  have "m_c C = (\<Sum>i<?a. m_o ?X (annos C ! i))"
    2.34 +  have "m_c C = (\<Sum>i<?a. m_o (annos C ! i) ?X)"
    2.35      by(simp add: m_c_def listsum_setsum_nth atLeast0LessThan)
    2.36    also have "\<dots> \<le> (\<Sum>i<?a. h * ?n + 1)"
    2.37      apply(rule setsum_mono) using m_o_h[OF finite_Cvars] by simp
    2.38 @@ -198,14 +198,15 @@
    2.39    show "(\<Sum>x\<in>X. m (S2 x)) < (\<Sum>x\<in>X. m (S1 x))" .
    2.40  qed
    2.41  
    2.42 -lemma m_s2: "finite(X) \<Longrightarrow> fun S1 = fun S2 on -X \<Longrightarrow> S1 < S2 \<Longrightarrow> m_s X S1 > m_s X S2"
    2.43 +lemma m_s2: "finite(X) \<Longrightarrow> fun S1 = fun S2 on -X
    2.44 +  \<Longrightarrow> S1 < S2 \<Longrightarrow> m_s S1 X > m_s S2 X"
    2.45  apply(auto simp add: less_st_def m_s_def)
    2.46  apply (transfer fixing: m)
    2.47  apply(simp add: less_eq_st_rep_iff eq_st_def m_s2_rep)
    2.48  done
    2.49  
    2.50  lemma m_o2: "finite X \<Longrightarrow> top_on_opt o1 (-X) \<Longrightarrow> top_on_opt o2 (-X) \<Longrightarrow>
    2.51 -  o1 < o2 \<Longrightarrow> m_o X o1 > m_o X o2"
    2.52 +  o1 < o2 \<Longrightarrow> m_o o1 X > m_o o2 X"
    2.53  proof(induction o1 o2 rule: less_eq_option.induct)
    2.54    case 1 thus ?case by (auto simp: m_o_def m_s2 less_option_def)
    2.55  next
    2.56 @@ -215,7 +216,7 @@
    2.57  qed
    2.58  
    2.59  lemma m_o1: "finite X \<Longrightarrow> top_on_opt o1 (-X) \<Longrightarrow> top_on_opt o2 (-X) \<Longrightarrow>
    2.60 -  o1 \<le> o2 \<Longrightarrow> m_o X o1 \<ge> m_o X o2"
    2.61 +  o1 \<le> o2 \<Longrightarrow> m_o o1 X \<ge> m_o o2 X"
    2.62  by(auto simp: le_less m_o2)
    2.63  
    2.64  
    2.65 @@ -226,7 +227,7 @@
    2.66    assume top: "top_on_acom C1 (- vars(strip C2))"  "top_on_acom C2 (- vars(strip C2))"
    2.67    and strip_eq: "strip C1 = strip C2"
    2.68    and 0: "\<forall>i<size(annos C2). annos C1 ! i \<le> annos C2 ! i"
    2.69 -  hence 1: "\<forall>i<size(annos C2). m_o ?X (annos C1 ! i) \<ge> m_o ?X (annos C2 ! i)"
    2.70 +  hence 1: "\<forall>i<size(annos C2). m_o (annos C1 ! i) ?X \<ge> m_o (annos C2 ! i) ?X"
    2.71      apply (auto simp: all_set_conv_all_nth vars_acom_def top_on_acom_def)
    2.72      by (metis finite_cvars m_o1 size_annos_same2)
    2.73    fix i assume i: "i < size(annos C2)" "\<not> annos C2 ! i \<le> annos C1 ! i"
    2.74 @@ -234,11 +235,11 @@
    2.75      using i(1) top(1) by(simp add: top_on_acom_def size_annos_same[OF strip_eq])
    2.76    have topo2: "top_on_opt (annos C2 ! i) (- ?X)"
    2.77      using i(1) top(2) by(simp add: top_on_acom_def size_annos_same[OF strip_eq])
    2.78 -  from i have "m_o ?X (annos C1 ! i) > m_o ?X (annos C2 ! i)" (is "?P i")
    2.79 +  from i have "m_o (annos C1 ! i) ?X > m_o (annos C2 ! i) ?X" (is "?P i")
    2.80      by (metis 0 less_option_def m_o2[OF finite_cvars topo1] topo2)
    2.81    hence 2: "\<exists>i < size(annos C2). ?P i" using `i < size(annos C2)` by blast
    2.82 -  have "(\<Sum>i<size(annos C2). m_o ?X (annos C2 ! i))
    2.83 -         < (\<Sum>i<size(annos C2). m_o ?X (annos C1 ! i))"
    2.84 +  have "(\<Sum>i<size(annos C2). m_o (annos C2 ! i) ?X)
    2.85 +         < (\<Sum>i<size(annos C2). m_o (annos C1 ! i) ?X)"
    2.86      apply(rule setsum_strict_mono_ex1) using 1 2 by (auto)
    2.87    thus ?thesis
    2.88      by(simp add: m_c_def vars_acom_def strip_eq listsum_setsum_nth atLeast0LessThan size_annos_same[OF strip_eq])
     3.1 --- a/src/HOL/IMP/Abs_Int3.thy	Fri Apr 26 12:09:51 2013 +0200
     3.2 +++ b/src/HOL/IMP/Abs_Int3.thy	Fri Apr 26 13:12:14 2013 +0200
     3.3 @@ -278,10 +278,8 @@
     3.4  
     3.5  subsubsection "Tests"
     3.6  
     3.7 -definition "step_up_ivl n =
     3.8 -  ((\<lambda>C. C \<nabla> step_ivl \<top> C)^^n)"
     3.9 -definition "step_down_ivl n =
    3.10 -  ((\<lambda>C. C \<triangle> step_ivl \<top> C)^^n)"
    3.11 +definition "step_up_ivl n = ((\<lambda>C. C \<nabla> step_ivl \<top> C)^^n)"
    3.12 +definition "step_down_ivl n = ((\<lambda>C. C \<triangle> step_ivl \<top> C)^^n)"
    3.13  
    3.14  text{* For @{const test3_ivl}, @{const AI_ivl} needed as many iterations as
    3.15  the loop took to execute. In contrast, @{const AI_ivl'} converges in a
    3.16 @@ -354,7 +352,7 @@
    3.17    thus "(\<Sum>x\<in>X. m (S2 x)) \<le> (\<Sum>x\<in>X. m (S1 x))" by (metis setsum_mono)
    3.18  qed
    3.19  
    3.20 -lemma m_s_anti_mono: "S1 \<le> S2 \<Longrightarrow> m_s X S1 \<ge> m_s X S2"
    3.21 +lemma m_s_anti_mono: "S1 \<le> S2 \<Longrightarrow> m_s S1 X \<ge> m_s S2 X"
    3.22  unfolding m_s_def
    3.23  apply (transfer fixing: m)
    3.24  apply(simp add: less_eq_st_rep_iff eq_st_def m_s_anti_mono_rep)
    3.25 @@ -374,14 +372,14 @@
    3.26  qed
    3.27  
    3.28  lemma m_s_widen: "finite X \<Longrightarrow> fun S1 = fun S2 on -X ==>
    3.29 -  ~ S2 \<le> S1 \<Longrightarrow> m_s X (S1 \<nabla> S2) < m_s X S1"
    3.30 +  ~ S2 \<le> S1 \<Longrightarrow> m_s (S1 \<nabla> S2) X < m_s S1 X"
    3.31  apply(auto simp add: less_st_def m_s_def)
    3.32  apply (transfer fixing: m)
    3.33  apply(auto simp add: less_eq_st_rep_iff m_s_widen_rep)
    3.34  done
    3.35  
    3.36  lemma m_o_anti_mono: "finite X \<Longrightarrow> top_on_opt o1 (-X) \<Longrightarrow> top_on_opt o2 (-X) \<Longrightarrow>
    3.37 -  o1 \<le> o2 \<Longrightarrow> m_o X o1 \<ge> m_o X o2"
    3.38 +  o1 \<le> o2 \<Longrightarrow> m_o o1 X \<ge> m_o o2 X"
    3.39  proof(induction o1 o2 rule: less_eq_option.induct)
    3.40    case 1 thus ?case by (simp add: m_o_def)(metis m_s_anti_mono)
    3.41  next
    3.42 @@ -392,7 +390,7 @@
    3.43  qed
    3.44  
    3.45  lemma m_o_widen: "\<lbrakk> finite X; top_on_opt S1 (-X); top_on_opt S2 (-X); \<not> S2 \<le> S1 \<rbrakk> \<Longrightarrow>
    3.46 -  m_o X (S1 \<nabla> S2) < m_o X S1"
    3.47 +  m_o (S1 \<nabla> S2) X < m_o S1 X"
    3.48  by(auto simp: m_o_def m_s_h less_Suc_eq_le m_s_widen split: option.split)
    3.49  
    3.50  lemma m_c_widen:
    3.51 @@ -409,8 +407,8 @@
    3.52  done
    3.53  
    3.54  
    3.55 -definition n_s :: "vname set \<Rightarrow> 'av st \<Rightarrow> nat" ("n\<^isub>s") where
    3.56 -"n\<^isub>s X S = (\<Sum>x\<in>X. n(fun S x))"
    3.57 +definition n_s :: "'av st \<Rightarrow> vname set \<Rightarrow> nat" ("n\<^isub>s") where
    3.58 +"n\<^isub>s S X = (\<Sum>x\<in>X. n(fun S x))"
    3.59  
    3.60  lemma n_s_narrow_rep:
    3.61  assumes "finite X"  "S1 = S2 on -X"  "\<forall>x. S2 x \<le> S1 x"  "\<forall>x. S1 x \<triangle> S2 x \<le> S1 x"
    3.62 @@ -427,25 +425,25 @@
    3.63  qed
    3.64  
    3.65  lemma n_s_narrow: "finite X \<Longrightarrow> fun S1 = fun S2 on -X \<Longrightarrow> S2 \<le> S1 \<Longrightarrow> S1 \<triangle> S2 < S1
    3.66 -  \<Longrightarrow> n\<^isub>s X (S1 \<triangle> S2) < n\<^isub>s X S1"
    3.67 +  \<Longrightarrow> n\<^isub>s (S1 \<triangle> S2) X < n\<^isub>s S1 X"
    3.68  apply(auto simp add: less_st_def n_s_def)
    3.69  apply (transfer fixing: n)
    3.70  apply(auto simp add: less_eq_st_rep_iff eq_st_def fun_eq_iff n_s_narrow_rep)
    3.71  done
    3.72  
    3.73 -definition n_o :: "vname set \<Rightarrow> 'av st option \<Rightarrow> nat" ("n\<^isub>o") where
    3.74 -"n\<^isub>o X opt = (case opt of None \<Rightarrow> 0 | Some S \<Rightarrow> n\<^isub>s X S + 1)"
    3.75 +definition n_o :: "'av st option \<Rightarrow> vname set \<Rightarrow> nat" ("n\<^isub>o") where
    3.76 +"n\<^isub>o opt X = (case opt of None \<Rightarrow> 0 | Some S \<Rightarrow> n\<^isub>s S X + 1)"
    3.77  
    3.78  lemma n_o_narrow:
    3.79    "top_on_opt S1 (-X) \<Longrightarrow> top_on_opt S2 (-X) \<Longrightarrow> finite X
    3.80 -  \<Longrightarrow> S2 \<le> S1 \<Longrightarrow> S1 \<triangle> S2 < S1 \<Longrightarrow> n\<^isub>o X (S1 \<triangle> S2) < n\<^isub>o X S1"
    3.81 +  \<Longrightarrow> S2 \<le> S1 \<Longrightarrow> S1 \<triangle> S2 < S1 \<Longrightarrow> n\<^isub>o (S1 \<triangle> S2) X < n\<^isub>o S1 X"
    3.82  apply(induction S1 S2 rule: narrow_option.induct)
    3.83  apply(auto simp: n_o_def n_s_narrow)
    3.84  done
    3.85  
    3.86  
    3.87  definition n_c :: "'av st option acom \<Rightarrow> nat" ("n\<^isub>c") where
    3.88 -"n\<^isub>c C = (let as = annos C in \<Sum>i<size as. n\<^isub>o (vars C) (as!i))"
    3.89 +"n\<^isub>c C = (let as = annos C in \<Sum>i<size as. n\<^isub>o (as!i) (vars C))"
    3.90  
    3.91  lemma less_annos_iff: "(C1 < C2) = (C1 \<le> C2 \<and>
    3.92    (\<exists>i<length (annos C1). annos C1 ! i < annos C2 ! i))"