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