1.1 --- a/src/HOL/UNITY/Lift.thy Thu Aug 20 16:58:28 1998 +0200
1.2 +++ b/src/HOL/UNITY/Lift.thy Thu Aug 20 17:43:01 1998 +0200
1.3 @@ -19,25 +19,26 @@
1.4 move :: bool (*whether moving takes precedence over opening*)
1.5
1.6 consts
1.7 - min, max :: nat (*least and greatest floors*)
1.8 + Min, Max :: nat (*least and greatest floors*)
1.9
1.10 rules
1.11 - min_le_max "min <= max"
1.12 + Min_le_Max "Min <= Max"
1.13
1.14 (** Linear arithmetic: justified by a separate call to arith_oracle_tac **)
1.15 arith1 "m < fl ==> n - Suc fl < fl - m + (n - m)"
1.16 - arith2 "[| Suc fl < n; m < n |] ==> n - Suc fl < fl - m + (n - m)"
1.17 -
1.18 + arith2 "[| m<n; m <= fl |] ==> n - Suc fl < fl - m + (n - m)"
1.19 + arith3 "[| Suc ix < m |] ==> ix - n < m - Suc ix + (m - n)"
1.20 + arith4 "[| ix < m; n < ix |] ==> ix - n < m - Suc (ix) + (m - n)"
1.21
1.22 constdefs
1.23
1.24 (** Abbreviations: the "always" part **)
1.25
1.26 above :: state set
1.27 - "above == {s. EX i. floor s < i & i <= max & i : req s}"
1.28 + "above == {s. EX i. floor s < i & i <= Max & i : req s}"
1.29
1.30 below :: state set
1.31 - "below == {s. EX i. min <= i & i < floor s & i : req s}"
1.32 + "below == {s. EX i. Min <= i & i < floor s & i : req s}"
1.33
1.34 queueing :: state set
1.35 "queueing == above Un below"
1.36 @@ -91,15 +92,15 @@
1.37 close_act :: "(state*state) set"
1.38 "close_act == {(s,s'). s' = s (|open := False|) & open s}"
1.39
1.40 - req_up_act :: "(state*state) set"
1.41 - "req_up_act ==
1.42 + req_up :: "(state*state) set"
1.43 + "req_up ==
1.44 {(s,s'). s' = s (|stop :=False,
1.45 floor := Suc (floor s),
1.46 up := True|)
1.47 & s : (ready Int goingup)}"
1.48
1.49 - req_down_act :: "(state*state) set"
1.50 - "req_down_act ==
1.51 + req_down :: "(state*state) set"
1.52 + "req_down ==
1.53 {(s,s'). s' = s (|stop :=False,
1.54 floor := floor s - 1,
1.55 up := False|)
1.56 @@ -115,17 +116,24 @@
1.57 {(s,s'). s' = s (|floor := floor s - 1|)
1.58 & ~ stop s & ~ up s & floor s ~: req s}"
1.59
1.60 + button_press :: "(state*state) set"
1.61 + "button_press ==
1.62 + {(s,s'). EX n. s' = s (|req := insert n (req s)|)
1.63 + & Min <= n & n <= Max}"
1.64 +
1.65 +
1.66 Lprg :: state program
1.67 - "Lprg == (|Init = {s. floor s = min & ~ up s & move s & stop s &
1.68 + (*for the moment, we OMIT button_press*)
1.69 + "Lprg == (|Init = {s. floor s = Min & ~ up s & move s & stop s &
1.70 ~ open s & req s = {}},
1.71 Acts = {id, request_act, open_act, close_act,
1.72 - req_up_act, req_down_act, move_up, move_down}|)"
1.73 + req_up, req_down, move_up, move_down}|)"
1.74
1.75
1.76 (** Invariants **)
1.77
1.78 bounded :: state set
1.79 - "bounded == {s. min <= floor s & floor s <= max}"
1.80 + "bounded == {s. Min <= floor s & floor s <= Max}"
1.81
1.82 open_stop :: state set
1.83 "open_stop == {s. open s --> stop s}"
1.84 @@ -138,25 +146,26 @@
1.85
1.86 moving_up :: state set
1.87 "moving_up == {s. ~ stop s & up s -->
1.88 - (EX f. floor s <= f & f <= max & f : req s)}"
1.89 + (EX f. floor s <= f & f <= Max & f : req s)}"
1.90
1.91 moving_down :: state set
1.92 "moving_down == {s. ~ stop s & ~ up s -->
1.93 - (EX f. min <= f & f <= floor s & f : req s)}"
1.94 + (EX f. Min <= f & f <= floor s & f : req s)}"
1.95
1.96 metric :: [nat,state] => nat
1.97 - "metric n s == if up s & floor s < n then n - floor s
1.98 - else if ~ up s & n < floor s then floor s - n
1.99 - else if up s & n < floor s then (max - floor s) + (max-n)
1.100 - else if ~ up s & floor s < n then (floor s - min) + (n-min)
1.101 - else 0"
1.102 + "metric ==
1.103 + %n s. if up s & floor s < n then n - floor s
1.104 + else if ~ up s & n < floor s then floor s - n
1.105 + else if up s & n < floor s then (Max - floor s) + (Max-n)
1.106 + else if ~ up s & floor s < n then (floor s - Min) + (n-Min)
1.107 + else 0"
1.108
1.109 locale floor =
1.110 fixes
1.111 n :: nat
1.112 assumes
1.113 - min_le_n "min <= n"
1.114 - n_le_max "n <= max"
1.115 + Min_le_n "Min <= n"
1.116 + n_le_Max "n <= Max"
1.117 defines
1.118
1.119 end