src/HOL/HoareParallel/OG_Examples.thy
author nipkow
Wed, 02 Mar 2005 12:06:15 +0100
changeset 15561 045a07ac35a7
parent 15045 d59f7e2e18d3
child 15912 47aa1a8fcdc9
permissions -rw-r--r--
another reorganization of setsums and intervals
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     1
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     2
header {* \section{Examples} *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     3
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     4
theory OG_Examples = OG_Syntax:
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     5
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     6
subsection {* Mutual Exclusion *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     7
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     8
subsubsection {* Peterson's Algorithm I*}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     9
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    10
text {* Eike Best. "Semantics of Sequential and Parallel Programs", page 217. *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    11
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    12
record Petersons_mutex_1 =
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    13
 pr1 :: nat
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    14
 pr2 :: nat
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    15
 in1 :: bool
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    16
 in2 :: bool 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    17
 hold :: nat
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    18
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    19
lemma Petersons_mutex_1: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    20
  "\<parallel>- .{\<acute>pr1=0 \<and> \<not>\<acute>in1 \<and> \<acute>pr2=0 \<and> \<not>\<acute>in2 }.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    21
  COBEGIN .{\<acute>pr1=0 \<and> \<not>\<acute>in1}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    22
  WHILE True INV .{\<acute>pr1=0 \<and> \<not>\<acute>in1}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    23
  DO  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    24
  .{\<acute>pr1=0 \<and> \<not>\<acute>in1}. \<langle> \<acute>in1:=True,,\<acute>pr1:=1 \<rangle>;;  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    25
  .{\<acute>pr1=1 \<and> \<acute>in1}.  \<langle> \<acute>hold:=1,,\<acute>pr1:=2 \<rangle>;;  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    26
  .{\<acute>pr1=2 \<and> \<acute>in1 \<and> (\<acute>hold=1 \<or> \<acute>hold=2 \<and> \<acute>pr2=2)}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    27
  AWAIT (\<not>\<acute>in2 \<or> \<not>(\<acute>hold=1)) THEN \<acute>pr1:=3 END;;    
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    28
  .{\<acute>pr1=3 \<and> \<acute>in1 \<and> (\<acute>hold=1 \<or> \<acute>hold=2 \<and> \<acute>pr2=2)}. 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    29
   \<langle>\<acute>in1:=False,,\<acute>pr1:=0\<rangle> 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    30
  OD .{\<acute>pr1=0 \<and> \<not>\<acute>in1}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    31
  \<parallel>  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    32
  .{\<acute>pr2=0 \<and> \<not>\<acute>in2}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    33
  WHILE True INV .{\<acute>pr2=0 \<and> \<not>\<acute>in2}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    34
  DO  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    35
  .{\<acute>pr2=0 \<and> \<not>\<acute>in2}. \<langle> \<acute>in2:=True,,\<acute>pr2:=1 \<rangle>;;  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    36
  .{\<acute>pr2=1 \<and> \<acute>in2}. \<langle>  \<acute>hold:=2,,\<acute>pr2:=2 \<rangle>;;  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    37
  .{\<acute>pr2=2 \<and> \<acute>in2 \<and> (\<acute>hold=2 \<or> (\<acute>hold=1 \<and> \<acute>pr1=2))}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    38
  AWAIT (\<not>\<acute>in1 \<or> \<not>(\<acute>hold=2)) THEN \<acute>pr2:=3  END;;    
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    39
  .{\<acute>pr2=3 \<and> \<acute>in2 \<and> (\<acute>hold=2 \<or> (\<acute>hold=1 \<and> \<acute>pr1=2))}. 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    40
    \<langle>\<acute>in2:=False,,\<acute>pr2:=0\<rangle> 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    41
  OD .{\<acute>pr2=0 \<and> \<not>\<acute>in2}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    42
  COEND  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    43
  .{\<acute>pr1=0 \<and> \<not>\<acute>in1 \<and> \<acute>pr2=0 \<and> \<not>\<acute>in2}."
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    44
apply oghoare
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    45
--{* 104 verification conditions. *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    46
apply auto
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    47
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    48
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    49
subsubsection {*Peterson's Algorithm II: A Busy Wait Solution *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    50
 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    51
text {* Apt and Olderog. "Verification of sequential and concurrent Programs", page 282. *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    52
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    53
record Busy_wait_mutex =
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    54
 flag1 :: bool
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    55
 flag2 :: bool
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    56
 turn  :: nat
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    57
 after1 :: bool 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    58
 after2 :: bool
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    59
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    60
lemma Busy_wait_mutex: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    61
 "\<parallel>-  .{True}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    62
  \<acute>flag1:=False,, \<acute>flag2:=False,,  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    63
  COBEGIN .{\<not>\<acute>flag1}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    64
        WHILE True  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    65
        INV .{\<not>\<acute>flag1}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    66
        DO .{\<not>\<acute>flag1}. \<langle> \<acute>flag1:=True,,\<acute>after1:=False \<rangle>;;  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    67
           .{\<acute>flag1 \<and> \<not>\<acute>after1}. \<langle> \<acute>turn:=1,,\<acute>after1:=True \<rangle>;;  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    68
           .{\<acute>flag1 \<and> \<acute>after1 \<and> (\<acute>turn=1 \<or> \<acute>turn=2)}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    69
            WHILE \<not>(\<acute>flag2 \<longrightarrow> \<acute>turn=2)  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    70
            INV .{\<acute>flag1 \<and> \<acute>after1 \<and> (\<acute>turn=1 \<or> \<acute>turn=2)}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    71
            DO .{\<acute>flag1 \<and> \<acute>after1 \<and> (\<acute>turn=1 \<or> \<acute>turn=2)}. SKIP OD;; 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    72
           .{\<acute>flag1 \<and> \<acute>after1 \<and> (\<acute>flag2 \<and> \<acute>after2 \<longrightarrow> \<acute>turn=2)}.
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    73
            \<acute>flag1:=False  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    74
        OD  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    75
       .{False}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    76
  \<parallel>  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    77
     .{\<not>\<acute>flag2}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    78
        WHILE True  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    79
        INV .{\<not>\<acute>flag2}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    80
        DO .{\<not>\<acute>flag2}. \<langle> \<acute>flag2:=True,,\<acute>after2:=False \<rangle>;;  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    81
           .{\<acute>flag2 \<and> \<not>\<acute>after2}. \<langle> \<acute>turn:=2,,\<acute>after2:=True \<rangle>;;  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    82
           .{\<acute>flag2 \<and> \<acute>after2 \<and> (\<acute>turn=1 \<or> \<acute>turn=2)}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    83
            WHILE \<not>(\<acute>flag1 \<longrightarrow> \<acute>turn=1)  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    84
            INV .{\<acute>flag2 \<and> \<acute>after2 \<and> (\<acute>turn=1 \<or> \<acute>turn=2)}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    85
            DO .{\<acute>flag2 \<and> \<acute>after2 \<and> (\<acute>turn=1 \<or> \<acute>turn=2)}. SKIP OD;;  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    86
           .{\<acute>flag2 \<and> \<acute>after2 \<and> (\<acute>flag1 \<and> \<acute>after1 \<longrightarrow> \<acute>turn=1)}. 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    87
            \<acute>flag2:=False  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    88
        OD  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    89
       .{False}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    90
  COEND  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    91
  .{False}."
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    92
apply oghoare
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    93
--{* 122 vc *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    94
apply auto
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    95
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    96
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    97
subsubsection {* Peterson's Algorithm III: A Solution using Semaphores  *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    98
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    99
record  Semaphores_mutex =
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   100
 out :: bool
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   101
 who :: nat
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   102
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   103
lemma Semaphores_mutex: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   104
 "\<parallel>- .{i\<noteq>j}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   105
  \<acute>out:=True ,,  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   106
  COBEGIN .{i\<noteq>j}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   107
       WHILE True INV .{i\<noteq>j}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   108
       DO .{i\<noteq>j}. AWAIT \<acute>out THEN  \<acute>out:=False,, \<acute>who:=i END;;  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   109
          .{\<not>\<acute>out \<and> \<acute>who=i \<and> i\<noteq>j}. \<acute>out:=True OD  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   110
       .{False}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   111
  \<parallel>  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   112
       .{i\<noteq>j}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   113
       WHILE True INV .{i\<noteq>j}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   114
       DO .{i\<noteq>j}. AWAIT \<acute>out THEN  \<acute>out:=False,,\<acute>who:=j END;;  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   115
          .{\<not>\<acute>out \<and> \<acute>who=j \<and> i\<noteq>j}. \<acute>out:=True OD  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   116
       .{False}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   117
  COEND  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   118
  .{False}."
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   119
apply oghoare
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   120
--{* 38 vc *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   121
apply auto
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   122
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   123
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   124
subsubsection {* Peterson's Algorithm III: Parameterized version: *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   125
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   126
lemma Semaphores_parameterized_mutex: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   127
 "0<n \<Longrightarrow> \<parallel>- .{True}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   128
  \<acute>out:=True ,,  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   129
 COBEGIN
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   130
  SCHEME [0\<le> i< n]
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   131
    .{True}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   132
     WHILE True INV .{True}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   133
      DO .{True}. AWAIT \<acute>out THEN  \<acute>out:=False,, \<acute>who:=i END;;  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   134
         .{\<not>\<acute>out \<and> \<acute>who=i}. \<acute>out:=True OD
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   135
    .{False}. 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   136
 COEND
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   137
  .{False}." 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   138
apply oghoare
13187
e5434b822a96 Modifications due to enhanced linear arithmetic.
nipkow
parents: 13022
diff changeset
   139
--{* 20 vc *}
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   140
apply auto
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   141
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   142
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   143
subsubsection{* The Ticket Algorithm *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   144
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   145
record Ticket_mutex =
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   146
 num :: nat
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   147
 nextv :: nat
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   148
 turn :: "nat list"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   149
 index :: nat 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   150
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   151
lemma Ticket_mutex: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   152
 "\<lbrakk> 0<n; I=\<guillemotleft>n=length \<acute>turn \<and> 0<\<acute>nextv \<and> (\<forall>k l. k<n \<and> l<n \<and> k\<noteq>l 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   153
    \<longrightarrow> \<acute>turn!k < \<acute>num \<and> (\<acute>turn!k =0 \<or> \<acute>turn!k\<noteq>\<acute>turn!l))\<guillemotright> \<rbrakk>
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   154
   \<Longrightarrow> \<parallel>- .{n=length \<acute>turn}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   155
   \<acute>index:= 0,,
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   156
   WHILE \<acute>index < n INV .{n=length \<acute>turn \<and> (\<forall>i<\<acute>index. \<acute>turn!i=0)}. 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   157
    DO \<acute>turn:= \<acute>turn[\<acute>index:=0],, \<acute>index:=\<acute>index +1 OD,,
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   158
  \<acute>num:=1 ,, \<acute>nextv:=1 ,, 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   159
 COBEGIN
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   160
  SCHEME [0\<le> i< n]
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   161
    .{\<acute>I}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   162
     WHILE True INV .{\<acute>I}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   163
      DO .{\<acute>I}. \<langle> \<acute>turn :=\<acute>turn[i:=\<acute>num],, \<acute>num:=\<acute>num+1 \<rangle>;;  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   164
         .{\<acute>I}. WAIT \<acute>turn!i=\<acute>nextv END;;
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   165
         .{\<acute>I \<and> \<acute>turn!i=\<acute>nextv}. \<acute>nextv:=\<acute>nextv+1
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   166
      OD
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   167
    .{False}. 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   168
 COEND
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   169
  .{False}." 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   170
apply oghoare
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   171
--{* 35 vc *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   172
apply simp_all
13187
e5434b822a96 Modifications due to enhanced linear arithmetic.
nipkow
parents: 13022
diff changeset
   173
--{* 21 vc *}
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   174
apply(tactic {* ALLGOALS Clarify_tac *})
13187
e5434b822a96 Modifications due to enhanced linear arithmetic.
nipkow
parents: 13022
diff changeset
   175
--{* 11 vc *}
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   176
apply simp_all
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   177
apply(tactic {* ALLGOALS Clarify_tac *})
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   178
--{* 11 subgoals left *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   179
apply(erule less_SucE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   180
 apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   181
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   182
--{* 10 subgoals left *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   183
apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   184
apply(case_tac "i=k")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   185
 apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   186
apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   187
apply(case_tac "i=l")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   188
 apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   189
apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   190
--{* 8 subgoals left *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   191
prefer 8
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   192
apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   193
apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   194
--{* 6 subgoals left *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   195
prefer 6
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   196
apply(erule_tac x=i in allE)
13601
fd3e3d6b37b2 Adapted to new simplifier.
berghofe
parents: 13517
diff changeset
   197
apply fastsimp
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   198
--{* 5 subgoals left *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   199
prefer 5
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   200
apply(tactic {* ALLGOALS (case_tac "j=k") *})
13187
e5434b822a96 Modifications due to enhanced linear arithmetic.
nipkow
parents: 13022
diff changeset
   201
--{* 10 subgoals left *}
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   202
apply simp_all
13601
fd3e3d6b37b2 Adapted to new simplifier.
berghofe
parents: 13517
diff changeset
   203
apply(erule_tac x=k in allE)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   204
apply force
13187
e5434b822a96 Modifications due to enhanced linear arithmetic.
nipkow
parents: 13022
diff changeset
   205
--{* 9 subgoals left *}
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   206
apply(case_tac "j=l")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   207
 apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   208
 apply(erule_tac x=k in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   209
 apply(erule_tac x=k in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   210
 apply(erule_tac x=l in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   211
 apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   212
apply(erule_tac x=k in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   213
apply(erule_tac x=k in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   214
apply(erule_tac x=l in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   215
apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   216
--{* 8 subgoals left *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   217
apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   218
apply(case_tac "j=l")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   219
 apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   220
apply(erule_tac x=k in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   221
apply(erule_tac x=l in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   222
apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   223
apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   224
apply force
13187
e5434b822a96 Modifications due to enhanced linear arithmetic.
nipkow
parents: 13022
diff changeset
   225
--{* 5 subgoals left *}
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   226
apply(erule_tac x=k in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   227
apply(erule_tac x=l in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   228
apply(case_tac "j=l")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   229
 apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   230
apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   231
apply force
13187
e5434b822a96 Modifications due to enhanced linear arithmetic.
nipkow
parents: 13022
diff changeset
   232
--{* 3 subgoals left *}
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   233
apply(erule_tac x=k in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   234
apply(erule_tac x=l in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   235
apply(case_tac "j=l")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   236
 apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   237
apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   238
apply force
13187
e5434b822a96 Modifications due to enhanced linear arithmetic.
nipkow
parents: 13022
diff changeset
   239
--{* 1 subgoals left *}
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   240
apply(erule_tac x=k in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   241
apply(erule_tac x=l in allE)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   242
apply(case_tac "j=l")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   243
 apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   244
apply force
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   245
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   246
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   247
subsection{* Parallel Zero Search *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   248
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   249
text {* Synchronized Zero Search. Zero-6 *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   250
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   251
text {*Apt and Olderog. "Verification of sequential and concurrent Programs" page 294: *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   252
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   253
record Zero_search =
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   254
   turn :: nat
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   255
   found :: bool
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   256
   x :: nat
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   257
   y :: nat
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   258
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   259
lemma Zero_search: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   260
  "\<lbrakk>I1= \<guillemotleft> a\<le>\<acute>x \<and> (\<acute>found \<longrightarrow> (a<\<acute>x \<and> f(\<acute>x)=0) \<or> (\<acute>y\<le>a \<and> f(\<acute>y)=0)) 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   261
      \<and> (\<not>\<acute>found \<and> a<\<acute> x \<longrightarrow> f(\<acute>x)\<noteq>0) \<guillemotright> ;  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   262
    I2= \<guillemotleft>\<acute>y\<le>a+1 \<and> (\<acute>found \<longrightarrow> (a<\<acute>x \<and> f(\<acute>x)=0) \<or> (\<acute>y\<le>a \<and> f(\<acute>y)=0)) 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   263
      \<and> (\<not>\<acute>found \<and> \<acute>y\<le>a \<longrightarrow> f(\<acute>y)\<noteq>0) \<guillemotright> \<rbrakk> \<Longrightarrow>  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   264
  \<parallel>- .{\<exists> u. f(u)=0}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   265
  \<acute>turn:=1,, \<acute>found:= False,,  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   266
  \<acute>x:=a,, \<acute>y:=a+1 ,,  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   267
  COBEGIN .{\<acute>I1}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   268
       WHILE \<not>\<acute>found  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   269
       INV .{\<acute>I1}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   270
       DO .{a\<le>\<acute>x \<and> (\<acute>found \<longrightarrow> \<acute>y\<le>a \<and> f(\<acute>y)=0) \<and> (a<\<acute>x \<longrightarrow> f(\<acute>x)\<noteq>0)}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   271
          WAIT \<acute>turn=1 END;;  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   272
          .{a\<le>\<acute>x \<and> (\<acute>found \<longrightarrow> \<acute>y\<le>a \<and> f(\<acute>y)=0) \<and> (a<\<acute>x \<longrightarrow> f(\<acute>x)\<noteq>0)}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   273
          \<acute>turn:=2;;  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   274
          .{a\<le>\<acute>x \<and> (\<acute>found \<longrightarrow> \<acute>y\<le>a \<and> f(\<acute>y)=0) \<and> (a<\<acute>x \<longrightarrow> f(\<acute>x)\<noteq>0)}.    
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   275
          \<langle> \<acute>x:=\<acute>x+1,,  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   276
            IF f(\<acute>x)=0 THEN \<acute>found:=True ELSE SKIP FI\<rangle>  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   277
       OD;;  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   278
       .{\<acute>I1  \<and> \<acute>found}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   279
       \<acute>turn:=2  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   280
       .{\<acute>I1 \<and> \<acute>found}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   281
  \<parallel>  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   282
      .{\<acute>I2}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   283
       WHILE \<not>\<acute>found  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   284
       INV .{\<acute>I2}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   285
       DO .{\<acute>y\<le>a+1 \<and> (\<acute>found \<longrightarrow> a<\<acute>x \<and> f(\<acute>x)=0) \<and> (\<acute>y\<le>a \<longrightarrow> f(\<acute>y)\<noteq>0)}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   286
          WAIT \<acute>turn=2 END;;  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   287
          .{\<acute>y\<le>a+1 \<and> (\<acute>found \<longrightarrow> a<\<acute>x \<and> f(\<acute>x)=0) \<and> (\<acute>y\<le>a \<longrightarrow> f(\<acute>y)\<noteq>0)}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   288
          \<acute>turn:=1;;  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   289
          .{\<acute>y\<le>a+1 \<and> (\<acute>found \<longrightarrow> a<\<acute>x \<and> f(\<acute>x)=0) \<and> (\<acute>y\<le>a \<longrightarrow> f(\<acute>y)\<noteq>0)}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   290
          \<langle> \<acute>y:=(\<acute>y - 1),,  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   291
            IF f(\<acute>y)=0 THEN \<acute>found:=True ELSE SKIP FI\<rangle>  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   292
       OD;;  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   293
       .{\<acute>I2 \<and> \<acute>found}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   294
       \<acute>turn:=1  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   295
       .{\<acute>I2 \<and> \<acute>found}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   296
  COEND  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   297
  .{f(\<acute>x)=0 \<or> f(\<acute>y)=0}."
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   298
apply oghoare
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   299
--{* 98 verification conditions *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   300
apply auto 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   301
--{* auto takes about 3 minutes !! *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   302
apply arith+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   303
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   304
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   305
text {* Easier Version: without AWAIT.  Apt and Olderog. page 256: *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   306
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   307
lemma Zero_Search_2: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   308
"\<lbrakk>I1=\<guillemotleft> a\<le>\<acute>x \<and> (\<acute>found \<longrightarrow> (a<\<acute>x \<and> f(\<acute>x)=0) \<or> (\<acute>y\<le>a \<and> f(\<acute>y)=0)) 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   309
    \<and> (\<not>\<acute>found \<and> a<\<acute>x \<longrightarrow> f(\<acute>x)\<noteq>0)\<guillemotright>;  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   310
 I2= \<guillemotleft>\<acute>y\<le>a+1 \<and> (\<acute>found \<longrightarrow> (a<\<acute>x \<and> f(\<acute>x)=0) \<or> (\<acute>y\<le>a \<and> f(\<acute>y)=0)) 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   311
    \<and> (\<not>\<acute>found \<and> \<acute>y\<le>a \<longrightarrow> f(\<acute>y)\<noteq>0)\<guillemotright>\<rbrakk> \<Longrightarrow>  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   312
  \<parallel>- .{\<exists>u. f(u)=0}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   313
  \<acute>found:= False,,  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   314
  \<acute>x:=a,, \<acute>y:=a+1,,  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   315
  COBEGIN .{\<acute>I1}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   316
       WHILE \<not>\<acute>found  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   317
       INV .{\<acute>I1}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   318
       DO .{a\<le>\<acute>x \<and> (\<acute>found \<longrightarrow> \<acute>y\<le>a \<and> f(\<acute>y)=0) \<and> (a<\<acute>x \<longrightarrow> f(\<acute>x)\<noteq>0)}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   319
          \<langle> \<acute>x:=\<acute>x+1,,IF f(\<acute>x)=0 THEN  \<acute>found:=True ELSE  SKIP FI\<rangle>  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   320
       OD  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   321
       .{\<acute>I1 \<and> \<acute>found}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   322
  \<parallel>  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   323
      .{\<acute>I2}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   324
       WHILE \<not>\<acute>found  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   325
       INV .{\<acute>I2}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   326
       DO .{\<acute>y\<le>a+1 \<and> (\<acute>found \<longrightarrow> a<\<acute>x \<and> f(\<acute>x)=0) \<and> (\<acute>y\<le>a \<longrightarrow> f(\<acute>y)\<noteq>0)}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   327
          \<langle> \<acute>y:=(\<acute>y - 1),,IF f(\<acute>y)=0 THEN  \<acute>found:=True ELSE  SKIP FI\<rangle>  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   328
       OD  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   329
       .{\<acute>I2 \<and> \<acute>found}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   330
  COEND  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   331
  .{f(\<acute>x)=0 \<or> f(\<acute>y)=0}."
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   332
apply oghoare
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   333
--{* 20 vc *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   334
apply auto
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   335
--{* auto takes aprox. 2 minutes. *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   336
apply arith+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   337
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   338
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   339
subsection {* Producer/Consumer *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   340
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   341
subsubsection {* Previous lemmas *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   342
13517
42efec18f5b2 Added div+mod cancelling simproc
nipkow
parents: 13187
diff changeset
   343
lemma nat_lemma2: "\<lbrakk> b = m*(n::nat) + t; a = s*n + u; t=u; b-a < n \<rbrakk> \<Longrightarrow> m \<le> s"
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   344
proof -
13517
42efec18f5b2 Added div+mod cancelling simproc
nipkow
parents: 13187
diff changeset
   345
  assume "b = m*(n::nat) + t" "a = s*n + u" "t=u"
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   346
  hence "(m - s) * n = b - a" by (simp add: diff_mult_distrib)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   347
  also assume "\<dots> < n"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   348
  finally have "m - s < 1" by simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   349
  thus ?thesis by arith
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   350
qed
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   351
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   352
lemma mod_lemma: "\<lbrakk> (c::nat) \<le> a; a < b; b - c < n \<rbrakk> \<Longrightarrow> b mod n \<noteq> a mod n"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   353
apply(subgoal_tac "b=b div n*n + b mod n" )
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   354
 prefer 2  apply (simp add: mod_div_equality [symmetric])
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   355
apply(subgoal_tac "a=a div n*n + a mod n")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   356
 prefer 2
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   357
 apply(simp add: mod_div_equality [symmetric])
13517
42efec18f5b2 Added div+mod cancelling simproc
nipkow
parents: 13187
diff changeset
   358
apply(subgoal_tac "b - a \<le> b - c")
42efec18f5b2 Added div+mod cancelling simproc
nipkow
parents: 13187
diff changeset
   359
 prefer 2 apply arith
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   360
apply(drule le_less_trans)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   361
back
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   362
 apply assumption
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   363
apply(frule less_not_refl2)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   364
apply(drule less_imp_le)
13517
42efec18f5b2 Added div+mod cancelling simproc
nipkow
parents: 13187
diff changeset
   365
apply (drule_tac m = "a" and k = n in div_le_mono)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   366
apply(safe)
13517
42efec18f5b2 Added div+mod cancelling simproc
nipkow
parents: 13187
diff changeset
   367
apply(frule_tac b = "b" and a = "a" and n = "n" in nat_lemma2, assumption, assumption)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   368
apply assumption
13517
42efec18f5b2 Added div+mod cancelling simproc
nipkow
parents: 13187
diff changeset
   369
apply(drule order_antisym, assumption)
42efec18f5b2 Added div+mod cancelling simproc
nipkow
parents: 13187
diff changeset
   370
apply(rotate_tac -3)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   371
apply(simp)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   372
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   373
13517
42efec18f5b2 Added div+mod cancelling simproc
nipkow
parents: 13187
diff changeset
   374
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   375
subsubsection {* Producer/Consumer Algorithm *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   376
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   377
record Producer_consumer =
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   378
  ins :: nat
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   379
  outs :: nat
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   380
  li :: nat
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   381
  lj :: nat
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   382
  vx :: nat
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   383
  vy :: nat
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   384
  buffer :: "nat list"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   385
  b :: "nat list"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   386
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   387
text {* The whole proof takes aprox. 4 minutes. *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   388
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   389
lemma Producer_consumer: 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   390
  "\<lbrakk>INIT= \<guillemotleft>0<length a \<and> 0<length \<acute>buffer \<and> length \<acute>b=length a\<guillemotright> ;  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   391
    I= \<guillemotleft>(\<forall>k<\<acute>ins. \<acute>outs\<le>k \<longrightarrow> (a ! k) = \<acute>buffer ! (k mod (length \<acute>buffer))) \<and>  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   392
            \<acute>outs\<le>\<acute>ins \<and> \<acute>ins-\<acute>outs\<le>length \<acute>buffer\<guillemotright> ;  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   393
    I1= \<guillemotleft>\<acute>I \<and> \<acute>li\<le>length a\<guillemotright> ;  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   394
    p1= \<guillemotleft>\<acute>I1 \<and> \<acute>li=\<acute>ins\<guillemotright> ;  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   395
    I2 = \<guillemotleft>\<acute>I \<and> (\<forall>k<\<acute>lj. (a ! k)=(\<acute>b ! k)) \<and> \<acute>lj\<le>length a\<guillemotright> ;
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   396
    p2 = \<guillemotleft>\<acute>I2 \<and> \<acute>lj=\<acute>outs\<guillemotright> \<rbrakk> \<Longrightarrow>   
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   397
  \<parallel>- .{\<acute>INIT}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   398
 \<acute>ins:=0,, \<acute>outs:=0,, \<acute>li:=0,, \<acute>lj:=0,,
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   399
 COBEGIN .{\<acute>p1 \<and> \<acute>INIT}. 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   400
   WHILE \<acute>li <length a 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   401
     INV .{\<acute>p1 \<and> \<acute>INIT}.   
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   402
   DO .{\<acute>p1 \<and> \<acute>INIT \<and> \<acute>li<length a}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   403
       \<acute>vx:= (a ! \<acute>li);;  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   404
      .{\<acute>p1 \<and> \<acute>INIT \<and> \<acute>li<length a \<and> \<acute>vx=(a ! \<acute>li)}. 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   405
        WAIT \<acute>ins-\<acute>outs < length \<acute>buffer END;; 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   406
      .{\<acute>p1 \<and> \<acute>INIT \<and> \<acute>li<length a \<and> \<acute>vx=(a ! \<acute>li) 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   407
         \<and> \<acute>ins-\<acute>outs < length \<acute>buffer}. 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   408
       \<acute>buffer:=(list_update \<acute>buffer (\<acute>ins mod (length \<acute>buffer)) \<acute>vx);; 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   409
      .{\<acute>p1 \<and> \<acute>INIT \<and> \<acute>li<length a 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   410
         \<and> (a ! \<acute>li)=(\<acute>buffer ! (\<acute>ins mod (length \<acute>buffer))) 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   411
         \<and> \<acute>ins-\<acute>outs <length \<acute>buffer}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   412
       \<acute>ins:=\<acute>ins+1;; 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   413
      .{\<acute>I1 \<and> \<acute>INIT \<and> (\<acute>li+1)=\<acute>ins \<and> \<acute>li<length a}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   414
       \<acute>li:=\<acute>li+1  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   415
   OD  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   416
  .{\<acute>p1 \<and> \<acute>INIT \<and> \<acute>li=length a}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   417
  \<parallel>  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   418
  .{\<acute>p2 \<and> \<acute>INIT}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   419
   WHILE \<acute>lj < length a  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   420
     INV .{\<acute>p2 \<and> \<acute>INIT}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   421
   DO .{\<acute>p2 \<and> \<acute>lj<length a \<and> \<acute>INIT}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   422
        WAIT \<acute>outs<\<acute>ins END;; 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   423
      .{\<acute>p2 \<and> \<acute>lj<length a \<and> \<acute>outs<\<acute>ins \<and> \<acute>INIT}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   424
       \<acute>vy:=(\<acute>buffer ! (\<acute>outs mod (length \<acute>buffer)));; 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   425
      .{\<acute>p2 \<and> \<acute>lj<length a \<and> \<acute>outs<\<acute>ins \<and> \<acute>vy=(a ! \<acute>lj) \<and> \<acute>INIT}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   426
       \<acute>outs:=\<acute>outs+1;;  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   427
      .{\<acute>I2 \<and> (\<acute>lj+1)=\<acute>outs \<and> \<acute>lj<length a \<and> \<acute>vy=(a ! \<acute>lj) \<and> \<acute>INIT}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   428
       \<acute>b:=(list_update \<acute>b \<acute>lj \<acute>vy);; 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   429
      .{\<acute>I2 \<and> (\<acute>lj+1)=\<acute>outs \<and> \<acute>lj<length a \<and> (a ! \<acute>lj)=(\<acute>b ! \<acute>lj) \<and> \<acute>INIT}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   430
       \<acute>lj:=\<acute>lj+1  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   431
   OD  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   432
  .{\<acute>p2 \<and> \<acute>lj=length a \<and> \<acute>INIT}.  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   433
 COEND  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   434
 .{ \<forall>k<length a. (a ! k)=(\<acute>b ! k)}."
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   435
apply oghoare
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   436
--{* 138 vc  *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   437
apply(tactic {* ALLGOALS Clarify_tac *})
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   438
--{* 112 subgoals left *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   439
apply(simp_all (no_asm))
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   440
apply(tactic {*ALLGOALS (conjI_Tac (K all_tac)) *})
13601
fd3e3d6b37b2 Adapted to new simplifier.
berghofe
parents: 13517
diff changeset
   441
--{* 930 subgoals left *}
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   442
apply(tactic {* ALLGOALS Clarify_tac *})
13601
fd3e3d6b37b2 Adapted to new simplifier.
berghofe
parents: 13517
diff changeset
   443
apply(simp_all (asm_lr) only:length_0_conv [THEN sym])
fd3e3d6b37b2 Adapted to new simplifier.
berghofe
parents: 13517
diff changeset
   444
--{* 44 subgoals left *}
fd3e3d6b37b2 Adapted to new simplifier.
berghofe
parents: 13517
diff changeset
   445
apply (simp_all (asm_lr) del:length_0_conv add: nth_list_update mod_less_divisor mod_lemma)
fd3e3d6b37b2 Adapted to new simplifier.
berghofe
parents: 13517
diff changeset
   446
--{* 33 subgoals left *}
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   447
apply(tactic {* ALLGOALS Clarify_tac *})
14757
556ce89b7d41 tactic call changed from TRYALL arith_tac to TRYALL simple_arith_tac preventing a call to presburger.
chaieb
parents: 13601
diff changeset
   448
556ce89b7d41 tactic call changed from TRYALL arith_tac to TRYALL simple_arith_tac preventing a call to presburger.
chaieb
parents: 13601
diff changeset
   449
ML "set Presburger.trace"
556ce89b7d41 tactic call changed from TRYALL arith_tac to TRYALL simple_arith_tac preventing a call to presburger.
chaieb
parents: 13601
diff changeset
   450
apply(tactic {* TRYALL simple_arith_tac *})
13601
fd3e3d6b37b2 Adapted to new simplifier.
berghofe
parents: 13517
diff changeset
   451
--{* 10 subgoals left *}
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   452
apply (force simp add:less_Suc_eq)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   453
apply(drule sym)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   454
apply (force simp add:less_Suc_eq)+
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   455
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   456
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   457
subsection {* Parameterized Examples *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   458
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   459
subsubsection {* Set Elements of an Array to Zero *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   460
13022
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
   461
record Example1 =
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   462
  a :: "nat \<Rightarrow> nat"
13022
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
   463
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
   464
lemma Example1: 
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   465
 "\<parallel>- .{True}.
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   466
   COBEGIN SCHEME [0\<le>i<n] .{True}. \<acute>a:=\<acute>a (i:=0) .{\<acute>a i=0}. COEND 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   467
  .{\<forall>i < n. \<acute>a i = 0}."
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   468
apply oghoare
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   469
apply simp_all
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   470
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   471
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   472
text {* Same example with lists as auxiliary variables. *}
13022
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
   473
record Example1_list =
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
   474
  A :: "nat list"
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
   475
lemma Example1_list: 
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
   476
 "\<parallel>- .{n < length \<acute>A}. 
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   477
   COBEGIN 
13022
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
   478
     SCHEME [0\<le>i<n] .{n < length \<acute>A}. \<acute>A:=\<acute>A[i:=0] .{\<acute>A!i=0}. 
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   479
   COEND 
13022
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
   480
    .{\<forall>i < n. \<acute>A!i = 0}."
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   481
apply oghoare
13187
e5434b822a96 Modifications due to enhanced linear arithmetic.
nipkow
parents: 13022
diff changeset
   482
apply force+
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   483
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   484
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   485
subsubsection {* Increment a Variable in Parallel *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   486
15561
045a07ac35a7 another reorganization of setsums and intervals
nipkow
parents: 15045
diff changeset
   487
declare setsum_op_ivl_Suc [simp]
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   488
15561
045a07ac35a7 another reorganization of setsums and intervals
nipkow
parents: 15045
diff changeset
   489
text {* First some lemmas about summation properties. *}
045a07ac35a7 another reorganization of setsums and intervals
nipkow
parents: 15045
diff changeset
   490
(*
15043
nipkow
parents: 15041
diff changeset
   491
lemma Example2_lemma1: "!!b. j<n \<Longrightarrow> (\<Sum>i::nat<n. b i) = (0::nat) \<Longrightarrow> b j = 0 "
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   492
apply(induct n)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   493
 apply simp_all
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   494
apply(force simp add: less_Suc_eq)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   495
done
15561
045a07ac35a7 another reorganization of setsums and intervals
nipkow
parents: 15045
diff changeset
   496
*)
13022
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
   497
lemma Example2_lemma2_aux: "!!b. j<n \<Longrightarrow> 
15561
045a07ac35a7 another reorganization of setsums and intervals
nipkow
parents: 15045
diff changeset
   498
 (\<Sum>i=0..<n. (b i::nat)) =
045a07ac35a7 another reorganization of setsums and intervals
nipkow
parents: 15045
diff changeset
   499
 (\<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
   500
apply(induct n)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   501
 apply simp_all
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   502
apply(simp add:less_Suc_eq)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   503
 apply(auto)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   504
apply(subgoal_tac "n - j = Suc(n- Suc j)")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   505
  apply simp
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   506
apply arith
13187
e5434b822a96 Modifications due to enhanced linear arithmetic.
nipkow
parents: 13022
diff changeset
   507
done
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   508
13022
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
   509
lemma Example2_lemma2_aux2: 
15561
045a07ac35a7 another reorganization of setsums and intervals
nipkow
parents: 15045
diff changeset
   510
  "!!b. j\<le> s \<Longrightarrow> (\<Sum>i::nat=0..<j. (b (s:=t)) i) = (\<Sum>i=0..<j. b i)"
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   511
apply(induct j)
15041
a6b1f0cef7b3 Got rid of Summation and made it a translation into setsum instead.
nipkow
parents: 14757
diff changeset
   512
 apply (simp_all cong:setsum_cong)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   513
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   514
13022
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
   515
lemma Example2_lemma2: 
15561
045a07ac35a7 another reorganization of setsums and intervals
nipkow
parents: 15045
diff changeset
   516
 "!!b. \<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)"
13022
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
   517
apply(frule_tac b="(b (j:=(Suc 0)))" in Example2_lemma2_aux)
15561
045a07ac35a7 another reorganization of setsums and intervals
nipkow
parents: 15045
diff changeset
   518
apply(erule_tac  t="setsum (b(j := (Suc 0))) {0..<n}" in ssubst)
13022
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
   519
apply(frule_tac b=b in Example2_lemma2_aux)
15561
045a07ac35a7 another reorganization of setsums and intervals
nipkow
parents: 15045
diff changeset
   520
apply(erule_tac  t="setsum b {0..<n}" in ssubst)
045a07ac35a7 another reorganization of setsums and intervals
nipkow
parents: 15045
diff changeset
   521
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)))")
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   522
apply(rotate_tac -1)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   523
apply(erule ssubst)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   524
apply(subgoal_tac "j\<le>j")
13022
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
   525
 apply(drule_tac b="b" and t="(Suc 0)" in Example2_lemma2_aux2)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   526
apply(rotate_tac -1)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   527
apply(erule ssubst)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   528
apply simp_all
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   529
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   530
15561
045a07ac35a7 another reorganization of setsums and intervals
nipkow
parents: 15045
diff changeset
   531
lemma Example2_lemma3: "!!b. \<forall>i< n. b i = (Suc 0) \<Longrightarrow> (\<Sum>i=0..<n. b i)= n"
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   532
apply (induct n)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   533
apply auto
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   534
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   535
13022
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
   536
record Example2 = 
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   537
 c :: "nat \<Rightarrow> nat" 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   538
 x :: nat
13022
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
   539
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
   540
lemma Example_2: "0<n \<Longrightarrow> 
15561
045a07ac35a7 another reorganization of setsums and intervals
nipkow
parents: 15045
diff changeset
   541
 \<parallel>- .{\<acute>x=0 \<and> (\<Sum>i=0..<n. \<acute>c i)=0}.  
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   542
 COBEGIN 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   543
   SCHEME [0\<le>i<n] 
15561
045a07ac35a7 another reorganization of setsums and intervals
nipkow
parents: 15045
diff changeset
   544
  .{\<acute>x=(\<Sum>i=0..<n. \<acute>c i) \<and> \<acute>c i=0}. 
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   545
   \<langle> \<acute>x:=\<acute>x+(Suc 0),, \<acute>c:=\<acute>c (i:=(Suc 0)) \<rangle>
15561
045a07ac35a7 another reorganization of setsums and intervals
nipkow
parents: 15045
diff changeset
   546
  .{\<acute>x=(\<Sum>i=0..<n. \<acute>c i) \<and> \<acute>c i=(Suc 0)}.
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   547
 COEND 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   548
 .{\<acute>x=n}."
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   549
apply oghoare
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   550
apply simp_all
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   551
apply (tactic {* ALLGOALS Clarify_tac *})
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   552
apply simp_all
13022
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
   553
   apply(erule Example2_lemma2)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   554
   apply simp
13022
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
   555
  apply(erule Example2_lemma2)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   556
  apply simp
13022
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
   557
 apply(erule Example2_lemma2)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   558
 apply simp
13022
b115b305612f New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
prensani
parents: 13020
diff changeset
   559
apply(force intro: Example2_lemma3)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   560
done
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
   561
13187
e5434b822a96 Modifications due to enhanced linear arithmetic.
nipkow
parents: 13022
diff changeset
   562
end