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);;