Update from HH
[hl193./.git] / Tutorial / Inductive_definitions.ml
1 (* ------------------------------------------------------------------------- *)
2 (* Bug puzzle.                                                               *)
3 (* ------------------------------------------------------------------------- *)
4
5 prioritize_real();;
6
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))`;;
15
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)`;;
20
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`;;
24
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);;
28
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]);;
32
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);;
42
43 (* ------------------------------------------------------------------------- *)
44 (* Verification of a simple concurrent program.                              *)
45 (* ------------------------------------------------------------------------- *)
46
47 let init = new_definition
48  `init (x,y,pc1,pc2,sem) <=>
49         pc1 = 10 /\ pc2 = 10 /\ x = 0 /\ y = 0 /\ sem = 1`;;
50
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)`;;
65
66 let mutex = new_definition
67  `mutex (x,y,pc1,pc2,sem) <=> pc1 = 10 \/ pc2 = 10`;;
68
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`;;
72
73 needs "Library/rstc.ml";;
74
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
84   MESON_TAC[]);;
85
86 let MUTEX = prove
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
90   ARITH_TAC);;