src/HOL/Hoare_Parallel/RG_Examples.thy
author huffman
Sun Apr 01 16:09:58 2012 +0200 (2012-04-01)
changeset 47255 30a1692557b0
parent 44890 22f665a2e91c
child 51121 34dbeb8f16a9
permissions -rw-r--r--
removed Nat_Numeral.thy, moving all theorems elsewhere
     1 header {* \section{Examples} *}
     2 
     3 theory RG_Examples
     4 imports RG_Syntax
     5 begin
     6 
     7 lemmas definitions [simp]= stable_def Pre_def Rely_def Guar_def Post_def Com_def 
     8 
     9 subsection {* Set Elements of an Array to Zero *}
    10 
    11 lemma le_less_trans2: "\<lbrakk>(j::nat)<k; i\<le> j\<rbrakk> \<Longrightarrow> i<k"
    12 by simp
    13 
    14 lemma add_le_less_mono: "\<lbrakk> (a::nat) < c; b\<le>d \<rbrakk> \<Longrightarrow> a + b < c + d"
    15 by simp
    16 
    17 record Example1 =
    18   A :: "nat list"
    19 
    20 lemma Example1: 
    21  "\<turnstile> COBEGIN
    22       SCHEME [0 \<le> i < n]
    23      (\<acute>A := \<acute>A [i := 0], 
    24      \<lbrace> n < length \<acute>A \<rbrace>, 
    25      \<lbrace> length \<ordmasculine>A = length \<ordfeminine>A \<and> \<ordmasculine>A ! i = \<ordfeminine>A ! i \<rbrace>, 
    26      \<lbrace> length \<ordmasculine>A = length \<ordfeminine>A \<and> (\<forall>j<n. i \<noteq> j \<longrightarrow> \<ordmasculine>A ! j = \<ordfeminine>A ! j) \<rbrace>, 
    27      \<lbrace> \<acute>A ! i = 0 \<rbrace>) 
    28     COEND
    29  SAT [\<lbrace> n < length \<acute>A \<rbrace>, \<lbrace> \<ordmasculine>A = \<ordfeminine>A \<rbrace>, \<lbrace> True \<rbrace>, \<lbrace> \<forall>i < n. \<acute>A ! i = 0 \<rbrace>]"
    30 apply(rule Parallel)
    31 apply (auto intro!: Basic) 
    32 done
    33 
    34 lemma Example1_parameterized: 
    35 "k < t \<Longrightarrow>
    36   \<turnstile> COBEGIN 
    37     SCHEME [k*n\<le>i<(Suc k)*n] (\<acute>A:=\<acute>A[i:=0], 
    38    \<lbrace>t*n < length \<acute>A\<rbrace>, 
    39    \<lbrace>t*n < length \<ordmasculine>A \<and> length \<ordmasculine>A=length \<ordfeminine>A \<and> \<ordmasculine>A!i = \<ordfeminine>A!i\<rbrace>, 
    40    \<lbrace>t*n < length \<ordmasculine>A \<and> length \<ordmasculine>A=length \<ordfeminine>A \<and> (\<forall>j<length \<ordmasculine>A . i\<noteq>j \<longrightarrow> \<ordmasculine>A!j = \<ordfeminine>A!j)\<rbrace>, 
    41    \<lbrace>\<acute>A!i=0\<rbrace>) 
    42    COEND  
    43  SAT [\<lbrace>t*n < length \<acute>A\<rbrace>, 
    44       \<lbrace>t*n < length \<ordmasculine>A \<and> length \<ordmasculine>A=length \<ordfeminine>A \<and> (\<forall>i<n. \<ordmasculine>A!(k*n+i)=\<ordfeminine>A!(k*n+i))\<rbrace>, 
    45       \<lbrace>t*n < length \<ordmasculine>A \<and> length \<ordmasculine>A=length \<ordfeminine>A \<and> 
    46       (\<forall>i<length \<ordmasculine>A . (i<k*n \<longrightarrow> \<ordmasculine>A!i = \<ordfeminine>A!i) \<and> ((Suc k)*n \<le> i\<longrightarrow> \<ordmasculine>A!i = \<ordfeminine>A!i))\<rbrace>, 
    47       \<lbrace>\<forall>i<n. \<acute>A!(k*n+i) = 0\<rbrace>]"
    48 apply(rule Parallel)
    49     apply auto
    50   apply(erule_tac x="k*n +i" in allE)
    51   apply(subgoal_tac "k*n+i <length (A b)")
    52    apply force
    53   apply(erule le_less_trans2) 
    54   apply(case_tac t,simp+)
    55   apply (simp add:add_commute)
    56   apply(simp add: add_le_mono)
    57 apply(rule Basic)
    58    apply simp
    59    apply clarify
    60    apply (subgoal_tac "k*n+i< length (A x)")
    61     apply simp
    62    apply(erule le_less_trans2)
    63    apply(case_tac t,simp+)
    64    apply (simp add:add_commute)
    65    apply(rule add_le_mono, auto)
    66 done
    67 
    68 
    69 subsection {* Increment a Variable in Parallel *}
    70 
    71 subsubsection {* Two components *}
    72 
    73 record Example2 =
    74   x  :: nat
    75   c_0 :: nat
    76   c_1 :: nat
    77 
    78 lemma Example2: 
    79  "\<turnstile>  COBEGIN
    80     (\<langle> \<acute>x:=\<acute>x+1;; \<acute>c_0:=\<acute>c_0 + 1 \<rangle>, 
    81      \<lbrace>\<acute>x=\<acute>c_0 + \<acute>c_1  \<and> \<acute>c_0=0\<rbrace>, 
    82      \<lbrace>\<ordmasculine>c_0 = \<ordfeminine>c_0 \<and> 
    83         (\<ordmasculine>x=\<ordmasculine>c_0 + \<ordmasculine>c_1 
    84         \<longrightarrow> \<ordfeminine>x = \<ordfeminine>c_0 + \<ordfeminine>c_1)\<rbrace>,  
    85      \<lbrace>\<ordmasculine>c_1 = \<ordfeminine>c_1 \<and> 
    86          (\<ordmasculine>x=\<ordmasculine>c_0 + \<ordmasculine>c_1 
    87          \<longrightarrow> \<ordfeminine>x =\<ordfeminine>c_0 + \<ordfeminine>c_1)\<rbrace>,
    88      \<lbrace>\<acute>x=\<acute>c_0 + \<acute>c_1 \<and> \<acute>c_0=1 \<rbrace>)
    89   \<parallel>
    90       (\<langle> \<acute>x:=\<acute>x+1;; \<acute>c_1:=\<acute>c_1+1 \<rangle>, 
    91      \<lbrace>\<acute>x=\<acute>c_0 + \<acute>c_1 \<and> \<acute>c_1=0 \<rbrace>, 
    92      \<lbrace>\<ordmasculine>c_1 = \<ordfeminine>c_1 \<and> 
    93         (\<ordmasculine>x=\<ordmasculine>c_0 + \<ordmasculine>c_1 
    94         \<longrightarrow> \<ordfeminine>x = \<ordfeminine>c_0 + \<ordfeminine>c_1)\<rbrace>,  
    95      \<lbrace>\<ordmasculine>c_0 = \<ordfeminine>c_0 \<and> 
    96          (\<ordmasculine>x=\<ordmasculine>c_0 + \<ordmasculine>c_1 
    97         \<longrightarrow> \<ordfeminine>x =\<ordfeminine>c_0 + \<ordfeminine>c_1)\<rbrace>,
    98      \<lbrace>\<acute>x=\<acute>c_0 + \<acute>c_1 \<and> \<acute>c_1=1\<rbrace>)
    99  COEND
   100  SAT [\<lbrace>\<acute>x=0 \<and> \<acute>c_0=0 \<and> \<acute>c_1=0\<rbrace>, 
   101       \<lbrace>\<ordmasculine>x=\<ordfeminine>x \<and>  \<ordmasculine>c_0= \<ordfeminine>c_0 \<and> \<ordmasculine>c_1=\<ordfeminine>c_1\<rbrace>,
   102       \<lbrace>True\<rbrace>,
   103       \<lbrace>\<acute>x=2\<rbrace>]"
   104 apply(rule Parallel)
   105    apply simp_all
   106    apply clarify
   107    apply(case_tac i)
   108     apply simp
   109     apply(rule conjI)
   110      apply clarify
   111      apply simp
   112     apply clarify
   113     apply simp
   114    apply simp
   115    apply(rule conjI)
   116     apply clarify
   117     apply simp
   118    apply clarify
   119    apply simp
   120    apply(subgoal_tac "j=0")
   121     apply (simp)
   122    apply arith
   123   apply clarify
   124   apply(case_tac i,simp,simp)
   125  apply clarify
   126  apply simp
   127  apply(erule_tac x=0 in all_dupE)
   128  apply(erule_tac x=1 in allE,simp)
   129 apply clarify
   130 apply(case_tac i,simp)
   131  apply(rule Await)
   132   apply simp_all
   133  apply(clarify)
   134  apply(rule Seq)
   135   prefer 2
   136   apply(rule Basic)
   137    apply simp_all
   138   apply(rule subset_refl)
   139  apply(rule Basic)
   140  apply simp_all
   141  apply clarify
   142  apply simp
   143 apply(rule Await)
   144  apply simp_all
   145 apply(clarify)
   146 apply(rule Seq)
   147  prefer 2
   148  apply(rule Basic)
   149   apply simp_all
   150  apply(rule subset_refl)
   151 apply(auto intro!: Basic)
   152 done
   153 
   154 subsubsection {* Parameterized *}
   155 
   156 lemma Example2_lemma2_aux: "j<n \<Longrightarrow> 
   157  (\<Sum>i=0..<n. (b i::nat)) =
   158  (\<Sum>i=0..<j. b i) + b j + (\<Sum>i=0..<n-(Suc j) . b (Suc j + i))"
   159 apply(induct n)
   160  apply simp_all
   161 apply(simp add:less_Suc_eq)
   162  apply(auto)
   163 apply(subgoal_tac "n - j = Suc(n- Suc j)")
   164   apply simp
   165 apply arith
   166 done
   167 
   168 lemma Example2_lemma2_aux2: 
   169   "j\<le> s \<Longrightarrow> (\<Sum>i::nat=0..<j. (b (s:=t)) i) = (\<Sum>i=0..<j. b i)"
   170 apply(induct j)
   171  apply (simp_all cong:setsum_cong)
   172 done
   173 
   174 lemma Example2_lemma2: 
   175  "\<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow> Suc (\<Sum>i::nat=0..<n. b i)=(\<Sum>i=0..<n. (b (j := Suc 0)) i)"
   176 apply(frule_tac b="(b (j:=(Suc 0)))" in Example2_lemma2_aux)
   177 apply(erule_tac  t="setsum (b(j := (Suc 0))) {0..<n}" in ssubst)
   178 apply(frule_tac b=b in Example2_lemma2_aux)
   179 apply(erule_tac  t="setsum b {0..<n}" in ssubst)
   180 apply(subgoal_tac "Suc (setsum b {0..<j} + b j + (\<Sum>i=0..<n - Suc j. b (Suc j + i)))=(setsum b {0..<j} + Suc (b j) + (\<Sum>i=0..<n - Suc j. b (Suc j + i)))")
   181 apply(rotate_tac -1)
   182 apply(erule ssubst)
   183 apply(subgoal_tac "j\<le>j")
   184  apply(drule_tac b="b" and t="(Suc 0)" in Example2_lemma2_aux2)
   185 apply(rotate_tac -1)
   186 apply(erule ssubst)
   187 apply simp_all
   188 done
   189 
   190 lemma Example2_lemma2_Suc0: "\<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow>
   191  Suc (\<Sum>i::nat=0..< n. b i)=(\<Sum>i=0..< n. (b (j:=Suc 0)) i)"
   192 by(simp add:Example2_lemma2)
   193 
   194 record Example2_parameterized =   
   195   C :: "nat \<Rightarrow> nat"
   196   y  :: nat
   197 
   198 lemma Example2_parameterized: "0<n \<Longrightarrow> 
   199   \<turnstile> COBEGIN SCHEME  [0\<le>i<n]
   200      (\<langle> \<acute>y:=\<acute>y+1;; \<acute>C:=\<acute>C (i:=1) \<rangle>, 
   201      \<lbrace>\<acute>y=(\<Sum>i=0..<n. \<acute>C i) \<and> \<acute>C i=0\<rbrace>, 
   202      \<lbrace>\<ordmasculine>C i = \<ordfeminine>C i \<and> 
   203       (\<ordmasculine>y=(\<Sum>i=0..<n. \<ordmasculine>C i) \<longrightarrow> \<ordfeminine>y =(\<Sum>i=0..<n. \<ordfeminine>C i))\<rbrace>,  
   204      \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordmasculine>C j = \<ordfeminine>C j) \<and> 
   205        (\<ordmasculine>y=(\<Sum>i=0..<n. \<ordmasculine>C i) \<longrightarrow> \<ordfeminine>y =(\<Sum>i=0..<n. \<ordfeminine>C i))\<rbrace>,
   206      \<lbrace>\<acute>y=(\<Sum>i=0..<n. \<acute>C i) \<and> \<acute>C i=1\<rbrace>) 
   207     COEND
   208  SAT [\<lbrace>\<acute>y=0 \<and> (\<Sum>i=0..<n. \<acute>C i)=0 \<rbrace>, \<lbrace>\<ordmasculine>C=\<ordfeminine>C \<and> \<ordmasculine>y=\<ordfeminine>y\<rbrace>, \<lbrace>True\<rbrace>, \<lbrace>\<acute>y=n\<rbrace>]"
   209 apply(rule Parallel)
   210 apply force
   211 apply force
   212 apply(force)
   213 apply clarify
   214 apply simp
   215 apply(simp cong:setsum_ivl_cong)
   216 apply clarify
   217 apply simp
   218 apply(rule Await)
   219 apply simp_all
   220 apply clarify
   221 apply(rule Seq)
   222 prefer 2
   223 apply(rule Basic)
   224 apply(rule subset_refl)
   225 apply simp+
   226 apply(rule Basic)
   227 apply simp
   228 apply clarify
   229 apply simp
   230 apply(simp add:Example2_lemma2_Suc0 cong:if_cong)
   231 apply simp+
   232 done
   233 
   234 subsection {* Find Least Element *}
   235 
   236 text {* A previous lemma: *}
   237 
   238 lemma mod_aux :"\<lbrakk>i < (n::nat); a mod n = i;  j < a + n; j mod n = i; a < j\<rbrakk> \<Longrightarrow> False"
   239 apply(subgoal_tac "a=a div n*n + a mod n" )
   240  prefer 2 apply (simp (no_asm_use))
   241 apply(subgoal_tac "j=j div n*n + j mod n")
   242  prefer 2 apply (simp (no_asm_use))
   243 apply simp
   244 apply(subgoal_tac "a div n*n < j div n*n")
   245 prefer 2 apply arith
   246 apply(subgoal_tac "j div n*n < (a div n + 1)*n")
   247 prefer 2 apply simp
   248 apply (simp only:mult_less_cancel2)
   249 apply arith
   250 done
   251 
   252 record Example3 =
   253   X :: "nat \<Rightarrow> nat"
   254   Y :: "nat \<Rightarrow> nat"
   255 
   256 lemma Example3: "m mod n=0 \<Longrightarrow> 
   257  \<turnstile> COBEGIN 
   258  SCHEME [0\<le>i<n]
   259  (WHILE (\<forall>j<n. \<acute>X i < \<acute>Y j)  DO 
   260    IF P(B!(\<acute>X i)) THEN \<acute>Y:=\<acute>Y (i:=\<acute>X i) 
   261    ELSE \<acute>X:= \<acute>X (i:=(\<acute>X i)+ n) FI 
   262   OD,
   263  \<lbrace>(\<acute>X i) mod n=i \<and> (\<forall>j<\<acute>X i. j mod n=i \<longrightarrow> \<not>P(B!j)) \<and> (\<acute>Y i<m \<longrightarrow> P(B!(\<acute>Y i)) \<and> \<acute>Y i\<le> m+i)\<rbrace>,
   264  \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordfeminine>Y j \<le> \<ordmasculine>Y j) \<and> \<ordmasculine>X i = \<ordfeminine>X i \<and> 
   265    \<ordmasculine>Y i = \<ordfeminine>Y i\<rbrace>,
   266  \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordmasculine>X j = \<ordfeminine>X j \<and> \<ordmasculine>Y j = \<ordfeminine>Y j) \<and>   
   267    \<ordfeminine>Y i \<le> \<ordmasculine>Y i\<rbrace>,
   268  \<lbrace>(\<acute>X i) mod n=i \<and> (\<forall>j<\<acute>X i. j mod n=i \<longrightarrow> \<not>P(B!j)) \<and> (\<acute>Y i<m \<longrightarrow> P(B!(\<acute>Y i)) \<and> \<acute>Y i\<le> m+i) \<and> (\<exists>j<n. \<acute>Y j \<le> \<acute>X i) \<rbrace>) 
   269  COEND
   270  SAT [\<lbrace> \<forall>i<n. \<acute>X i=i \<and> \<acute>Y i=m+i \<rbrace>,\<lbrace>\<ordmasculine>X=\<ordfeminine>X \<and> \<ordmasculine>Y=\<ordfeminine>Y\<rbrace>,\<lbrace>True\<rbrace>,
   271   \<lbrace>\<forall>i<n. (\<acute>X i) mod n=i \<and> (\<forall>j<\<acute>X i. j mod n=i \<longrightarrow> \<not>P(B!j)) \<and> 
   272     (\<acute>Y i<m \<longrightarrow> P(B!(\<acute>Y i)) \<and> \<acute>Y i\<le> m+i) \<and> (\<exists>j<n. \<acute>Y j \<le> \<acute>X i)\<rbrace>]"
   273 apply(rule Parallel)
   274 --{*5 subgoals left *}
   275 apply force+
   276 apply clarify
   277 apply simp
   278 apply(rule While)
   279     apply force
   280    apply force
   281   apply force
   282  apply(rule_tac pre'="\<lbrace> \<acute>X i mod n = i \<and> (\<forall>j. j<\<acute>X i \<longrightarrow> j mod n = i \<longrightarrow> \<not>P(B!j)) \<and> (\<acute>Y i < n * q \<longrightarrow> P (B!(\<acute>Y i))) \<and> \<acute>X i<\<acute>Y i\<rbrace>" in Conseq)
   283      apply force
   284     apply(rule subset_refl)+
   285  apply(rule Cond)
   286     apply force
   287    apply(rule Basic)
   288       apply force
   289      apply fastforce
   290     apply force
   291    apply force
   292   apply(rule Basic)
   293      apply simp
   294      apply clarify
   295      apply simp
   296      apply (case_tac "X x (j mod n) \<le> j")
   297      apply (drule le_imp_less_or_eq)
   298      apply (erule disjE)
   299      apply (drule_tac j=j and n=n and i="j mod n" and a="X x (j mod n)" in mod_aux)
   300      apply auto
   301 done
   302 
   303 text {* Same but with a list as auxiliary variable: *}
   304 
   305 record Example3_list =
   306   X :: "nat list"
   307   Y :: "nat list"
   308 
   309 lemma Example3_list: "m mod n=0 \<Longrightarrow> \<turnstile> (COBEGIN SCHEME [0\<le>i<n]
   310  (WHILE (\<forall>j<n. \<acute>X!i < \<acute>Y!j)  DO 
   311      IF P(B!(\<acute>X!i)) THEN \<acute>Y:=\<acute>Y[i:=\<acute>X!i] ELSE \<acute>X:= \<acute>X[i:=(\<acute>X!i)+ n] FI 
   312   OD,
   313  \<lbrace>n<length \<acute>X \<and> n<length \<acute>Y \<and> (\<acute>X!i) mod n=i \<and> (\<forall>j<\<acute>X!i. j mod n=i \<longrightarrow> \<not>P(B!j)) \<and> (\<acute>Y!i<m \<longrightarrow> P(B!(\<acute>Y!i)) \<and> \<acute>Y!i\<le> m+i)\<rbrace>,
   314  \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordfeminine>Y!j \<le> \<ordmasculine>Y!j) \<and> \<ordmasculine>X!i = \<ordfeminine>X!i \<and> 
   315    \<ordmasculine>Y!i = \<ordfeminine>Y!i \<and> length \<ordmasculine>X = length \<ordfeminine>X \<and> length \<ordmasculine>Y = length \<ordfeminine>Y\<rbrace>,
   316  \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordmasculine>X!j = \<ordfeminine>X!j \<and> \<ordmasculine>Y!j = \<ordfeminine>Y!j) \<and>   
   317    \<ordfeminine>Y!i \<le> \<ordmasculine>Y!i \<and> length \<ordmasculine>X = length \<ordfeminine>X \<and> length \<ordmasculine>Y = length \<ordfeminine>Y\<rbrace>,
   318  \<lbrace>(\<acute>X!i) mod n=i \<and> (\<forall>j<\<acute>X!i. j mod n=i \<longrightarrow> \<not>P(B!j)) \<and> (\<acute>Y!i<m \<longrightarrow> P(B!(\<acute>Y!i)) \<and> \<acute>Y!i\<le> m+i) \<and> (\<exists>j<n. \<acute>Y!j \<le> \<acute>X!i) \<rbrace>) COEND)
   319  SAT [\<lbrace>n<length \<acute>X \<and> n<length \<acute>Y \<and> (\<forall>i<n. \<acute>X!i=i \<and> \<acute>Y!i=m+i) \<rbrace>,
   320       \<lbrace>\<ordmasculine>X=\<ordfeminine>X \<and> \<ordmasculine>Y=\<ordfeminine>Y\<rbrace>,
   321       \<lbrace>True\<rbrace>,
   322       \<lbrace>\<forall>i<n. (\<acute>X!i) mod n=i \<and> (\<forall>j<\<acute>X!i. j mod n=i \<longrightarrow> \<not>P(B!j)) \<and> 
   323         (\<acute>Y!i<m \<longrightarrow> P(B!(\<acute>Y!i)) \<and> \<acute>Y!i\<le> m+i) \<and> (\<exists>j<n. \<acute>Y!j \<le> \<acute>X!i)\<rbrace>]"
   324 apply(rule Parallel)
   325 --{* 5 subgoals left *}
   326 apply force+
   327 apply clarify
   328 apply simp
   329 apply(rule While)
   330     apply force
   331    apply force
   332   apply force
   333  apply(rule_tac pre'="\<lbrace>n<length \<acute>X \<and> n<length \<acute>Y \<and> \<acute>X ! i mod n = i \<and> (\<forall>j. j < \<acute>X ! i \<longrightarrow> j mod n = i \<longrightarrow> \<not> P (B ! j)) \<and> (\<acute>Y ! i < n * q \<longrightarrow> P (B ! (\<acute>Y ! i))) \<and> \<acute>X!i<\<acute>Y!i\<rbrace>" in Conseq)
   334      apply force
   335     apply(rule subset_refl)+
   336  apply(rule Cond)
   337     apply force
   338    apply(rule Basic)
   339       apply force
   340      apply force
   341     apply force
   342    apply force
   343   apply(rule Basic)
   344      apply simp
   345      apply clarify
   346      apply simp
   347      apply(rule allI)
   348      apply(rule impI)+
   349      apply(case_tac "X x ! i\<le> j")
   350       apply(drule le_imp_less_or_eq)
   351       apply(erule disjE)
   352        apply(drule_tac j=j and n=n and i=i and a="X x ! i" in mod_aux)
   353      apply auto
   354 done
   355 
   356 end