1 (* ------------------------------------------------------------------------- *)
3 (* ------------------------------------------------------------------------- *)
7 let move = new_definition
8 `move ((ax,ay),(bx,by),(cx,cy)) ((ax',ay'),(bx',by'),(cx',cy')) <=>
9 (?a. ax' = ax + a * (cx - bx) /\ ay' = ay + a * (cy - by) /\
10 bx' = bx /\ by' = by /\ cx' = cx /\ cy' = cy) \/
11 (?b. bx' = bx + b * (ax - cx) /\ by' = by + b * (ay - cy) /\
12 ax' = ax /\ ay' = ay /\ cx' = cx /\ cy' = cy) \/
13 (?c. ax' = ax /\ ay' = ay /\ bx' = bx /\ by' = by /\
14 cx' = cx + c * (bx - ax) /\ cy' = cy + c * (by - ay))`;;
16 let reachable_RULES,reachable_INDUCT,reachable_CASES =
17 new_inductive_definition
18 `(!p. reachable p p) /\
19 (!p q r. move p q /\ reachable q r ==> reachable p r)`;;
21 let oriented_area = new_definition
22 `oriented_area ((ax,ay),(bx,by),(cx,cy)) =
23 ((bx - ax) * (cy - ay) - (cx - ax) * (by - ay)) / &2`;;
25 let MOVE_INVARIANT = prove
26 (`!p p'. move p p' ==> oriented_area p = oriented_area p'`,
27 REWRITE_TAC[FORALL_PAIR_THM; move; oriented_area] THEN CONV_TAC REAL_RING);;
29 let REACHABLE_INVARIANT = prove
30 (`!p p'. reachable p p' ==> oriented_area p = oriented_area p'`,
31 MATCH_MP_TAC reachable_INDUCT THEN MESON_TAC[MOVE_INVARIANT]);;
33 let IMPOSSIBILITY_B = prove
34 (`~(reachable ((&0,&0),(&3,&0),(&0,&3)) ((&1,&2),(&2,&5),(-- &2,&3)) \/
35 reachable ((&0,&0),(&3,&0),(&0,&3)) ((&1,&2),(-- &2,&3),(&2,&5)) \/
36 reachable ((&0,&0),(&3,&0),(&0,&3)) ((&2,&5),(&1,&2),(-- &2,&3)) \/
37 reachable ((&0,&0),(&3,&0),(&0,&3)) ((&2,&5),(-- &2,&3),(&1,&2)) \/
38 reachable ((&0,&0),(&3,&0),(&0,&3)) ((-- &2,&3),(&1,&2),(&2,&5)) \/
39 reachable ((&0,&0),(&3,&0),(&0,&3)) ((-- &2,&3),(&2,&5),(&1,&2)))`,
40 STRIP_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP REACHABLE_INVARIANT) THEN
41 REWRITE_TAC[oriented_area] THEN REAL_ARITH_TAC);;
43 (* ------------------------------------------------------------------------- *)
44 (* Verification of a simple concurrent program. *)
45 (* ------------------------------------------------------------------------- *)
47 let init = new_definition
48 `init (x,y,pc1,pc2,sem) <=>
49 pc1 = 10 /\ pc2 = 10 /\ x = 0 /\ y = 0 /\ sem = 1`;;
51 let trans = new_definition
52 `trans (x,y,pc1,pc2,sem) (x',y',pc1',pc2',sem') <=>
53 pc1 = 10 /\ sem > 0 /\ pc1' = 20 /\ sem' = sem - 1 /\
54 (x',y',pc2') = (x,y,pc2) \/
55 pc2 = 10 /\ sem > 0 /\ pc2' = 20 /\ sem' = sem - 1 /\
56 (x',y',pc1') = (x,y,pc1) \/
57 pc1 = 20 /\ pc1' = 30 /\ x' = x + 1 /\
58 (y',pc2',sem') = (y,pc2,sem) \/
59 pc2 = 20 /\ pc2' = 30 /\ y' = y + 1 /\ x' = x /\
60 pc1' = pc1 /\ sem' = sem \/
61 pc1 = 30 /\ pc1' = 10 /\ sem' = sem + 1 /\
62 (x',y',pc2') = (x,y,pc2) \/
63 pc2 = 30 /\ pc2' = 10 /\ sem' = sem + 1 /\
64 (x',y',pc1') = (x,y,pc1)`;;
66 let mutex = new_definition
67 `mutex (x,y,pc1,pc2,sem) <=> pc1 = 10 \/ pc2 = 10`;;
69 let indinv = new_definition
70 `indinv (x:num,y:num,pc1,pc2,sem) <=>
71 sem + (if pc1 = 10 then 0 else 1) + (if pc2 = 10 then 0 else 1) = 1`;;
73 needs "Library/rstc.ml";;
75 let INDUCTIVE_INVARIANT = prove
76 (`!init invariant transition P.
77 (!s. init s ==> invariant s) /\
78 (!s s'. invariant s /\ transition s s' ==> invariant s') /\
79 (!s. invariant s ==> P s)
80 ==> !s s':A. init s /\ RTC transition s s' ==> P s'`,
81 REPEAT GEN_TAC THEN MP_TAC(ISPECL
82 [`transition:A->A->bool`;
83 `\s s':A. invariant s ==> invariant s'`] RTC_INDUCT) THEN
87 (`!s s'. init s /\ RTC trans s s' ==> mutex s'`,
88 MATCH_MP_TAC INDUCTIVE_INVARIANT THEN EXISTS_TAC `indinv` THEN
89 REWRITE_TAC[init; trans; indinv; mutex; FORALL_PAIR_THM; PAIR_EQ] THEN