author  paulson 
Sat, 08 Feb 2003 16:05:33 +0100  
changeset 13812  91713a1915ee 
parent 13806  fd40c9d9076b 
child 14378  69c4d5997669 
permissions  rwrr 
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

1 
(* Title: HOL/UNITY/Lift.thy 
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

2 
ID: $Id$ 
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

4 
Copyright 1998 University of Cambridge 
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

5 

65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

6 
The LiftControl Example 
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

7 
*) 
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

8 

13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

9 
theory Lift = UNITY_Main: 
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

10 

65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

11 
record state = 
13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

12 
floor :: "int" (*current position of the lift*) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

13 
"open" :: "bool" (*whether the door is opened at floor*) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

14 
stop :: "bool" (*whether the lift is stopped at floor*) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

15 
req :: "int set" (*for each floor, whether the lift is requested*) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

16 
up :: "bool" (*current direction of movement*) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

17 
move :: "bool" (*whether moving takes precedence over opening*) 
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

18 

65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

19 
consts 
13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

20 
Min :: "int" (*least and greatest floors*) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

21 
Max :: "int" (*least and greatest floors*) 
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

22 

13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

23 
axioms 
13806  24 
Min_le_Max [iff]: "Min \<le> Max" 
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

25 

65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

26 
constdefs 
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

27 

65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

28 
(** Abbreviations: the "always" part **) 
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

29 

13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

30 
above :: "state set" 
13806  31 
"above == {s. \<exists>i. floor s < i & i \<le> Max & i \<in> req s}" 
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

32 

13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

33 
below :: "state set" 
13806  34 
"below == {s. \<exists>i. Min \<le> i & i < floor s & i \<in> req s}" 
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

35 

13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

36 
queueing :: "state set" 
13806  37 
"queueing == above \<union> below" 
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

38 

13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

39 
goingup :: "state set" 
13806  40 
"goingup == above \<inter> ({s. up s} \<union> below)" 
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

41 

13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

42 
goingdown :: "state set" 
13806  43 
"goingdown == below \<inter> ({s. ~ up s} \<union> above)" 
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

44 

13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

45 
ready :: "state set" 
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

46 
"ready == {s. stop s & ~ open s & move s}" 
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

47 

65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

48 
(** Further abbreviations **) 
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

49 

13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

50 
moving :: "state set" 
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

51 
"moving == {s. ~ stop s & ~ open s}" 
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

52 

13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

53 
stopped :: "state set" 
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

54 
"stopped == {s. stop s & ~ open s & ~ move s}" 
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

55 

13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

56 
opened :: "state set" 
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

57 
"opened == {s. stop s & open s & move s}" 
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

58 

13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

59 
closed :: "state set" (*but this is the same as ready!!*) 
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

60 
"closed == {s. stop s & ~ open s & move s}" 
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

61 

13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

62 
atFloor :: "int => state set" 
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

63 
"atFloor n == {s. floor s = n}" 
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

64 

13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

65 
Req :: "int => state set" 
13806  66 
"Req n == {s. n \<in> req s}" 
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

67 

65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

68 

65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

69 

65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

70 
(** The program **) 
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

71 

65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

72 
request_act :: "(state*state) set" 
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

73 
"request_act == {(s,s'). s' = s (stop:=True, move:=False) 
13806  74 
& ~ stop s & floor s \<in> req s}" 
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

75 

65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

76 
open_act :: "(state*state) set" 
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

77 
"open_act == 
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

78 
{(s,s'). s' = s (open :=True, 
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

79 
req := req s  {floor s}, 
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

80 
move := True) 
13806  81 
& stop s & ~ open s & floor s \<in> req s 
82 
& ~(move s & s \<in> queueing)}" 

11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

83 

65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

84 
close_act :: "(state*state) set" 
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

85 
"close_act == {(s,s'). s' = s (open := False) & open s}" 
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

86 

65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

87 
req_up :: "(state*state) set" 
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

88 
"req_up == 
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

89 
{(s,s'). s' = s (stop :=False, 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

90 
floor := floor s + 1, 
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

91 
up := True) 
13806  92 
& s \<in> (ready \<inter> goingup)}" 
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

93 

65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

94 
req_down :: "(state*state) set" 
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

95 
"req_down == 
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

96 
{(s,s'). s' = s (stop :=False, 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

97 
floor := floor s  1, 
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

98 
up := False) 
13806  99 
& s \<in> (ready \<inter> goingdown)}" 
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

100 

65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

101 
move_up :: "(state*state) set" 
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

102 
"move_up == 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

103 
{(s,s'). s' = s (floor := floor s + 1) 
13806  104 
& ~ stop s & up s & floor s \<notin> req s}" 
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

105 

65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

106 
move_down :: "(state*state) set" 
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

107 
"move_down == 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

108 
{(s,s'). s' = s (floor := floor s  1) 
13806  109 
& ~ stop s & ~ up s & floor s \<notin> req s}" 
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

110 

65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

111 
(*This action is omitted from prior treatments, which therefore are 
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

112 
unrealistic: nobody asks the lift to do anything! But adding this 
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

113 
action invalidates many of the existing progress arguments: various 
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

114 
"ensures" properties fail.*) 
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

115 
button_press :: "(state*state) set" 
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

116 
"button_press == 
13806  117 
{(s,s'). \<exists>n. s' = s (req := insert n (req s)) 
118 
& Min \<le> n & n \<le> Max}" 

11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

119 

65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

120 

13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

121 
Lift :: "state program" 
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

122 
(*for the moment, we OMIT button_press*) 
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13806
diff
changeset

123 
"Lift == mk_total_program 
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13806
diff
changeset

124 
({s. floor s = Min & ~ up s & move s & stop s & 
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

125 
~ open s & req s = {}}, 
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13806
diff
changeset

126 
{request_act, open_act, close_act, 
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13806
diff
changeset

127 
req_up, req_down, move_up, move_down}, 
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13806
diff
changeset

128 
UNIV)" 
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

129 

65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

130 

65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

131 
(** Invariants **) 
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

132 

13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

133 
bounded :: "state set" 
13806  134 
"bounded == {s. Min \<le> floor s & floor s \<le> Max}" 
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

135 

13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

136 
open_stop :: "state set" 
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

137 
"open_stop == {s. open s > stop s}" 
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

138 

13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

139 
open_move :: "state set" 
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

140 
"open_move == {s. open s > move s}" 
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

141 

13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

142 
stop_floor :: "state set" 
13806  143 
"stop_floor == {s. stop s & ~ move s > floor s \<in> req s}" 
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

144 

13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

145 
moving_up :: "state set" 
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

146 
"moving_up == {s. ~ stop s & up s > 
13806  147 
(\<exists>f. floor s \<le> f & f \<le> Max & f \<in> req s)}" 
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

148 

13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

149 
moving_down :: "state set" 
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

150 
"moving_down == {s. ~ stop s & ~ up s > 
13806  151 
(\<exists>f. Min \<le> f & f \<le> floor s & f \<in> req s)}" 
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

152 

13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

153 
metric :: "[int,state] => int" 
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

154 
"metric == 
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

155 
%n s. if floor s < n then (if up s then n  floor s 
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

156 
else (floor s  Min) + (nMin)) 
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

157 
else 
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

158 
if n < floor s then (if up s then (Max  floor s) + (Maxn) 
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

159 
else floor s  n) 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

160 
else 0" 
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

161 

13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

162 
locale Floor = 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

163 
fixes n 
13806  164 
assumes Min_le_n [iff]: "Min \<le> n" 
165 
and n_le_Max [iff]: "n \<le> Max" 

13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

166 

13806  167 
lemma not_mem_distinct: "[ x \<notin> A; y \<in> A ] ==> x \<noteq> y" 
13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

168 
by blast 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

169 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

170 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

171 
declare Lift_def [THEN def_prg_Init, simp] 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

172 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

173 
declare request_act_def [THEN def_act_simp, simp] 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

174 
declare open_act_def [THEN def_act_simp, simp] 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

175 
declare close_act_def [THEN def_act_simp, simp] 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

176 
declare req_up_def [THEN def_act_simp, simp] 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

177 
declare req_down_def [THEN def_act_simp, simp] 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

178 
declare move_up_def [THEN def_act_simp, simp] 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

179 
declare move_down_def [THEN def_act_simp, simp] 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

180 
declare button_press_def [THEN def_act_simp, simp] 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

181 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

182 
(*The ALWAYS properties*) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

183 
declare above_def [THEN def_set_simp, simp] 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

184 
declare below_def [THEN def_set_simp, simp] 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

185 
declare queueing_def [THEN def_set_simp, simp] 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

186 
declare goingup_def [THEN def_set_simp, simp] 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

187 
declare goingdown_def [THEN def_set_simp, simp] 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

188 
declare ready_def [THEN def_set_simp, simp] 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

189 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

190 
(*Basic definitions*) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

191 
declare bounded_def [simp] 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

192 
open_stop_def [simp] 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

193 
open_move_def [simp] 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

194 
stop_floor_def [simp] 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

195 
moving_up_def [simp] 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

196 
moving_down_def [simp] 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

197 

13806  198 
lemma open_stop: "Lift \<in> Always open_stop" 
13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

199 
apply (rule AlwaysI, force) 
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13806
diff
changeset

200 
apply (unfold Lift_def, constrains) 
13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

201 
done 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

202 

13806  203 
lemma stop_floor: "Lift \<in> Always stop_floor" 
13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

204 
apply (rule AlwaysI, force) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

205 
apply (unfold Lift_def, constrains) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

206 
done 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

207 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

208 
(*This one needs open_stop, which was proved above*) 
13806  209 
lemma open_move: "Lift \<in> Always open_move" 
13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

210 
apply (cut_tac open_stop) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

211 
apply (rule AlwaysI, force) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

212 
apply (unfold Lift_def, constrains) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

213 
done 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

214 

13806  215 
lemma moving_up: "Lift \<in> Always moving_up" 
13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

216 
apply (rule AlwaysI, force) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

217 
apply (unfold Lift_def, constrains) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

218 
apply (auto dest: zle_imp_zless_or_eq simp add: add1_zle_eq) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

219 
done 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

220 

13806  221 
lemma moving_down: "Lift \<in> Always moving_down" 
13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

222 
apply (rule AlwaysI, force) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

223 
apply (unfold Lift_def, constrains) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

224 
apply (blast dest: zle_imp_zless_or_eq) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

225 
done 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

226 

13806  227 
lemma bounded: "Lift \<in> Always bounded" 
13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

228 
apply (cut_tac moving_up moving_down) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

229 
apply (rule AlwaysI, force) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

230 
apply (unfold Lift_def, constrains, auto) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

231 
apply (drule not_mem_distinct, assumption, arith)+ 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

232 
done 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

233 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

234 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

235 
subsection{*Progress*} 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

236 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

237 
declare moving_def [THEN def_set_simp, simp] 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

238 
declare stopped_def [THEN def_set_simp, simp] 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

239 
declare opened_def [THEN def_set_simp, simp] 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

240 
declare closed_def [THEN def_set_simp, simp] 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

241 
declare atFloor_def [THEN def_set_simp, simp] 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

242 
declare Req_def [THEN def_set_simp, simp] 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

243 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

244 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

245 
(** The HUG'93 paper mistakenly omits the Req n from these! **) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

246 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

247 
(** Lift_1 **) 
13806  248 
lemma E_thm01: "Lift \<in> (stopped \<inter> atFloor n) LeadsTo (opened \<inter> atFloor n)" 
13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

249 
apply (cut_tac stop_floor) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

250 
apply (unfold Lift_def, ensures_tac "open_act") 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

251 
done (*lem_lift_1_5*) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

252 

13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13806
diff
changeset

253 

91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13806
diff
changeset

254 

91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13806
diff
changeset

255 

13806  256 
lemma E_thm02: "Lift \<in> (Req n \<inter> stopped  atFloor n) LeadsTo 
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13806
diff
changeset

257 
(Req n \<inter> opened  atFloor n)" 
13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

258 
apply (cut_tac stop_floor) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

259 
apply (unfold Lift_def, ensures_tac "open_act") 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

260 
done (*lem_lift_1_1*) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

261 

13806  262 
lemma E_thm03: "Lift \<in> (Req n \<inter> opened  atFloor n) LeadsTo 
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13806
diff
changeset

263 
(Req n \<inter> closed  (atFloor n  queueing))" 
13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

264 
apply (unfold Lift_def, ensures_tac "close_act") 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

265 
done (*lem_lift_1_2*) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

266 

13806  267 
lemma E_thm04: "Lift \<in> (Req n \<inter> closed \<inter> (atFloor n  queueing)) 
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13806
diff
changeset

268 
LeadsTo (opened \<inter> atFloor n)" 
13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

269 
apply (unfold Lift_def, ensures_tac "open_act") 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

270 
done (*lem_lift_1_7*) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

271 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

272 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

273 
(** Lift 2. Statements of thm05a and thm05b were wrong! **) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

274 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

275 
lemmas linorder_leI = linorder_not_less [THEN iffD1] 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

276 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

277 
lemmas (in Floor) le_MinD = Min_le_n [THEN order_antisym] 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

278 
and Max_leD = n_le_Max [THEN [2] order_antisym] 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

279 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

280 
declare (in Floor) le_MinD [dest!] 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

281 
and linorder_leI [THEN le_MinD, dest!] 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

282 
and Max_leD [dest!] 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

283 
and linorder_leI [THEN Max_leD, dest!] 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

284 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

285 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

286 
(*lem_lift_2_0 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

287 
NOT an ensures_tac property, but a mere inclusion 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

288 
don't know why script lift_2.uni says ENSURES*) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

289 
lemma (in Floor) E_thm05c: 
13806  290 
"Lift \<in> (Req n \<inter> closed  (atFloor n  queueing)) 
291 
LeadsTo ((closed \<inter> goingup \<inter> Req n) \<union> 

292 
(closed \<inter> goingdown \<inter> Req n))" 

13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

293 
by (auto intro!: subset_imp_LeadsTo elim!: int_neqE) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

294 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

295 
(*lift_2*) 
13806  296 
lemma (in Floor) lift_2: "Lift \<in> (Req n \<inter> closed  (atFloor n  queueing)) 
297 
LeadsTo (moving \<inter> Req n)" 

13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

298 
apply (rule LeadsTo_Trans [OF E_thm05c LeadsTo_Un]) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

299 
apply (unfold Lift_def) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

300 
apply (ensures_tac [2] "req_down") 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

301 
apply (ensures_tac "req_up", auto) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

302 
done 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

303 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

304 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

305 
(** Towards lift_4 ***) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

306 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

307 
declare split_if_asm [split] 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

308 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

309 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

310 
(*lem_lift_4_1 *) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

311 
lemma (in Floor) E_thm12a: 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

312 
"0 < N ==> 
13806  313 
Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> 
314 
{s. floor s \<notin> req s} \<inter> {s. up s}) 

13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

315 
LeadsTo 
13806  316 
(moving \<inter> Req n \<inter> {s. metric n s < N})" 
13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

317 
apply (cut_tac moving_up) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

318 
apply (unfold Lift_def, ensures_tac "move_up", safe) 
13806  319 
(*this step consolidates two formulae to the goal metric n s' \<le> metric n s*) 
13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

320 
apply (erule linorder_leI [THEN order_antisym, symmetric]) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

321 
apply (auto simp add: metric_def) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

322 
done 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

323 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

324 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

325 
(*lem_lift_4_3 *) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

326 
lemma (in Floor) E_thm12b: "0 < N ==> 
13806  327 
Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> 
328 
{s. floor s \<notin> req s}  {s. up s}) 

329 
LeadsTo (moving \<inter> Req n \<inter> {s. metric n s < N})" 

13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

330 
apply (cut_tac moving_down) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

331 
apply (unfold Lift_def, ensures_tac "move_down", safe) 
13806  332 
(*this step consolidates two formulae to the goal metric n s' \<le> metric n s*) 
13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

333 
apply (erule linorder_leI [THEN order_antisym, symmetric]) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

334 
apply (auto simp add: metric_def) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

335 
done 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

336 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

337 
(*lift_4*) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

338 
lemma (in Floor) lift_4: 
13806  339 
"0<N ==> Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> 
340 
{s. floor s \<notin> req s}) LeadsTo 

341 
(moving \<inter> Req n \<inter> {s. metric n s < N})" 

13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

342 
apply (rule LeadsTo_Trans [OF subset_imp_LeadsTo 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

343 
LeadsTo_Un [OF E_thm12a E_thm12b]], auto) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

344 
done 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

345 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

346 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

347 
(** towards lift_5 **) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

348 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

349 
(*lem_lift_5_3*) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

350 
lemma (in Floor) E_thm16a: "0<N 
13806  351 
==> Lift \<in> (closed \<inter> Req n \<inter> {s. metric n s = N} \<inter> goingup) LeadsTo 
352 
(moving \<inter> Req n \<inter> {s. metric n s < N})" 

13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

353 
apply (cut_tac bounded) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

354 
apply (unfold Lift_def, ensures_tac "req_up") 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

355 
apply (auto simp add: metric_def) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

356 
done 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

357 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

358 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

359 
(*lem_lift_5_1 has ~goingup instead of goingdown*) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

360 
lemma (in Floor) E_thm16b: "0<N ==> 
13806  361 
Lift \<in> (closed \<inter> Req n \<inter> {s. metric n s = N} \<inter> goingdown) LeadsTo 
362 
(moving \<inter> Req n \<inter> {s. metric n s < N})" 

13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

363 
apply (cut_tac bounded) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

364 
apply (unfold Lift_def, ensures_tac "req_down") 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

365 
apply (auto simp add: metric_def) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

366 
done 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

367 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

368 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

369 
(*lem_lift_5_0 proves an intersection involving ~goingup and goingup, 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

370 
i.e. the trivial disjunction, leading to an asymmetrical proof.*) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

371 
lemma (in Floor) E_thm16c: 
13806  372 
"0<N ==> Req n \<inter> {s. metric n s = N} \<subseteq> goingup \<union> goingdown" 
13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

373 
by (force simp add: metric_def) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

374 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

375 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

376 
(*lift_5*) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

377 
lemma (in Floor) lift_5: 
13806  378 
"0<N ==> Lift \<in> (closed \<inter> Req n \<inter> {s. metric n s = N}) LeadsTo 
379 
(moving \<inter> Req n \<inter> {s. metric n s < N})" 

13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

380 
apply (rule LeadsTo_Trans [OF subset_imp_LeadsTo 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

381 
LeadsTo_Un [OF E_thm16a E_thm16b]]) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

382 
apply (drule E_thm16c, auto) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

383 
done 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

384 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

385 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

386 
(** towards lift_3 **) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

387 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

388 
(*lemma used to prove lem_lift_3_1*) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

389 
lemma (in Floor) metric_eq_0D [dest]: 
13806  390 
"[ metric n s = 0; Min \<le> floor s; floor s \<le> Max ] ==> floor s = n" 
13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

391 
by (force simp add: metric_def) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

392 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

393 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

394 
(*lem_lift_3_1*) 
13806  395 
lemma (in Floor) E_thm11: "Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = 0}) LeadsTo 
396 
(stopped \<inter> atFloor n)" 

13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

397 
apply (cut_tac bounded) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

398 
apply (unfold Lift_def, ensures_tac "request_act", auto) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

399 
done 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

400 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

401 
(*lem_lift_3_5*) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

402 
lemma (in Floor) E_thm13: 
13806  403 
"Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> {s. floor s \<in> req s}) 
404 
LeadsTo (stopped \<inter> Req n \<inter> {s. metric n s = N} \<inter> {s. floor s \<in> req s})" 

13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

405 
apply (unfold Lift_def, ensures_tac "request_act") 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

406 
apply (auto simp add: metric_def) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

407 
done 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

408 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

409 
(*lem_lift_3_6*) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

410 
lemma (in Floor) E_thm14: "0 < N ==> 
13806  411 
Lift \<in> 
412 
(stopped \<inter> Req n \<inter> {s. metric n s = N} \<inter> {s. floor s \<in> req s}) 

413 
LeadsTo (opened \<inter> Req n \<inter> {s. metric n s = N})" 

13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

414 
apply (unfold Lift_def, ensures_tac "open_act") 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

415 
apply (auto simp add: metric_def) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

416 
done 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

417 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

418 
(*lem_lift_3_7*) 
13806  419 
lemma (in Floor) E_thm15: "Lift \<in> (opened \<inter> Req n \<inter> {s. metric n s = N}) 
420 
LeadsTo (closed \<inter> Req n \<inter> {s. metric n s = N})" 

13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

421 
apply (unfold Lift_def, ensures_tac "close_act") 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

422 
apply (auto simp add: metric_def) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

423 
done 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

424 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

425 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

426 
(** the final steps **) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

427 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

428 
lemma (in Floor) lift_3_Req: "0 < N ==> 
13806  429 
Lift \<in> 
430 
(moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> {s. floor s \<in> req s}) 

431 
LeadsTo (moving \<inter> Req n \<inter> {s. metric n s < N})" 

13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

432 
apply (blast intro!: E_thm13 E_thm14 E_thm15 lift_5 intro: LeadsTo_Trans) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

433 
done 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

434 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

435 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

436 
(*Now we observe that our integer metric is really a natural number*) 
13806  437 
lemma (in Floor) Always_nonneg: "Lift \<in> Always {s. 0 \<le> metric n s}" 
13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

438 
apply (rule bounded [THEN Always_weaken]) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

439 
apply (auto simp add: metric_def) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

440 
done 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

441 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

442 
lemmas (in Floor) R_thm11 = Always_LeadsTo_weaken [OF Always_nonneg E_thm11] 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

443 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

444 
lemma (in Floor) lift_3: 
13806  445 
"Lift \<in> (moving \<inter> Req n) LeadsTo (stopped \<inter> atFloor n)" 
13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

446 
apply (rule Always_nonneg [THEN integ_0_le_induct]) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

447 
apply (case_tac "0 < z") 
13806  448 
(*If z \<le> 0 then actually z = 0*) 
13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

449 
prefer 2 apply (force intro: R_thm11 order_antisym simp add: linorder_not_less) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

450 
apply (rule LeadsTo_weaken_R [OF asm_rl Un_upper1]) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

451 
apply (rule LeadsTo_Trans [OF subset_imp_LeadsTo 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

452 
LeadsTo_Un [OF lift_4 lift_3_Req]], auto) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

453 
done 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

454 

e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

455 

13806  456 
lemma (in Floor) lift_1: "Lift \<in> (Req n) LeadsTo (opened \<inter> atFloor n)" 
13785
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

457 
apply (rule LeadsTo_Trans) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

458 
prefer 2 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

459 
apply (rule LeadsTo_Un [OF E_thm04 LeadsTo_Un_post]) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

460 
apply (rule E_thm01 [THEN [2] LeadsTo_Trans_Un]) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

461 
apply (rule lift_3 [THEN [2] LeadsTo_Trans_Un]) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

462 
apply (rule lift_2 [THEN [2] LeadsTo_Trans_Un]) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

463 
apply (rule LeadsTo_Trans_Un [OF E_thm02 E_thm03]) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

464 
apply (rule open_move [THEN Always_LeadsToI]) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

465 
apply (rule Always_LeadsToI [OF open_stop subset_imp_LeadsTo], clarify) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

466 
(*The case split is not essential but makes the proof much faster.*) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

467 
apply (case_tac "open x", auto) 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

468 
done 
e2fcd88be55d
Partial conversion of UNITY to Isar newstyle theories
paulson
parents:
11868
diff
changeset

469 

11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

470 

65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset

471 
end 