src/HOL/Hoare_Parallel/RG_Examples.thy
author wenzelm
Sun, 11 Feb 2018 12:51:23 +0100
changeset 67593 5efb88c90051
parent 67443 3abf6a722518
child 68260 61188c781cdd
permissions -rw-r--r--
clarified command-line defaults;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
59189
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
     1
section \<open>Examples\<close>
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     2
27651
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 16733
diff changeset
     3
theory RG_Examples
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 16733
diff changeset
     4
imports RG_Syntax
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 16733
diff changeset
     5
begin
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     6
59189
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
     7
lemmas definitions [simp]= stable_def Pre_def Rely_def Guar_def Post_def Com_def
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     8
59189
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
     9
subsection \<open>Set Elements of an Array to Zero\<close>
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    10
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    11
lemma le_less_trans2: "\<lbrakk>(j::nat)<k; i\<le> j\<rbrakk> \<Longrightarrow> i<k"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    12
by simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    13
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    14
lemma add_le_less_mono: "\<lbrakk> (a::nat) < c; b\<le>d \<rbrakk> \<Longrightarrow> a + b < c + d"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    15
by simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    16
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    17
record Example1 =
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    18
  A :: "nat list"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    19
59189
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
    20
lemma Example1:
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    21
 "\<turnstile> COBEGIN
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    22
      SCHEME [0 \<le> i < n]
59189
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
    23
     (\<acute>A := \<acute>A [i := 0],
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
    24
     \<lbrace> n < length \<acute>A \<rbrace>,
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
    25
     \<lbrace> length \<ordmasculine>A = length \<ordfeminine>A \<and> \<ordmasculine>A ! i = \<ordfeminine>A ! i \<rbrace>,
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
    26
     \<lbrace> length \<ordmasculine>A = length \<ordfeminine>A \<and> (\<forall>j<n. i \<noteq> j \<longrightarrow> \<ordmasculine>A ! j = \<ordfeminine>A ! j) \<rbrace>,
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
    27
     \<lbrace> \<acute>A ! i = 0 \<rbrace>)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    28
    COEND
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    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>]"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    30
apply(rule Parallel)
59189
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
    31
apply (auto intro!: Basic)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    32
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    33
59189
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
    34
lemma Example1_parameterized:
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    35
"k < t \<Longrightarrow>
59189
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
    36
  \<turnstile> COBEGIN
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
    37
    SCHEME [k*n\<le>i<(Suc k)*n] (\<acute>A:=\<acute>A[i:=0],
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
    38
   \<lbrace>t*n < length \<acute>A\<rbrace>,
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
    39
   \<lbrace>t*n < length \<ordmasculine>A \<and> length \<ordmasculine>A=length \<ordfeminine>A \<and> \<ordmasculine>A!i = \<ordfeminine>A!i\<rbrace>,
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
    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>,
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
    41
   \<lbrace>\<acute>A!i=0\<rbrace>)
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
    42
   COEND
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
    43
 SAT [\<lbrace>t*n < length \<acute>A\<rbrace>,
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
    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>,
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
    45
      \<lbrace>t*n < length \<ordmasculine>A \<and> length \<ordmasculine>A=length \<ordfeminine>A \<and>
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
    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>,
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    47
      \<lbrace>\<forall>i<n. \<acute>A!(k*n+i) = 0\<rbrace>]"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    48
apply(rule Parallel)
15102
04b0e943fcc9 new simprules Int_subset_iff and Un_subset_iff
paulson
parents: 15045
diff changeset
    49
    apply auto
04b0e943fcc9 new simprules Int_subset_iff and Un_subset_iff
paulson
parents: 15045
diff changeset
    50
  apply(erule_tac x="k*n +i" in allE)
04b0e943fcc9 new simprules Int_subset_iff and Un_subset_iff
paulson
parents: 15045
diff changeset
    51
  apply(subgoal_tac "k*n+i <length (A b)")
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    52
   apply force
59189
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
    53
  apply(erule le_less_trans2)
15102
04b0e943fcc9 new simprules Int_subset_iff and Un_subset_iff
paulson
parents: 15045
diff changeset
    54
  apply(case_tac t,simp+)
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 56248
diff changeset
    55
  apply (simp add:add.commute)
15102
04b0e943fcc9 new simprules Int_subset_iff and Un_subset_iff
paulson
parents: 15045
diff changeset
    56
  apply(simp add: add_le_mono)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    57
apply(rule Basic)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    58
   apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    59
   apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    60
   apply (subgoal_tac "k*n+i< length (A x)")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    61
    apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    62
   apply(erule le_less_trans2)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    63
   apply(case_tac t,simp+)
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 56248
diff changeset
    64
   apply (simp add:add.commute)
15102
04b0e943fcc9 new simprules Int_subset_iff and Un_subset_iff
paulson
parents: 15045
diff changeset
    65
   apply(rule add_le_mono, auto)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    66
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    67
15102
04b0e943fcc9 new simprules Int_subset_iff and Un_subset_iff
paulson
parents: 15045
diff changeset
    68
59189
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
    69
subsection \<open>Increment a Variable in Parallel\<close>
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    70
59189
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
    71
subsubsection \<open>Two components\<close>
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    72
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    73
record Example2 =
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    74
  x  :: nat
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    75
  c_0 :: nat
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    76
  c_1 :: nat
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    77
59189
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
    78
lemma Example2:
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    79
 "\<turnstile>  COBEGIN
59189
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
    80
    (\<langle> \<acute>x:=\<acute>x+1;; \<acute>c_0:=\<acute>c_0 + 1 \<rangle>,
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
    81
     \<lbrace>\<acute>x=\<acute>c_0 + \<acute>c_1  \<and> \<acute>c_0=0\<rbrace>,
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
    82
     \<lbrace>\<ordmasculine>c_0 = \<ordfeminine>c_0 \<and>
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
    83
        (\<ordmasculine>x=\<ordmasculine>c_0 + \<ordmasculine>c_1
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
    84
        \<longrightarrow> \<ordfeminine>x = \<ordfeminine>c_0 + \<ordfeminine>c_1)\<rbrace>,
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
    85
     \<lbrace>\<ordmasculine>c_1 = \<ordfeminine>c_1 \<and>
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
    86
         (\<ordmasculine>x=\<ordmasculine>c_0 + \<ordmasculine>c_1
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    87
         \<longrightarrow> \<ordfeminine>x =\<ordfeminine>c_0 + \<ordfeminine>c_1)\<rbrace>,
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    88
     \<lbrace>\<acute>x=\<acute>c_0 + \<acute>c_1 \<and> \<acute>c_0=1 \<rbrace>)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    89
  \<parallel>
59189
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
    90
      (\<langle> \<acute>x:=\<acute>x+1;; \<acute>c_1:=\<acute>c_1+1 \<rangle>,
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
    91
     \<lbrace>\<acute>x=\<acute>c_0 + \<acute>c_1 \<and> \<acute>c_1=0 \<rbrace>,
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
    92
     \<lbrace>\<ordmasculine>c_1 = \<ordfeminine>c_1 \<and>
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
    93
        (\<ordmasculine>x=\<ordmasculine>c_0 + \<ordmasculine>c_1
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
    94
        \<longrightarrow> \<ordfeminine>x = \<ordfeminine>c_0 + \<ordfeminine>c_1)\<rbrace>,
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
    95
     \<lbrace>\<ordmasculine>c_0 = \<ordfeminine>c_0 \<and>
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
    96
         (\<ordmasculine>x=\<ordmasculine>c_0 + \<ordmasculine>c_1
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    97
        \<longrightarrow> \<ordfeminine>x =\<ordfeminine>c_0 + \<ordfeminine>c_1)\<rbrace>,
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    98
     \<lbrace>\<acute>x=\<acute>c_0 + \<acute>c_1 \<and> \<acute>c_1=1\<rbrace>)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    99
 COEND
59189
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
   100
 SAT [\<lbrace>\<acute>x=0 \<and> \<acute>c_0=0 \<and> \<acute>c_1=0\<rbrace>,
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   101
      \<lbrace>\<ordmasculine>x=\<ordfeminine>x \<and>  \<ordmasculine>c_0= \<ordfeminine>c_0 \<and> \<ordmasculine>c_1=\<ordfeminine>c_1\<rbrace>,
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   102
      \<lbrace>True\<rbrace>,
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   103
      \<lbrace>\<acute>x=2\<rbrace>]"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   104
apply(rule Parallel)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   105
   apply simp_all
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   106
   apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   107
   apply(case_tac i)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   108
    apply simp
15102
04b0e943fcc9 new simprules Int_subset_iff and Un_subset_iff
paulson
parents: 15045
diff changeset
   109
    apply(rule conjI)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   110
     apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   111
     apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   112
    apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   113
    apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   114
   apply simp
15102
04b0e943fcc9 new simprules Int_subset_iff and Un_subset_iff
paulson
parents: 15045
diff changeset
   115
   apply(rule conjI)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   116
    apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   117
    apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   118
   apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   119
   apply simp
56248
67dc9549fa15 generalized and strengthened cong rules on compound operators, similar to 1ed737a98198
haftmann
parents: 52567
diff changeset
   120
   apply(subgoal_tac "xa=0")
67dc9549fa15 generalized and strengthened cong rules on compound operators, similar to 1ed737a98198
haftmann
parents: 52567
diff changeset
   121
    apply simp
13187
e5434b822a96 Modifications due to enhanced linear arithmetic.
nipkow
parents: 13103
diff changeset
   122
   apply arith
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   123
  apply clarify
56248
67dc9549fa15 generalized and strengthened cong rules on compound operators, similar to 1ed737a98198
haftmann
parents: 52567
diff changeset
   124
  apply(case_tac xaa, simp, simp)
34233
156c42518cfc removed more asm_rl's - unfortunately slowdown of 1 min.
nipkow
parents: 32621
diff changeset
   125
 apply clarify
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   126
 apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   127
 apply(erule_tac x=0 in all_dupE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   128
 apply(erule_tac x=1 in allE,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   129
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   130
apply(case_tac i,simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   131
 apply(rule Await)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   132
  apply simp_all
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   133
 apply(clarify)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   134
 apply(rule Seq)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   135
  prefer 2
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   136
  apply(rule Basic)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   137
   apply simp_all
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   138
  apply(rule subset_refl)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   139
 apply(rule Basic)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   140
 apply simp_all
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   141
 apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   142
 apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   143
apply(rule Await)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   144
 apply simp_all
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   145
apply(clarify)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   146
apply(rule Seq)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   147
 prefer 2
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   148
 apply(rule Basic)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   149
  apply simp_all
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   150
 apply(rule subset_refl)
15102
04b0e943fcc9 new simprules Int_subset_iff and Un_subset_iff
paulson
parents: 15045
diff changeset
   151
apply(auto intro!: Basic)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   152
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   153
59189
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
   154
subsubsection \<open>Parameterized\<close>
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   155
59189
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
   156
lemma Example2_lemma2_aux: "j<n \<Longrightarrow>
15561
045a07ac35a7 another reorganization of setsums and intervals
nipkow
parents: 15102
diff changeset
   157
 (\<Sum>i=0..<n. (b i::nat)) =
045a07ac35a7 another reorganization of setsums and intervals
nipkow
parents: 15102
diff changeset
   158
 (\<Sum>i=0..<j. b i) + b j + (\<Sum>i=0..<n-(Suc j) . b (Suc j + i))"
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   159
apply(induct n)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   160
 apply simp_all
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   161
apply(simp add:less_Suc_eq)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   162
 apply(auto)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   163
apply(subgoal_tac "n - j = Suc(n- Suc j)")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   164
  apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   165
apply arith
15561
045a07ac35a7 another reorganization of setsums and intervals
nipkow
parents: 15102
diff changeset
   166
done
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   167
59189
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
   168
lemma Example2_lemma2_aux2:
15561
045a07ac35a7 another reorganization of setsums and intervals
nipkow
parents: 15102
diff changeset
   169
  "j\<le> s \<Longrightarrow> (\<Sum>i::nat=0..<j. (b (s:=t)) i) = (\<Sum>i=0..<j. b i)"
52567
b6912471b8f5 tuned proofs;
wenzelm
parents: 51121
diff changeset
   170
  by (induct j) simp_all
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   171
59189
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
   172
lemma Example2_lemma2:
15561
045a07ac35a7 another reorganization of setsums and intervals
nipkow
parents: 15102
diff changeset
   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)"
15041
a6b1f0cef7b3 Got rid of Summation and made it a translation into setsum instead.
nipkow
parents: 14174
diff changeset
   174
apply(frule_tac b="(b (j:=(Suc 0)))" in Example2_lemma2_aux)
64267
b9a1486e79be setsum -> sum
nipkow
parents: 62042
diff changeset
   175
apply(erule_tac  t="sum (b(j := (Suc 0))) {0..<n}" in ssubst)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   176
apply(frule_tac b=b in Example2_lemma2_aux)
64267
b9a1486e79be setsum -> sum
nipkow
parents: 62042
diff changeset
   177
apply(erule_tac  t="sum b {0..<n}" in ssubst)
b9a1486e79be setsum -> sum
nipkow
parents: 62042
diff changeset
   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)))")
15041
a6b1f0cef7b3 Got rid of Summation and made it a translation into setsum instead.
nipkow
parents: 14174
diff changeset
   179
apply(rotate_tac -1)
a6b1f0cef7b3 Got rid of Summation and made it a translation into setsum instead.
nipkow
parents: 14174
diff changeset
   180
apply(erule ssubst)
a6b1f0cef7b3 Got rid of Summation and made it a translation into setsum instead.
nipkow
parents: 14174
diff changeset
   181
apply(subgoal_tac "j\<le>j")
a6b1f0cef7b3 Got rid of Summation and made it a translation into setsum instead.
nipkow
parents: 14174
diff changeset
   182
 apply(drule_tac b="b" and t="(Suc 0)" in Example2_lemma2_aux2)
a6b1f0cef7b3 Got rid of Summation and made it a translation into setsum instead.
nipkow
parents: 14174
diff changeset
   183
apply(rotate_tac -1)
a6b1f0cef7b3 Got rid of Summation and made it a translation into setsum instead.
nipkow
parents: 14174
diff changeset
   184
apply(erule ssubst)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   185
apply simp_all
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   186
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   187
15561
045a07ac35a7 another reorganization of setsums and intervals
nipkow
parents: 15102
diff changeset
   188
lemma Example2_lemma2_Suc0: "\<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow>
045a07ac35a7 another reorganization of setsums and intervals
nipkow
parents: 15102
diff changeset
   189
 Suc (\<Sum>i::nat=0..< n. b i)=(\<Sum>i=0..< n. (b (j:=Suc 0)) i)"
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   190
by(simp add:Example2_lemma2)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   191
59189
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
   192
record Example2_parameterized =
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   193
  C :: "nat \<Rightarrow> nat"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   194
  y  :: nat
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   195
59189
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
   196
lemma Example2_parameterized: "0<n \<Longrightarrow>
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   197
  \<turnstile> COBEGIN SCHEME  [0\<le>i<n]
59189
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
   198
     (\<langle> \<acute>y:=\<acute>y+1;; \<acute>C:=\<acute>C (i:=1) \<rangle>,
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
   199
     \<lbrace>\<acute>y=(\<Sum>i=0..<n. \<acute>C i) \<and> \<acute>C i=0\<rbrace>,
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
   200
     \<lbrace>\<ordmasculine>C i = \<ordfeminine>C i \<and>
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
   201
      (\<ordmasculine>y=(\<Sum>i=0..<n. \<ordmasculine>C i) \<longrightarrow> \<ordfeminine>y =(\<Sum>i=0..<n. \<ordfeminine>C i))\<rbrace>,
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
   202
     \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordmasculine>C j = \<ordfeminine>C j) \<and>
15561
045a07ac35a7 another reorganization of setsums and intervals
nipkow
parents: 15102
diff changeset
   203
       (\<ordmasculine>y=(\<Sum>i=0..<n. \<ordmasculine>C i) \<longrightarrow> \<ordfeminine>y =(\<Sum>i=0..<n. \<ordfeminine>C i))\<rbrace>,
59189
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
   204
     \<lbrace>\<acute>y=(\<Sum>i=0..<n. \<acute>C i) \<and> \<acute>C i=1\<rbrace>)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   205
    COEND
15561
045a07ac35a7 another reorganization of setsums and intervals
nipkow
parents: 15102
diff changeset
   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>]"
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   207
apply(rule Parallel)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   208
apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   209
apply force
15561
045a07ac35a7 another reorganization of setsums and intervals
nipkow
parents: 15102
diff changeset
   210
apply(force)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   211
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   212
apply simp
52567
b6912471b8f5 tuned proofs;
wenzelm
parents: 51121
diff changeset
   213
apply simp
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   214
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   215
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   216
apply(rule Await)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   217
apply simp_all
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   218
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   219
apply(rule Seq)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   220
prefer 2
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   221
apply(rule Basic)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   222
apply(rule subset_refl)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   223
apply simp+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   224
apply(rule Basic)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   225
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   226
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   227
apply simp
16733
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16417
diff changeset
   228
apply(simp add:Example2_lemma2_Suc0 cong:if_cong)
52567
b6912471b8f5 tuned proofs;
wenzelm
parents: 51121
diff changeset
   229
apply simp_all
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   230
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   231
59189
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
   232
subsection \<open>Find Least Element\<close>
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   233
59189
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
   234
text \<open>A previous lemma:\<close>
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   235
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   236
lemma mod_aux :"\<lbrakk>i < (n::nat); a mod n = i;  j < a + n; j mod n = i; a < j\<rbrakk> \<Longrightarrow> False"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   237
apply(subgoal_tac "a=a div n*n + a mod n" )
13517
42efec18f5b2 Added div+mod cancelling simproc
nipkow
parents: 13187
diff changeset
   238
 prefer 2 apply (simp (no_asm_use))
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   239
apply(subgoal_tac "j=j div n*n + j mod n")
13517
42efec18f5b2 Added div+mod cancelling simproc
nipkow
parents: 13187
diff changeset
   240
 prefer 2 apply (simp (no_asm_use))
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   241
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   242
apply(subgoal_tac "a div n*n < j div n*n")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   243
prefer 2 apply arith
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   244
apply(subgoal_tac "j div n*n < (a div n + 1)*n")
13517
42efec18f5b2 Added div+mod cancelling simproc
nipkow
parents: 13187
diff changeset
   245
prefer 2 apply simp
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   246
apply (simp only:mult_less_cancel2)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   247
apply arith
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   248
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   249
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   250
record Example3 =
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   251
  X :: "nat \<Rightarrow> nat"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   252
  Y :: "nat \<Rightarrow> nat"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   253
59189
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
   254
lemma Example3: "m mod n=0 \<Longrightarrow>
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
   255
 \<turnstile> COBEGIN
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   256
 SCHEME [0\<le>i<n]
59189
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
   257
 (WHILE (\<forall>j<n. \<acute>X i < \<acute>Y j)  DO
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
   258
   IF P(B!(\<acute>X i)) THEN \<acute>Y:=\<acute>Y (i:=\<acute>X i)
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
   259
   ELSE \<acute>X:= \<acute>X (i:=(\<acute>X i)+ n) FI
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   260
  OD,
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   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>,
59189
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
   262
 \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordfeminine>Y j \<le> \<ordmasculine>Y j) \<and> \<ordmasculine>X i = \<ordfeminine>X i \<and>
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   263
   \<ordmasculine>Y i = \<ordfeminine>Y i\<rbrace>,
59189
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
   264
 \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordmasculine>X j = \<ordfeminine>X j \<and> \<ordmasculine>Y j = \<ordfeminine>Y j) \<and>
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   265
   \<ordfeminine>Y i \<le> \<ordmasculine>Y i\<rbrace>,
59189
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
   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>)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   267
 COEND
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   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>,
59189
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
   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>
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   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>]"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   271
apply(rule Parallel)
67443
3abf6a722518 standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents: 64267
diff changeset
   272
\<comment> \<open>5 subgoals left\<close>
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   273
apply force+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   274
apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   275
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   276
apply(rule While)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   277
    apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   278
   apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   279
  apply force
14174
f3cafd2929d5 Methods rule_tac etc support static (Isar) contexts.
ballarin
parents: 13601
diff changeset
   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)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   281
     apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   282
    apply(rule subset_refl)+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   283
 apply(rule Cond)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   284
    apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   285
   apply(rule Basic)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   286
      apply force
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 41842
diff changeset
   287
     apply fastforce
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   288
    apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   289
   apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   290
  apply(rule Basic)
27676
55676111ed69 (re-)added simp rules for (_ + _) div/mod _
haftmann
parents: 27651
diff changeset
   291
     apply simp
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   292
     apply clarify
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   293
     apply simp
27651
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 16733
diff changeset
   294
     apply (case_tac "X x (j mod n) \<le> j")
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 16733
diff changeset
   295
     apply (drule le_imp_less_or_eq)
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 16733
diff changeset
   296
     apply (erule disjE)
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 16733
diff changeset
   297
     apply (drule_tac j=j and n=n and i="j mod n" and a="X x (j mod n)" in mod_aux)
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 16733
diff changeset
   298
     apply auto
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   299
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   300
59189
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
   301
text \<open>Same but with a list as auxiliary variable:\<close>
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   302
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   303
record Example3_list =
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   304
  X :: "nat list"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   305
  Y :: "nat list"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   306
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   307
lemma Example3_list: "m mod n=0 \<Longrightarrow> \<turnstile> (COBEGIN SCHEME [0\<le>i<n]
59189
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
   308
 (WHILE (\<forall>j<n. \<acute>X!i < \<acute>Y!j)  DO
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
   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
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   310
  OD,
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   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>,
59189
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
   312
 \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordfeminine>Y!j \<le> \<ordmasculine>Y!j) \<and> \<ordmasculine>X!i = \<ordfeminine>X!i \<and>
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   313
   \<ordmasculine>Y!i = \<ordfeminine>Y!i \<and> length \<ordmasculine>X = length \<ordfeminine>X \<and> length \<ordmasculine>Y = length \<ordfeminine>Y\<rbrace>,
59189
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
   314
 \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordmasculine>X!j = \<ordfeminine>X!j \<and> \<ordmasculine>Y!j = \<ordfeminine>Y!j) \<and>
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   315
   \<ordfeminine>Y!i \<le> \<ordmasculine>Y!i \<and> length \<ordmasculine>X = length \<ordfeminine>X \<and> length \<ordmasculine>Y = length \<ordfeminine>Y\<rbrace>,
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   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)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   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>,
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   318
      \<lbrace>\<ordmasculine>X=\<ordfeminine>X \<and> \<ordmasculine>Y=\<ordfeminine>Y\<rbrace>,
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   319
      \<lbrace>True\<rbrace>,
59189
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
   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>
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   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>]"
56248
67dc9549fa15 generalized and strengthened cong rules on compound operators, similar to 1ed737a98198
haftmann
parents: 52567
diff changeset
   322
apply (rule Parallel)
59189
ad8e0a789af6 update_cartouches;
wenzelm
parents: 58884
diff changeset
   323
apply (auto cong del: strong_INF_cong strong_SUP_cong)
56248
67dc9549fa15 generalized and strengthened cong rules on compound operators, similar to 1ed737a98198
haftmann
parents: 52567
diff changeset
   324
apply force
67dc9549fa15 generalized and strengthened cong rules on compound operators, similar to 1ed737a98198
haftmann
parents: 52567
diff changeset
   325
apply (rule While)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   326
    apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   327
   apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   328
  apply force
14174
f3cafd2929d5 Methods rule_tac etc support static (Isar) contexts.
ballarin
parents: 13601
diff changeset
   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)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   330
     apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   331
    apply(rule subset_refl)+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   332
 apply(rule Cond)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   333
    apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   334
   apply(rule Basic)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   335
      apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   336
     apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   337
    apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   338
   apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   339
  apply(rule Basic)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   340
     apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   341
     apply clarify
27676
55676111ed69 (re-)added simp rules for (_ + _) div/mod _
haftmann
parents: 27651
diff changeset
   342
     apply simp
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   343
     apply(rule allI)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   344
     apply(rule impI)+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   345
     apply(case_tac "X x ! i\<le> j")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   346
      apply(drule le_imp_less_or_eq)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   347
      apply(erule disjE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   348
       apply(drule_tac j=j and n=n and i=i and a="X x ! i" in mod_aux)
27651
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 16733
diff changeset
   349
     apply auto
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   350
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   351
13187
e5434b822a96 Modifications due to enhanced linear arithmetic.
nipkow
parents: 13103
diff changeset
   352
end