src/HOL/UNITY/Simple/Lift.thy
author paulson
Sat, 08 Feb 2003 16:05:33 +0100
changeset 13812 91713a1915ee
parent 13806 fd40c9d9076b
child 14378 69c4d5997669
permissions -rw-r--r--
converting HOL/UNITY to use unconditional fairness
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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 Lift-Control 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 new-style 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 new-style theories
paulson
parents: 11868
diff changeset
    12
  floor :: "int"	    (*current position of the lift*)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
    13
  "open" :: "bool"	    (*whether the door is opened at floor*)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
    14
  stop  :: "bool"	    (*whether the lift is stopped at floor*)
e2fcd88be55d Partial conversion of UNITY to Isar new-style 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 new-style theories
paulson
parents: 11868
diff changeset
    16
  up    :: "bool"	    (*current direction of movement*)
e2fcd88be55d Partial conversion of UNITY to Isar new-style 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 new-style theories
paulson
parents: 11868
diff changeset
    20
  Min :: "int"       (*least and greatest floors*)
e2fcd88be55d Partial conversion of UNITY to Isar new-style 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 new-style theories
paulson
parents: 11868
diff changeset
    23
axioms
13806
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
    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 new-style theories
paulson
parents: 11868
diff changeset
    30
  above :: "state set"
13806
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
    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 new-style theories
paulson
parents: 11868
diff changeset
    33
  below :: "state set"
13806
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
    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 new-style theories
paulson
parents: 11868
diff changeset
    36
  queueing :: "state set"
13806
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
    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 new-style theories
paulson
parents: 11868
diff changeset
    39
  goingup :: "state set"
13806
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
    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 new-style theories
paulson
parents: 11868
diff changeset
    42
  goingdown :: "state set"
13806
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
    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 new-style 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 new-style 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 new-style 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 new-style 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 new-style 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 new-style 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 new-style theories
paulson
parents: 11868
diff changeset
    65
  Req :: "int => state set"
13806
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
    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
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
    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
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
    81
		       & stop s & ~ open s & floor s \<in> req s
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
    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
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
    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
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
    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
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   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
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   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
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   117
         {(s,s'). \<exists>n. s' = s (|req := insert n (req s)|)
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   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 new-style 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 new-style theories
paulson
parents: 11868
diff changeset
   133
  bounded :: "state set"
13806
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   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 new-style 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 new-style 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 new-style theories
paulson
parents: 11868
diff changeset
   142
  stop_floor :: "state set"
13806
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   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 new-style 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
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   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 new-style 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
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   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 new-style 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) + (n-Min))
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) + (Max-n)
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 new-style theories
paulson
parents: 11868
diff changeset
   162
locale Floor =
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   163
  fixes n
13806
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   164
  assumes Min_le_n [iff]: "Min \<le> n"
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   165
      and n_le_Max [iff]: "n \<le> Max"
13785
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   166
13806
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   167
lemma not_mem_distinct: "[| x \<notin> A;  y \<in> A |] ==> x \<noteq> y"
13785
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   168
by blast
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   169
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   170
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   171
declare Lift_def [THEN def_prg_Init, simp]
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   172
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   173
declare request_act_def [THEN def_act_simp, simp]
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   174
declare open_act_def [THEN def_act_simp, simp]
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   175
declare close_act_def [THEN def_act_simp, simp]
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   176
declare req_up_def [THEN def_act_simp, simp]
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   177
declare req_down_def [THEN def_act_simp, simp]
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   178
declare move_up_def [THEN def_act_simp, simp]
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   179
declare move_down_def [THEN def_act_simp, simp]
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   180
declare button_press_def [THEN def_act_simp, simp]
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   181
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   182
(*The ALWAYS properties*)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   183
declare above_def [THEN def_set_simp, simp]
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   184
declare below_def [THEN def_set_simp, simp]
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   185
declare queueing_def [THEN def_set_simp, simp]
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   186
declare goingup_def [THEN def_set_simp, simp]
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   187
declare goingdown_def [THEN def_set_simp, simp]
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   188
declare ready_def [THEN def_set_simp, simp]
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   189
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   190
(*Basic definitions*)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   191
declare bounded_def [simp] 
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   192
        open_stop_def [simp] 
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   193
        open_move_def [simp] 
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   194
        stop_floor_def [simp]
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   195
        moving_up_def [simp]
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   196
        moving_down_def [simp]
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   197
13806
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   198
lemma open_stop: "Lift \<in> Always open_stop"
13785
e2fcd88be55d Partial conversion of UNITY to Isar new-style 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 new-style theories
paulson
parents: 11868
diff changeset
   201
done
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   202
13806
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   203
lemma stop_floor: "Lift \<in> Always stop_floor"
13785
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   204
apply (rule AlwaysI, force) 
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   205
apply (unfold Lift_def, constrains)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   206
done
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   207
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   208
(*This one needs open_stop, which was proved above*)
13806
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   209
lemma open_move: "Lift \<in> Always open_move"
13785
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   210
apply (cut_tac open_stop)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   211
apply (rule AlwaysI, force) 
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   212
apply (unfold Lift_def, constrains)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   213
done
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   214
13806
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   215
lemma moving_up: "Lift \<in> Always moving_up"
13785
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   216
apply (rule AlwaysI, force) 
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   217
apply (unfold Lift_def, constrains)
e2fcd88be55d Partial conversion of UNITY to Isar new-style 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 new-style theories
paulson
parents: 11868
diff changeset
   219
done
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   220
13806
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   221
lemma moving_down: "Lift \<in> Always moving_down"
13785
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   222
apply (rule AlwaysI, force) 
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   223
apply (unfold Lift_def, constrains)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   224
apply (blast dest: zle_imp_zless_or_eq)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   225
done
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   226
13806
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   227
lemma bounded: "Lift \<in> Always bounded"
13785
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   228
apply (cut_tac moving_up moving_down)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   229
apply (rule AlwaysI, force) 
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   230
apply (unfold Lift_def, constrains, auto)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   231
apply (drule not_mem_distinct, assumption, arith)+
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   232
done
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   233
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   234
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   235
subsection{*Progress*}
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   236
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   237
declare moving_def [THEN def_set_simp, simp]
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   238
declare stopped_def [THEN def_set_simp, simp]
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   239
declare opened_def [THEN def_set_simp, simp]
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   240
declare closed_def [THEN def_set_simp, simp]
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   241
declare atFloor_def [THEN def_set_simp, simp]
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   242
declare Req_def [THEN def_set_simp, simp]
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   243
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   244
e2fcd88be55d Partial conversion of UNITY to Isar new-style 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 new-style theories
paulson
parents: 11868
diff changeset
   246
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   247
(** Lift_1 **)
13806
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   248
lemma E_thm01: "Lift \<in> (stopped \<inter> atFloor n) LeadsTo (opened \<inter> atFloor n)"
13785
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   249
apply (cut_tac stop_floor)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   250
apply (unfold Lift_def, ensures_tac "open_act")
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   251
done  (*lem_lift_1_5*)
e2fcd88be55d Partial conversion of UNITY to Isar new-style 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
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   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 new-style theories
paulson
parents: 11868
diff changeset
   258
apply (cut_tac stop_floor)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   259
apply (unfold Lift_def, ensures_tac "open_act")
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   260
done  (*lem_lift_1_1*)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   261
13806
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   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 new-style theories
paulson
parents: 11868
diff changeset
   264
apply (unfold Lift_def, ensures_tac "close_act")
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   265
done  (*lem_lift_1_2*)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   266
13806
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   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 new-style theories
paulson
parents: 11868
diff changeset
   269
apply (unfold Lift_def, ensures_tac "open_act")
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   270
done  (*lem_lift_1_7*)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   271
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   272
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   273
(** Lift 2.  Statements of thm05a and thm05b were wrong! **)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   274
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   275
lemmas linorder_leI = linorder_not_less [THEN iffD1]
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   276
e2fcd88be55d Partial conversion of UNITY to Isar new-style 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 new-style theories
paulson
parents: 11868
diff changeset
   278
              and Max_leD = n_le_Max [THEN [2] order_antisym]
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   279
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   280
declare (in Floor) le_MinD [dest!]
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   281
               and linorder_leI [THEN le_MinD, dest!]
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   282
               and Max_leD [dest!]
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   283
               and linorder_leI [THEN Max_leD, dest!]
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   284
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   285
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   286
(*lem_lift_2_0 
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   287
  NOT an ensures_tac property, but a mere inclusion
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   288
  don't know why script lift_2.uni says ENSURES*)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   289
lemma (in Floor) E_thm05c: 
13806
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   290
    "Lift \<in> (Req n \<inter> closed - (atFloor n - queueing))    
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   291
             LeadsTo ((closed \<inter> goingup \<inter> Req n)  \<union> 
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   292
                      (closed \<inter> goingdown \<inter> Req n))"
13785
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   293
by (auto intro!: subset_imp_LeadsTo elim!: int_neqE)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   294
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   295
(*lift_2*)
13806
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   296
lemma (in Floor) lift_2: "Lift \<in> (Req n \<inter> closed - (atFloor n - queueing))    
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   297
             LeadsTo (moving \<inter> Req n)"
13785
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   298
apply (rule LeadsTo_Trans [OF E_thm05c LeadsTo_Un])
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   299
apply (unfold Lift_def) 
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   300
apply (ensures_tac [2] "req_down")
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   301
apply (ensures_tac "req_up", auto)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   302
done
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   303
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   304
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   305
(** Towards lift_4 ***)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   306
 
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   307
declare split_if_asm [split]
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   308
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   309
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   310
(*lem_lift_4_1 *)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   311
lemma (in Floor) E_thm12a:
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   312
     "0 < N ==>  
13806
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   313
      Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> 
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   314
              {s. floor s \<notin> req s} \<inter> {s. up s})    
13785
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   315
             LeadsTo  
13806
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   316
               (moving \<inter> Req n \<inter> {s. metric n s < N})"
13785
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   317
apply (cut_tac moving_up)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   318
apply (unfold Lift_def, ensures_tac "move_up", safe)
13806
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   319
(*this step consolidates two formulae to the goal  metric n s' \<le> metric n s*)
13785
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   320
apply (erule linorder_leI [THEN order_antisym, symmetric])
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   321
apply (auto simp add: metric_def)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   322
done
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   323
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   324
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   325
(*lem_lift_4_3 *)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   326
lemma (in Floor) E_thm12b: "0 < N ==>  
13806
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   327
      Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> 
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   328
              {s. floor s \<notin> req s} - {s. up s})    
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   329
             LeadsTo (moving \<inter> Req n \<inter> {s. metric n s < N})"
13785
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   330
apply (cut_tac moving_down)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   331
apply (unfold Lift_def, ensures_tac "move_down", safe)
13806
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   332
(*this step consolidates two formulae to the goal  metric n s' \<le> metric n s*)
13785
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   333
apply (erule linorder_leI [THEN order_antisym, symmetric])
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   334
apply (auto simp add: metric_def)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   335
done
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   336
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   337
(*lift_4*)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   338
lemma (in Floor) lift_4:
13806
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   339
     "0<N ==> Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> 
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   340
                            {s. floor s \<notin> req s}) LeadsTo      
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   341
                           (moving \<inter> Req n \<inter> {s. metric n s < N})"
13785
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   342
apply (rule LeadsTo_Trans [OF subset_imp_LeadsTo
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   343
                              LeadsTo_Un [OF E_thm12a E_thm12b]], auto)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   344
done
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   345
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   346
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   347
(** towards lift_5 **)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   348
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   349
(*lem_lift_5_3*)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   350
lemma (in Floor) E_thm16a: "0<N    
13806
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   351
  ==> Lift \<in> (closed \<inter> Req n \<inter> {s. metric n s = N} \<inter> goingup) LeadsTo  
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   352
             (moving \<inter> Req n \<inter> {s. metric n s < N})"
13785
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   353
apply (cut_tac bounded)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   354
apply (unfold Lift_def, ensures_tac "req_up")
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   355
apply (auto simp add: metric_def)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   356
done
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   357
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   358
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   359
(*lem_lift_5_1 has ~goingup instead of goingdown*)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   360
lemma (in Floor) E_thm16b: "0<N ==>    
13806
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   361
      Lift \<in> (closed \<inter> Req n \<inter> {s. metric n s = N} \<inter> goingdown) LeadsTo  
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   362
                   (moving \<inter> Req n \<inter> {s. metric n s < N})"
13785
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   363
apply (cut_tac bounded)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   364
apply (unfold Lift_def, ensures_tac "req_down")
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   365
apply (auto simp add: metric_def)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   366
done
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   367
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   368
e2fcd88be55d Partial conversion of UNITY to Isar new-style 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 new-style theories
paulson
parents: 11868
diff changeset
   370
  i.e. the trivial disjunction, leading to an asymmetrical proof.*)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   371
lemma (in Floor) E_thm16c:
13806
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   372
     "0<N ==> Req n \<inter> {s. metric n s = N} \<subseteq> goingup \<union> goingdown"
13785
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   373
by (force simp add: metric_def)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   374
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   375
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   376
(*lift_5*)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   377
lemma (in Floor) lift_5:
13806
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   378
     "0<N ==> Lift \<in> (closed \<inter> Req n \<inter> {s. metric n s = N}) LeadsTo    
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   379
                     (moving \<inter> Req n \<inter> {s. metric n s < N})"
13785
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   380
apply (rule LeadsTo_Trans [OF subset_imp_LeadsTo
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   381
                              LeadsTo_Un [OF E_thm16a E_thm16b]])
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   382
apply (drule E_thm16c, auto)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   383
done
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   384
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   385
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   386
(** towards lift_3 **)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   387
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   388
(*lemma used to prove lem_lift_3_1*)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   389
lemma (in Floor) metric_eq_0D [dest]:
13806
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   390
     "[| metric n s = 0;  Min \<le> floor s;  floor s \<le> Max |] ==> floor s = n"
13785
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   391
by (force simp add: metric_def)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   392
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   393
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   394
(*lem_lift_3_1*)
13806
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   395
lemma (in Floor) E_thm11: "Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = 0}) LeadsTo    
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   396
                       (stopped \<inter> atFloor n)"
13785
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   397
apply (cut_tac bounded)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   398
apply (unfold Lift_def, ensures_tac "request_act", auto)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   399
done
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   400
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   401
(*lem_lift_3_5*)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   402
lemma (in Floor) E_thm13: 
13806
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   403
  "Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> {s. floor s \<in> req s})  
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   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 new-style theories
paulson
parents: 11868
diff changeset
   405
apply (unfold Lift_def, ensures_tac "request_act")
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   406
apply (auto simp add: metric_def)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   407
done
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   408
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   409
(*lem_lift_3_6*)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   410
lemma (in Floor) E_thm14: "0 < N ==>  
13806
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   411
      Lift \<in>  
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   412
        (stopped \<inter> Req n \<inter> {s. metric n s = N} \<inter> {s. floor s \<in> req s})  
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   413
        LeadsTo (opened \<inter> Req n \<inter> {s. metric n s = N})"
13785
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   414
apply (unfold Lift_def, ensures_tac "open_act")
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   415
apply (auto simp add: metric_def)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   416
done
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   417
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   418
(*lem_lift_3_7*)
13806
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   419
lemma (in Floor) E_thm15: "Lift \<in> (opened \<inter> Req n \<inter> {s. metric n s = N})   
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   420
             LeadsTo (closed \<inter> Req n \<inter> {s. metric n s = N})"
13785
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   421
apply (unfold Lift_def, ensures_tac "close_act")
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   422
apply (auto simp add: metric_def)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   423
done
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   424
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   425
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   426
(** the final steps **)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   427
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   428
lemma (in Floor) lift_3_Req: "0 < N ==>  
13806
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   429
      Lift \<in>  
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   430
        (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> {s. floor s \<in> req s})    
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   431
        LeadsTo (moving \<inter> Req n \<inter> {s. metric n s < N})"
13785
e2fcd88be55d Partial conversion of UNITY to Isar new-style 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 new-style theories
paulson
parents: 11868
diff changeset
   433
done
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   434
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   435
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   436
(*Now we observe that our integer metric is really a natural number*)
13806
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   437
lemma (in Floor) Always_nonneg: "Lift \<in> Always {s. 0 \<le> metric n s}"
13785
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   438
apply (rule bounded [THEN Always_weaken])
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   439
apply (auto simp add: metric_def)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   440
done
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   441
e2fcd88be55d Partial conversion of UNITY to Isar new-style 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 new-style theories
paulson
parents: 11868
diff changeset
   443
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   444
lemma (in Floor) lift_3:
13806
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   445
     "Lift \<in> (moving \<inter> Req n) LeadsTo (stopped \<inter> atFloor n)"
13785
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   446
apply (rule Always_nonneg [THEN integ_0_le_induct])
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   447
apply (case_tac "0 < z")
13806
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   448
(*If z \<le> 0 then actually z = 0*)
13785
e2fcd88be55d Partial conversion of UNITY to Isar new-style 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 new-style theories
paulson
parents: 11868
diff changeset
   450
apply (rule LeadsTo_weaken_R [OF asm_rl Un_upper1])
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   451
apply (rule LeadsTo_Trans [OF subset_imp_LeadsTo
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   452
                              LeadsTo_Un [OF lift_4 lift_3_Req]], auto)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   453
done
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   454
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   455
13806
fd40c9d9076b more tidying
paulson
parents: 13785
diff changeset
   456
lemma (in Floor) lift_1: "Lift \<in> (Req n) LeadsTo (opened \<inter> atFloor n)"
13785
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   457
apply (rule LeadsTo_Trans)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   458
 prefer 2
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   459
 apply (rule LeadsTo_Un [OF E_thm04 LeadsTo_Un_post])
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   460
 apply (rule E_thm01 [THEN [2] LeadsTo_Trans_Un])
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   461
 apply (rule lift_3 [THEN [2] LeadsTo_Trans_Un])
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   462
 apply (rule lift_2 [THEN [2] LeadsTo_Trans_Un])
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   463
 apply (rule LeadsTo_Trans_Un [OF E_thm02 E_thm03])
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   464
apply (rule open_move [THEN Always_LeadsToI])
e2fcd88be55d Partial conversion of UNITY to Isar new-style 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 new-style 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 new-style theories
paulson
parents: 11868
diff changeset
   467
apply (case_tac "open x", auto)
e2fcd88be55d Partial conversion of UNITY to Isar new-style theories
paulson
parents: 11868
diff changeset
   468
done
e2fcd88be55d Partial conversion of UNITY to Isar new-style 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