diff -r 07593a0a27f4 -r effd8fcabca2 src/HOL/Hoare_Parallel/OG_Examples.thy --- a/src/HOL/Hoare_Parallel/OG_Examples.thy Tue Aug 27 23:54:23 2013 +0200 +++ b/src/HOL/Hoare_Parallel/OG_Examples.thy Wed Aug 28 00:18:50 2013 +0200 @@ -16,30 +16,30 @@ hold :: nat lemma Petersons_mutex_1: - "\- .{\pr1=0 \ \\in1 \ \pr2=0 \ \\in2 }. - COBEGIN .{\pr1=0 \ \\in1}. - WHILE True INV .{\pr1=0 \ \\in1}. + "\- \\pr1=0 \ \\in1 \ \pr2=0 \ \\in2 \ + COBEGIN \\pr1=0 \ \\in1\ + WHILE True INV \\pr1=0 \ \\in1\ DO - .{\pr1=0 \ \\in1}. \ \in1:=True,,\pr1:=1 \;; - .{\pr1=1 \ \in1}. \ \hold:=1,,\pr1:=2 \;; - .{\pr1=2 \ \in1 \ (\hold=1 \ \hold=2 \ \pr2=2)}. + \\pr1=0 \ \\in1\ \ \in1:=True,,\pr1:=1 \;; + \\pr1=1 \ \in1\ \ \hold:=1,,\pr1:=2 \;; + \\pr1=2 \ \in1 \ (\hold=1 \ \hold=2 \ \pr2=2)\ AWAIT (\\in2 \ \(\hold=1)) THEN \pr1:=3 END;; - .{\pr1=3 \ \in1 \ (\hold=1 \ \hold=2 \ \pr2=2)}. + \\pr1=3 \ \in1 \ (\hold=1 \ \hold=2 \ \pr2=2)\ \\in1:=False,,\pr1:=0\ - OD .{\pr1=0 \ \\in1}. + OD \\pr1=0 \ \\in1\ \ - .{\pr2=0 \ \\in2}. - WHILE True INV .{\pr2=0 \ \\in2}. + \\pr2=0 \ \\in2\ + WHILE True INV \\pr2=0 \ \\in2\ DO - .{\pr2=0 \ \\in2}. \ \in2:=True,,\pr2:=1 \;; - .{\pr2=1 \ \in2}. \ \hold:=2,,\pr2:=2 \;; - .{\pr2=2 \ \in2 \ (\hold=2 \ (\hold=1 \ \pr1=2))}. + \\pr2=0 \ \\in2\ \ \in2:=True,,\pr2:=1 \;; + \\pr2=1 \ \in2\ \ \hold:=2,,\pr2:=2 \;; + \\pr2=2 \ \in2 \ (\hold=2 \ (\hold=1 \ \pr1=2))\ AWAIT (\\in1 \ \(\hold=2)) THEN \pr2:=3 END;; - .{\pr2=3 \ \in2 \ (\hold=2 \ (\hold=1 \ \pr1=2))}. + \\pr2=3 \ \in2 \ (\hold=2 \ (\hold=1 \ \pr1=2))\ \\in2:=False,,\pr2:=0\ - OD .{\pr2=0 \ \\in2}. + OD \\pr2=0 \ \\in2\ COEND - .{\pr1=0 \ \\in1 \ \pr2=0 \ \\in2}." + \\pr1=0 \ \\in1 \ \pr2=0 \ \\in2\" apply oghoare --{* 104 verification conditions. *} apply auto @@ -57,37 +57,37 @@ after2 :: bool lemma Busy_wait_mutex: - "\- .{True}. + "\- \True\ \flag1:=False,, \flag2:=False,, - COBEGIN .{\\flag1}. + COBEGIN \\\flag1\ WHILE True - INV .{\\flag1}. - DO .{\\flag1}. \ \flag1:=True,,\after1:=False \;; - .{\flag1 \ \\after1}. \ \turn:=1,,\after1:=True \;; - .{\flag1 \ \after1 \ (\turn=1 \ \turn=2)}. + INV \\\flag1\ + DO \\\flag1\ \ \flag1:=True,,\after1:=False \;; + \\flag1 \ \\after1\ \ \turn:=1,,\after1:=True \;; + \\flag1 \ \after1 \ (\turn=1 \ \turn=2)\ WHILE \(\flag2 \ \turn=2) - INV .{\flag1 \ \after1 \ (\turn=1 \ \turn=2)}. - DO .{\flag1 \ \after1 \ (\turn=1 \ \turn=2)}. SKIP OD;; - .{\flag1 \ \after1 \ (\flag2 \ \after2 \ \turn=2)}. + INV \\flag1 \ \after1 \ (\turn=1 \ \turn=2)\ + DO \\flag1 \ \after1 \ (\turn=1 \ \turn=2)\ SKIP OD;; + \\flag1 \ \after1 \ (\flag2 \ \after2 \ \turn=2)\ \flag1:=False OD - .{False}. + \False\ \ - .{\\flag2}. + \\\flag2\ WHILE True - INV .{\\flag2}. - DO .{\\flag2}. \ \flag2:=True,,\after2:=False \;; - .{\flag2 \ \\after2}. \ \turn:=2,,\after2:=True \;; - .{\flag2 \ \after2 \ (\turn=1 \ \turn=2)}. + INV \\\flag2\ + DO \\\flag2\ \ \flag2:=True,,\after2:=False \;; + \\flag2 \ \\after2\ \ \turn:=2,,\after2:=True \;; + \\flag2 \ \after2 \ (\turn=1 \ \turn=2)\ WHILE \(\flag1 \ \turn=1) - INV .{\flag2 \ \after2 \ (\turn=1 \ \turn=2)}. - DO .{\flag2 \ \after2 \ (\turn=1 \ \turn=2)}. SKIP OD;; - .{\flag2 \ \after2 \ (\flag1 \ \after1 \ \turn=1)}. + INV \\flag2 \ \after2 \ (\turn=1 \ \turn=2)\ + DO \\flag2 \ \after2 \ (\turn=1 \ \turn=2)\ SKIP OD;; + \\flag2 \ \after2 \ (\flag1 \ \after1 \ \turn=1)\ \flag2:=False OD - .{False}. + \False\ COEND - .{False}." + \False\" apply oghoare --{* 122 vc *} apply auto @@ -100,21 +100,21 @@ who :: nat lemma Semaphores_mutex: - "\- .{i\j}. + "\- \i\j\ \out:=True ,, - COBEGIN .{i\j}. - WHILE True INV .{i\j}. - DO .{i\j}. AWAIT \out THEN \out:=False,, \who:=i END;; - .{\\out \ \who=i \ i\j}. \out:=True OD - .{False}. + COBEGIN \i\j\ + WHILE True INV \i\j\ + DO \i\j\ AWAIT \out THEN \out:=False,, \who:=i END;; + \\\out \ \who=i \ i\j\ \out:=True OD + \False\ \ - .{i\j}. - WHILE True INV .{i\j}. - DO .{i\j}. AWAIT \out THEN \out:=False,,\who:=j END;; - .{\\out \ \who=j \ i\j}. \out:=True OD - .{False}. + \i\j\ + WHILE True INV \i\j\ + DO \i\j\ AWAIT \out THEN \out:=False,,\who:=j END;; + \\\out \ \who=j \ i\j\ \out:=True OD + \False\ COEND - .{False}." + \False\" apply oghoare --{* 38 vc *} apply auto @@ -123,17 +123,17 @@ subsubsection {* Peterson's Algorithm III: Parameterized version: *} lemma Semaphores_parameterized_mutex: - "0 \- .{True}. + "0 \- \True\ \out:=True ,, COBEGIN SCHEME [0\ i< n] - .{True}. - WHILE True INV .{True}. - DO .{True}. AWAIT \out THEN \out:=False,, \who:=i END;; - .{\\out \ \who=i}. \out:=True OD - .{False}. + \True\ + WHILE True INV \True\ + DO \True\ AWAIT \out THEN \out:=False,, \who:=i END;; + \\\out \ \who=i\ \out:=True OD + \False\ COEND - .{False}." + \False\" apply oghoare --{* 20 vc *} apply auto @@ -150,22 +150,22 @@ lemma Ticket_mutex: "\ 0n=length \turn \ 0<\nextv \ (\k l. k l k\l \ \turn!k < \num \ (\turn!k =0 \ \turn!k\\turn!l))\ \ - \ \- .{n=length \turn}. + \ \- \n=length \turn\ \index:= 0,, - WHILE \index < n INV .{n=length \turn \ (\i<\index. \turn!i=0)}. + WHILE \index < n INV \n=length \turn \ (\i<\index. \turn!i=0)\ DO \turn:= \turn[\index:=0],, \index:=\index +1 OD,, \num:=1 ,, \nextv:=1 ,, COBEGIN SCHEME [0\ i< n] - .{\I}. - WHILE True INV .{\I}. - DO .{\I}. \ \turn :=\turn[i:=\num],, \num:=\num+1 \;; - .{\I}. WAIT \turn!i=\nextv END;; - .{\I \ \turn!i=\nextv}. \nextv:=\nextv+1 + \\I\ + WHILE True INV \\I\ + DO \\I\ \ \turn :=\turn[i:=\num],, \num:=\num+1 \;; + \\I\ WAIT \turn!i=\nextv END;; + \\I \ \turn!i=\nextv\ \nextv:=\nextv+1 OD - .{False}. + \False\ COEND - .{False}." + \False\" apply oghoare --{* 35 vc *} apply simp_all @@ -259,40 +259,40 @@ \ (\\found \ a<\ x \ f(\x)\0) \ ; I2= \\y\a+1 \ (\found \ (a<\x \ f(\x)=0) \ (\y\a \ f(\y)=0)) \ (\\found \ \y\a \ f(\y)\0) \ \ \ - \- .{\ u. f(u)=0}. + \- \\ u. f(u)=0\ \turn:=1,, \found:= False,, \x:=a,, \y:=a+1 ,, - COBEGIN .{\I1}. + COBEGIN \\I1\ WHILE \\found - INV .{\I1}. - DO .{a\\x \ (\found \ \y\a \ f(\y)=0) \ (a<\x \ f(\x)\0)}. + INV \\I1\ + DO \a\\x \ (\found \ \y\a \ f(\y)=0) \ (a<\x \ f(\x)\0)\ WAIT \turn=1 END;; - .{a\\x \ (\found \ \y\a \ f(\y)=0) \ (a<\x \ f(\x)\0)}. + \a\\x \ (\found \ \y\a \ f(\y)=0) \ (a<\x \ f(\x)\0)\ \turn:=2;; - .{a\\x \ (\found \ \y\a \ f(\y)=0) \ (a<\x \ f(\x)\0)}. + \a\\x \ (\found \ \y\a \ f(\y)=0) \ (a<\x \ f(\x)\0)\ \ \x:=\x+1,, IF f(\x)=0 THEN \found:=True ELSE SKIP FI\ OD;; - .{\I1 \ \found}. + \\I1 \ \found\ \turn:=2 - .{\I1 \ \found}. + \\I1 \ \found\ \ - .{\I2}. + \\I2\ WHILE \\found - INV .{\I2}. - DO .{\y\a+1 \ (\found \ a<\x \ f(\x)=0) \ (\y\a \ f(\y)\0)}. + INV \\I2\ + DO \\y\a+1 \ (\found \ a<\x \ f(\x)=0) \ (\y\a \ f(\y)\0)\ WAIT \turn=2 END;; - .{\y\a+1 \ (\found \ a<\x \ f(\x)=0) \ (\y\a \ f(\y)\0)}. + \\y\a+1 \ (\found \ a<\x \ f(\x)=0) \ (\y\a \ f(\y)\0)\ \turn:=1;; - .{\y\a+1 \ (\found \ a<\x \ f(\x)=0) \ (\y\a \ f(\y)\0)}. + \\y\a+1 \ (\found \ a<\x \ f(\x)=0) \ (\y\a \ f(\y)\0)\ \ \y:=(\y - 1),, IF f(\y)=0 THEN \found:=True ELSE SKIP FI\ OD;; - .{\I2 \ \found}. + \\I2 \ \found\ \turn:=1 - .{\I2 \ \found}. + \\I2 \ \found\ COEND - .{f(\x)=0 \ f(\y)=0}." + \f(\x)=0 \ f(\y)=0\" apply oghoare --{* 98 verification conditions *} apply auto @@ -306,26 +306,26 @@ \ (\\found \ a<\x \ f(\x)\0)\; I2= \\y\a+1 \ (\found \ (a<\x \ f(\x)=0) \ (\y\a \ f(\y)=0)) \ (\\found \ \y\a \ f(\y)\0)\\ \ - \- .{\u. f(u)=0}. + \- \\u. f(u)=0\ \found:= False,, \x:=a,, \y:=a+1,, - COBEGIN .{\I1}. + COBEGIN \\I1\ WHILE \\found - INV .{\I1}. - DO .{a\\x \ (\found \ \y\a \ f(\y)=0) \ (a<\x \ f(\x)\0)}. + INV \\I1\ + DO \a\\x \ (\found \ \y\a \ f(\y)=0) \ (a<\x \ f(\x)\0)\ \ \x:=\x+1,,IF f(\x)=0 THEN \found:=True ELSE SKIP FI\ OD - .{\I1 \ \found}. + \\I1 \ \found\ \ - .{\I2}. + \\I2\ WHILE \\found - INV .{\I2}. - DO .{\y\a+1 \ (\found \ a<\x \ f(\x)=0) \ (\y\a \ f(\y)\0)}. + INV \\I2\ + DO \\y\a+1 \ (\found \ a<\x \ f(\x)=0) \ (\y\a \ f(\y)\0)\ \ \y:=(\y - 1),,IF f(\y)=0 THEN \found:=True ELSE SKIP FI\ OD - .{\I2 \ \found}. + \\I2 \ \found\ COEND - .{f(\x)=0 \ f(\y)=0}." + \f(\x)=0 \ f(\y)=0\" apply oghoare --{* 20 vc *} apply auto @@ -390,44 +390,44 @@ p1= \\I1 \ \li=\ins\ ; I2 = \\I \ (\k<\lj. (a ! k)=(\b ! k)) \ \lj\length a\ ; p2 = \\I2 \ \lj=\outs\ \ \ - \- .{\INIT}. + \- \\INIT\ \ins:=0,, \outs:=0,, \li:=0,, \lj:=0,, - COBEGIN .{\p1 \ \INIT}. + COBEGIN \\p1 \ \INIT\ WHILE \li p1 \ \INIT}. - DO .{\p1 \ \INIT \ \li\p1 \ \INIT\ + DO \\p1 \ \INIT \ \li \vx:= (a ! \li);; - .{\p1 \ \INIT \ \li \vx=(a ! \li)}. + \\p1 \ \INIT \ \li \vx=(a ! \li)\ WAIT \ins-\outs < length \buffer END;; - .{\p1 \ \INIT \ \li \vx=(a ! \li) - \ \ins-\outs < length \buffer}. + \\p1 \ \INIT \ \li \vx=(a ! \li) + \ \ins-\outs < length \buffer\ \buffer:=(list_update \buffer (\ins mod (length \buffer)) \vx);; - .{\p1 \ \INIT \ \li\p1 \ \INIT \ \li (a ! \li)=(\buffer ! (\ins mod (length \buffer))) - \ \ins-\outs buffer}. + \ \ins-\outs buffer\ \ins:=\ins+1;; - .{\I1 \ \INIT \ (\li+1)=\ins \ \li\I1 \ \INIT \ (\li+1)=\ins \ \li \li:=\li+1 OD - .{\p1 \ \INIT \ \li=length a}. + \\p1 \ \INIT \ \li=length a\ \ - .{\p2 \ \INIT}. + \\p2 \ \INIT\ WHILE \lj < length a - INV .{\p2 \ \INIT}. - DO .{\p2 \ \lj \INIT}. + INV \\p2 \ \INIT\ + DO \\p2 \ \lj \INIT\ WAIT \outs<\ins END;; - .{\p2 \ \lj \outs<\ins \ \INIT}. + \\p2 \ \lj \outs<\ins \ \INIT\ \vy:=(\buffer ! (\outs mod (length \buffer)));; - .{\p2 \ \lj \outs<\ins \ \vy=(a ! \lj) \ \INIT}. + \\p2 \ \lj \outs<\ins \ \vy=(a ! \lj) \ \INIT\ \outs:=\outs+1;; - .{\I2 \ (\lj+1)=\outs \ \lj \vy=(a ! \lj) \ \INIT}. + \\I2 \ (\lj+1)=\outs \ \lj \vy=(a ! \lj) \ \INIT\ \b:=(list_update \b \lj \vy);; - .{\I2 \ (\lj+1)=\outs \ \lj (a ! \lj)=(\b ! \lj) \ \INIT}. + \\I2 \ (\lj+1)=\outs \ \lj (a ! \lj)=(\b ! \lj) \ \INIT\ \lj:=\lj+1 OD - .{\p2 \ \lj=length a \ \INIT}. + \\p2 \ \lj=length a \ \INIT\ COEND - .{ \kb ! k)}." + \ \kb ! k)\" apply oghoare --{* 138 vc *} apply(tactic {* ALLGOALS (clarify_tac @{context}) *}) @@ -455,9 +455,9 @@ a :: "nat \ nat" lemma Example1: - "\- .{True}. - COBEGIN SCHEME [0\ia:=\a (i:=0) .{\a i=0}. COEND - .{\i < n. \a i = 0}." + "\- \True\ + COBEGIN SCHEME [0\iTrue\ \a:=\a (i:=0) \\a i=0\ COEND + \\i < n. \a i = 0\" apply oghoare apply simp_all done @@ -466,11 +466,11 @@ record Example1_list = A :: "nat list" lemma Example1_list: - "\- .{n < length \A}. + "\- \n < length \A\ COBEGIN - SCHEME [0\iA}. \A:=\A[i:=0] .{\A!i=0}. + SCHEME [0\in < length \A\ \A:=\A[i:=0] \\A!i=0\ COEND - .{\i < n. \A!i = 0}." + \\i < n. \A!i = 0\" apply oghoare apply force+ done @@ -525,14 +525,14 @@ x :: nat lemma Example_2: "0 - \- .{\x=0 \ (\i=0..c i)=0}. + \- \\x=0 \ (\i=0..c i)=0\ COBEGIN SCHEME [0\ix=(\i=0..c i) \ \c i=0}. + \\x=(\i=0..c i) \ \c i=0\ \ \x:=\x+(Suc 0),, \c:=\c (i:=(Suc 0)) \ - .{\x=(\i=0..c i) \ \c i=(Suc 0)}. + \\x=(\i=0..c i) \ \c i=(Suc 0)\ COEND - .{\x=n}." + \\x=n\" apply oghoare apply (simp_all cong del: strong_setsum_cong) apply (tactic {* ALLGOALS (clarify_tac @{context}) *})