src/HOL/Hoare_Parallel/RG_Examples.thy
author blanchet
Tue Nov 07 15:16:42 2017 +0100 (20 months ago)
changeset 67022 49309fe530fd
parent 64267 b9a1486e79be
child 67443 3abf6a722518
permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
     1 section \<open>Examples\<close>
     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 \<open>Set Elements of an Array to Zero\<close>
    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 \<open>Increment a Variable in Parallel\<close>
    70 
    71 subsubsection \<open>Two components\<close>
    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 "xa=0")
   121     apply simp
   122    apply arith
   123   apply clarify
   124   apply(case_tac xaa, 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 \<open>Parameterized\<close>
   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   by (induct j) simp_all
   171 
   172 lemma Example2_lemma2:
   173  "\<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)"
   174 apply(frule_tac b="(b (j:=(Suc 0)))" in Example2_lemma2_aux)
   175 apply(erule_tac  t="sum (b(j := (Suc 0))) {0..<n}" in ssubst)
   176 apply(frule_tac b=b in Example2_lemma2_aux)
   177 apply(erule_tac  t="sum b {0..<n}" in ssubst)
   178 apply(subgoal_tac "Suc (sum b {0..<j} + b j + (\<Sum>i=0..<n - Suc j. b (Suc j + i)))=(sum b {0..<j} + Suc (b j) + (\<Sum>i=0..<n - Suc j. b (Suc j + i)))")
   179 apply(rotate_tac -1)
   180 apply(erule ssubst)
   181 apply(subgoal_tac "j\<le>j")
   182  apply(drule_tac b="b" and t="(Suc 0)" in Example2_lemma2_aux2)
   183 apply(rotate_tac -1)
   184 apply(erule ssubst)
   185 apply simp_all
   186 done
   187 
   188 lemma Example2_lemma2_Suc0: "\<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow>
   189  Suc (\<Sum>i::nat=0..< n. b i)=(\<Sum>i=0..< n. (b (j:=Suc 0)) i)"
   190 by(simp add:Example2_lemma2)
   191 
   192 record Example2_parameterized =
   193   C :: "nat \<Rightarrow> nat"
   194   y  :: nat
   195 
   196 lemma Example2_parameterized: "0<n \<Longrightarrow>
   197   \<turnstile> COBEGIN SCHEME  [0\<le>i<n]
   198      (\<langle> \<acute>y:=\<acute>y+1;; \<acute>C:=\<acute>C (i:=1) \<rangle>,
   199      \<lbrace>\<acute>y=(\<Sum>i=0..<n. \<acute>C i) \<and> \<acute>C i=0\<rbrace>,
   200      \<lbrace>\<ordmasculine>C i = \<ordfeminine>C i \<and>
   201       (\<ordmasculine>y=(\<Sum>i=0..<n. \<ordmasculine>C i) \<longrightarrow> \<ordfeminine>y =(\<Sum>i=0..<n. \<ordfeminine>C i))\<rbrace>,
   202      \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordmasculine>C j = \<ordfeminine>C j) \<and>
   203        (\<ordmasculine>y=(\<Sum>i=0..<n. \<ordmasculine>C i) \<longrightarrow> \<ordfeminine>y =(\<Sum>i=0..<n. \<ordfeminine>C i))\<rbrace>,
   204      \<lbrace>\<acute>y=(\<Sum>i=0..<n. \<acute>C i) \<and> \<acute>C i=1\<rbrace>)
   205     COEND
   206  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>]"
   207 apply(rule Parallel)
   208 apply force
   209 apply force
   210 apply(force)
   211 apply clarify
   212 apply simp
   213 apply simp
   214 apply clarify
   215 apply simp
   216 apply(rule Await)
   217 apply simp_all
   218 apply clarify
   219 apply(rule Seq)
   220 prefer 2
   221 apply(rule Basic)
   222 apply(rule subset_refl)
   223 apply simp+
   224 apply(rule Basic)
   225 apply simp
   226 apply clarify
   227 apply simp
   228 apply(simp add:Example2_lemma2_Suc0 cong:if_cong)
   229 apply simp_all
   230 done
   231 
   232 subsection \<open>Find Least Element\<close>
   233 
   234 text \<open>A previous lemma:\<close>
   235 
   236 lemma mod_aux :"\<lbrakk>i < (n::nat); a mod n = i;  j < a + n; j mod n = i; a < j\<rbrakk> \<Longrightarrow> False"
   237 apply(subgoal_tac "a=a div n*n + a mod n" )
   238  prefer 2 apply (simp (no_asm_use))
   239 apply(subgoal_tac "j=j div n*n + j mod n")
   240  prefer 2 apply (simp (no_asm_use))
   241 apply simp
   242 apply(subgoal_tac "a div n*n < j div n*n")
   243 prefer 2 apply arith
   244 apply(subgoal_tac "j div n*n < (a div n + 1)*n")
   245 prefer 2 apply simp
   246 apply (simp only:mult_less_cancel2)
   247 apply arith
   248 done
   249 
   250 record Example3 =
   251   X :: "nat \<Rightarrow> nat"
   252   Y :: "nat \<Rightarrow> nat"
   253 
   254 lemma Example3: "m mod n=0 \<Longrightarrow>
   255  \<turnstile> COBEGIN
   256  SCHEME [0\<le>i<n]
   257  (WHILE (\<forall>j<n. \<acute>X i < \<acute>Y j)  DO
   258    IF P(B!(\<acute>X i)) THEN \<acute>Y:=\<acute>Y (i:=\<acute>X i)
   259    ELSE \<acute>X:= \<acute>X (i:=(\<acute>X i)+ n) FI
   260   OD,
   261  \<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>,
   262  \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordfeminine>Y j \<le> \<ordmasculine>Y j) \<and> \<ordmasculine>X i = \<ordfeminine>X i \<and>
   263    \<ordmasculine>Y i = \<ordfeminine>Y i\<rbrace>,
   264  \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordmasculine>X j = \<ordfeminine>X j \<and> \<ordmasculine>Y j = \<ordfeminine>Y j) \<and>
   265    \<ordfeminine>Y i \<le> \<ordmasculine>Y i\<rbrace>,
   266  \<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>)
   267  COEND
   268  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>,
   269   \<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>
   270     (\<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>]"
   271 apply(rule Parallel)
   272 \<comment>\<open>5 subgoals left\<close>
   273 apply force+
   274 apply clarify
   275 apply simp
   276 apply(rule While)
   277     apply force
   278    apply force
   279   apply force
   280  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)
   281      apply force
   282     apply(rule subset_refl)+
   283  apply(rule Cond)
   284     apply force
   285    apply(rule Basic)
   286       apply force
   287      apply fastforce
   288     apply force
   289    apply force
   290   apply(rule Basic)
   291      apply simp
   292      apply clarify
   293      apply simp
   294      apply (case_tac "X x (j mod n) \<le> j")
   295      apply (drule le_imp_less_or_eq)
   296      apply (erule disjE)
   297      apply (drule_tac j=j and n=n and i="j mod n" and a="X x (j mod n)" in mod_aux)
   298      apply auto
   299 done
   300 
   301 text \<open>Same but with a list as auxiliary variable:\<close>
   302 
   303 record Example3_list =
   304   X :: "nat list"
   305   Y :: "nat list"
   306 
   307 lemma Example3_list: "m mod n=0 \<Longrightarrow> \<turnstile> (COBEGIN SCHEME [0\<le>i<n]
   308  (WHILE (\<forall>j<n. \<acute>X!i < \<acute>Y!j)  DO
   309      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
   310   OD,
   311  \<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>,
   312  \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordfeminine>Y!j \<le> \<ordmasculine>Y!j) \<and> \<ordmasculine>X!i = \<ordfeminine>X!i \<and>
   313    \<ordmasculine>Y!i = \<ordfeminine>Y!i \<and> length \<ordmasculine>X = length \<ordfeminine>X \<and> length \<ordmasculine>Y = length \<ordfeminine>Y\<rbrace>,
   314  \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordmasculine>X!j = \<ordfeminine>X!j \<and> \<ordmasculine>Y!j = \<ordfeminine>Y!j) \<and>
   315    \<ordfeminine>Y!i \<le> \<ordmasculine>Y!i \<and> length \<ordmasculine>X = length \<ordfeminine>X \<and> length \<ordmasculine>Y = length \<ordfeminine>Y\<rbrace>,
   316  \<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)
   317  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>,
   318       \<lbrace>\<ordmasculine>X=\<ordfeminine>X \<and> \<ordmasculine>Y=\<ordfeminine>Y\<rbrace>,
   319       \<lbrace>True\<rbrace>,
   320       \<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>
   321         (\<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>]"
   322 apply (rule Parallel)
   323 apply (auto cong del: strong_INF_cong strong_SUP_cong)
   324 apply force
   325 apply (rule While)
   326     apply force
   327    apply force
   328   apply force
   329  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)
   330      apply force
   331     apply(rule subset_refl)+
   332  apply(rule Cond)
   333     apply force
   334    apply(rule Basic)
   335       apply force
   336      apply force
   337     apply force
   338    apply force
   339   apply(rule Basic)
   340      apply simp
   341      apply clarify
   342      apply simp
   343      apply(rule allI)
   344      apply(rule impI)+
   345      apply(case_tac "X x ! i\<le> j")
   346       apply(drule le_imp_less_or_eq)
   347       apply(erule disjE)
   348        apply(drule_tac j=j and n=n and i=i and a="X x ! i" in mod_aux)
   349      apply auto
   350 done
   351 
   352 end