src/HOL/UNITY/Simple/Lift.thy
changeset 13806 fd40c9d9076b
parent 13785 e2fcd88be55d
child 13812 91713a1915ee
--- a/src/HOL/UNITY/Simple/Lift.thy	Tue Feb 04 18:12:40 2003 +0100
+++ b/src/HOL/UNITY/Simple/Lift.thy	Wed Feb 05 13:35:32 2003 +0100
@@ -21,26 +21,26 @@
   Max :: "int"       (*least and greatest floors*)
 
 axioms
-  Min_le_Max [iff]: "Min <= Max"
+  Min_le_Max [iff]: "Min \<le> Max"
   
 constdefs
   
   (** Abbreviations: the "always" part **)
   
   above :: "state set"
-    "above == {s. EX i. floor s < i & i <= Max & i : req s}"
+    "above == {s. \<exists>i. floor s < i & i \<le> Max & i \<in> req s}"
 
   below :: "state set"
-    "below == {s. EX i. Min <= i & i < floor s & i : req s}"
+    "below == {s. \<exists>i. Min \<le> i & i < floor s & i \<in> req s}"
 
   queueing :: "state set"
-    "queueing == above Un below"
+    "queueing == above \<union> below"
 
   goingup :: "state set"
-    "goingup   == above Int  ({s. up s}  Un -below)"
+    "goingup   == above \<inter> ({s. up s}  \<union> -below)"
 
   goingdown :: "state set"
-    "goingdown == below Int ({s. ~ up s} Un -above)"
+    "goingdown == below \<inter> ({s. ~ up s} \<union> -above)"
 
   ready :: "state set"
     "ready == {s. stop s & ~ open s & move s}"
@@ -63,7 +63,7 @@
     "atFloor n ==  {s. floor s = n}"
 
   Req :: "int => state set"
-    "Req n ==  {s. n : req s}"
+    "Req n ==  {s. n \<in> req s}"
 
 
   
@@ -71,15 +71,15 @@
   
   request_act :: "(state*state) set"
     "request_act == {(s,s'). s' = s (|stop:=True, move:=False|)
-		                  & ~ stop s & floor s : req s}"
+		                  & ~ stop s & floor s \<in> req s}"
 
   open_act :: "(state*state) set"
     "open_act ==
          {(s,s'). s' = s (|open :=True,
 			   req  := req s - {floor s},
 			   move := True|)
-		       & stop s & ~ open s & floor s : req s
-	               & ~(move s & s: queueing)}"
+		       & stop s & ~ open s & floor s \<in> req s
+	               & ~(move s & s \<in> queueing)}"
 
   close_act :: "(state*state) set"
     "close_act == {(s,s'). s' = s (|open := False|) & open s}"
@@ -89,24 +89,24 @@
          {(s,s'). s' = s (|stop  :=False,
 			   floor := floor s + 1,
 			   up    := True|)
-		       & s : (ready Int goingup)}"
+		       & s \<in> (ready \<inter> goingup)}"
 
   req_down :: "(state*state) set"
     "req_down ==
          {(s,s'). s' = s (|stop  :=False,
 			   floor := floor s - 1,
 			   up    := False|)
-		       & s : (ready Int goingdown)}"
+		       & s \<in> (ready \<inter> goingdown)}"
 
   move_up :: "(state*state) set"
     "move_up ==
          {(s,s'). s' = s (|floor := floor s + 1|)
-		       & ~ stop s & up s & floor s ~: req s}"
+		       & ~ stop s & up s & floor s \<notin> req s}"
 
   move_down :: "(state*state) set"
     "move_down ==
          {(s,s'). s' = s (|floor := floor s - 1|)
-		       & ~ stop s & ~ up s & floor s ~: req s}"
+		       & ~ stop s & ~ up s & floor s \<notin> req s}"
 
   (*This action is omitted from prior treatments, which therefore are
     unrealistic: nobody asks the lift to do anything!  But adding this
@@ -114,8 +114,8 @@
     "ensures" properties fail.*)
   button_press  :: "(state*state) set"
     "button_press ==
-         {(s,s'). EX n. s' = s (|req := insert n (req s)|)
-		        & Min <= n & n <= Max}"
+         {(s,s'). \<exists>n. s' = s (|req := insert n (req s)|)
+		        & Min \<le> n & n \<le> Max}"
 
 
   Lift :: "state program"
@@ -130,7 +130,7 @@
   (** Invariants **)
 
   bounded :: "state set"
-    "bounded == {s. Min <= floor s & floor s <= Max}"
+    "bounded == {s. Min \<le> floor s & floor s \<le> Max}"
 
   open_stop :: "state set"
     "open_stop == {s. open s --> stop s}"
@@ -139,15 +139,15 @@
     "open_move == {s. open s --> move s}"
   
   stop_floor :: "state set"
-    "stop_floor == {s. stop s & ~ move s --> floor s : req s}"
+    "stop_floor == {s. stop s & ~ move s --> floor s \<in> req s}"
   
   moving_up :: "state set"
     "moving_up == {s. ~ stop s & up s -->
-                   (EX f. floor s <= f & f <= Max & f : req s)}"
+                   (\<exists>f. floor s \<le> f & f \<le> Max & f \<in> req s)}"
   
   moving_down :: "state set"
     "moving_down == {s. ~ stop s & ~ up s -->
-                     (EX f. Min <= f & f <= floor s & f : req s)}"
+                     (\<exists>f. Min \<le> f & f \<le> floor s & f \<in> req s)}"
   
   metric :: "[int,state] => int"
     "metric ==
@@ -160,10 +160,10 @@
 
 locale Floor =
   fixes n
-  assumes Min_le_n [iff]: "Min <= n"
-      and n_le_Max [iff]: "n <= Max"
+  assumes Min_le_n [iff]: "Min \<le> n"
+      and n_le_Max [iff]: "n \<le> Max"
 
-lemma not_mem_distinct: "[| x ~: A;  y : A |] ==> x ~= y"
+lemma not_mem_distinct: "[| x \<notin> A;  y \<in> A |] ==> x \<noteq> y"
 by blast
 
 
@@ -194,36 +194,36 @@
         moving_up_def [simp]
         moving_down_def [simp]
 
-lemma open_stop: "Lift : Always open_stop"
+lemma open_stop: "Lift \<in> Always open_stop"
 apply (rule AlwaysI, force) 
 apply (unfold Lift_def, constrains) 
 done
 
-lemma stop_floor: "Lift : Always stop_floor"
+lemma stop_floor: "Lift \<in> Always stop_floor"
 apply (rule AlwaysI, force) 
 apply (unfold Lift_def, constrains)
 done
 
 (*This one needs open_stop, which was proved above*)
-lemma open_move: "Lift : Always open_move"
+lemma open_move: "Lift \<in> Always open_move"
 apply (cut_tac open_stop)
 apply (rule AlwaysI, force) 
 apply (unfold Lift_def, constrains)
 done
 
-lemma moving_up: "Lift : Always moving_up"
+lemma moving_up: "Lift \<in> Always moving_up"
 apply (rule AlwaysI, force) 
 apply (unfold Lift_def, constrains)
 apply (auto dest: zle_imp_zless_or_eq simp add: add1_zle_eq)
 done
 
-lemma moving_down: "Lift : Always moving_down"
+lemma moving_down: "Lift \<in> Always moving_down"
 apply (rule AlwaysI, force) 
 apply (unfold Lift_def, constrains)
 apply (blast dest: zle_imp_zless_or_eq)
 done
 
-lemma bounded: "Lift : Always bounded"
+lemma bounded: "Lift \<in> Always bounded"
 apply (cut_tac moving_up moving_down)
 apply (rule AlwaysI, force) 
 apply (unfold Lift_def, constrains, auto)
@@ -244,24 +244,24 @@
 (** The HUG'93 paper mistakenly omits the Req n from these! **)
 
 (** Lift_1 **)
-lemma E_thm01: "Lift : (stopped Int atFloor n) LeadsTo (opened Int atFloor n)"
+lemma E_thm01: "Lift \<in> (stopped \<inter> atFloor n) LeadsTo (opened \<inter> atFloor n)"
 apply (cut_tac stop_floor)
 apply (unfold Lift_def, ensures_tac "open_act")
 done  (*lem_lift_1_5*)
 
-lemma E_thm02: "Lift : (Req n Int stopped - atFloor n) LeadsTo  
-                     (Req n Int opened - atFloor n)"
+lemma E_thm02: "Lift \<in> (Req n \<inter> stopped - atFloor n) LeadsTo  
+                     (Req n \<inter> opened - atFloor n)"
 apply (cut_tac stop_floor)
 apply (unfold Lift_def, ensures_tac "open_act")
 done  (*lem_lift_1_1*)
 
-lemma E_thm03: "Lift : (Req n Int opened - atFloor n) LeadsTo  
-                     (Req n Int closed - (atFloor n - queueing))"
+lemma E_thm03: "Lift \<in> (Req n \<inter> opened - atFloor n) LeadsTo  
+                     (Req n \<inter> closed - (atFloor n - queueing))"
 apply (unfold Lift_def, ensures_tac "close_act")
 done  (*lem_lift_1_2*)
 
-lemma E_thm04: "Lift : (Req n Int closed Int (atFloor n - queueing))   
-             LeadsTo (opened Int atFloor n)"
+lemma E_thm04: "Lift \<in> (Req n \<inter> closed \<inter> (atFloor n - queueing))   
+             LeadsTo (opened \<inter> atFloor n)"
 apply (unfold Lift_def, ensures_tac "open_act")
 done  (*lem_lift_1_7*)
 
@@ -283,14 +283,14 @@
   NOT an ensures_tac property, but a mere inclusion
   don't know why script lift_2.uni says ENSURES*)
 lemma (in Floor) E_thm05c: 
-    "Lift : (Req n Int closed - (atFloor n - queueing))    
-             LeadsTo ((closed Int goingup Int Req n)  Un  
-                      (closed Int goingdown Int Req n))"
+    "Lift \<in> (Req n \<inter> closed - (atFloor n - queueing))    
+             LeadsTo ((closed \<inter> goingup \<inter> Req n)  \<union> 
+                      (closed \<inter> goingdown \<inter> Req n))"
 by (auto intro!: subset_imp_LeadsTo elim!: int_neqE)
 
 (*lift_2*)
-lemma (in Floor) lift_2: "Lift : (Req n Int closed - (atFloor n - queueing))    
-             LeadsTo (moving Int Req n)"
+lemma (in Floor) lift_2: "Lift \<in> (Req n \<inter> closed - (atFloor n - queueing))    
+             LeadsTo (moving \<inter> Req n)"
 apply (rule LeadsTo_Trans [OF E_thm05c LeadsTo_Un])
 apply (unfold Lift_def) 
 apply (ensures_tac [2] "req_down")
@@ -306,13 +306,13 @@
 (*lem_lift_4_1 *)
 lemma (in Floor) E_thm12a:
      "0 < N ==>  
-      Lift : (moving Int Req n Int {s. metric n s = N} Int  
-              {s. floor s ~: req s} Int {s. up s})    
+      Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> 
+              {s. floor s \<notin> req s} \<inter> {s. up s})    
              LeadsTo  
-               (moving Int Req n Int {s. metric n s < N})"
+               (moving \<inter> Req n \<inter> {s. metric n s < N})"
 apply (cut_tac moving_up)
 apply (unfold Lift_def, ensures_tac "move_up", safe)
-(*this step consolidates two formulae to the goal  metric n s' <= metric n s*)
+(*this step consolidates two formulae to the goal  metric n s' \<le> metric n s*)
 apply (erule linorder_leI [THEN order_antisym, symmetric])
 apply (auto simp add: metric_def)
 done
@@ -320,21 +320,21 @@
 
 (*lem_lift_4_3 *)
 lemma (in Floor) E_thm12b: "0 < N ==>  
-      Lift : (moving Int Req n Int {s. metric n s = N} Int  
-              {s. floor s ~: req s} - {s. up s})    
-             LeadsTo (moving Int Req n Int {s. metric n s < N})"
+      Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> 
+              {s. floor s \<notin> req s} - {s. up s})    
+             LeadsTo (moving \<inter> Req n \<inter> {s. metric n s < N})"
 apply (cut_tac moving_down)
 apply (unfold Lift_def, ensures_tac "move_down", safe)
-(*this step consolidates two formulae to the goal  metric n s' <= metric n s*)
+(*this step consolidates two formulae to the goal  metric n s' \<le> metric n s*)
 apply (erule linorder_leI [THEN order_antisym, symmetric])
 apply (auto simp add: metric_def)
 done
 
 (*lift_4*)
 lemma (in Floor) lift_4:
-     "0<N ==> Lift : (moving Int Req n Int {s. metric n s = N} Int  
-                            {s. floor s ~: req s}) LeadsTo      
-                           (moving Int Req n Int {s. metric n s < N})"
+     "0<N ==> Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> 
+                            {s. floor s \<notin> req s}) LeadsTo      
+                           (moving \<inter> Req n \<inter> {s. metric n s < N})"
 apply (rule LeadsTo_Trans [OF subset_imp_LeadsTo
                               LeadsTo_Un [OF E_thm12a E_thm12b]], auto)
 done
@@ -344,8 +344,8 @@
 
 (*lem_lift_5_3*)
 lemma (in Floor) E_thm16a: "0<N    
-  ==> Lift : (closed Int Req n Int {s. metric n s = N} Int goingup) LeadsTo  
-             (moving Int Req n Int {s. metric n s < N})"
+  ==> Lift \<in> (closed \<inter> Req n \<inter> {s. metric n s = N} \<inter> goingup) LeadsTo  
+             (moving \<inter> Req n \<inter> {s. metric n s < N})"
 apply (cut_tac bounded)
 apply (unfold Lift_def, ensures_tac "req_up")
 apply (auto simp add: metric_def)
@@ -354,8 +354,8 @@
 
 (*lem_lift_5_1 has ~goingup instead of goingdown*)
 lemma (in Floor) E_thm16b: "0<N ==>    
-      Lift : (closed Int Req n Int {s. metric n s = N} Int goingdown) LeadsTo  
-                   (moving Int Req n Int {s. metric n s < N})"
+      Lift \<in> (closed \<inter> Req n \<inter> {s. metric n s = N} \<inter> goingdown) LeadsTo  
+                   (moving \<inter> Req n \<inter> {s. metric n s < N})"
 apply (cut_tac bounded)
 apply (unfold Lift_def, ensures_tac "req_down")
 apply (auto simp add: metric_def)
@@ -365,14 +365,14 @@
 (*lem_lift_5_0 proves an intersection involving ~goingup and goingup,
   i.e. the trivial disjunction, leading to an asymmetrical proof.*)
 lemma (in Floor) E_thm16c:
-     "0<N ==> Req n Int {s. metric n s = N} <= goingup Un goingdown"
+     "0<N ==> Req n \<inter> {s. metric n s = N} \<subseteq> goingup \<union> goingdown"
 by (force simp add: metric_def)
 
 
 (*lift_5*)
 lemma (in Floor) lift_5:
-     "0<N ==> Lift : (closed Int Req n Int {s. metric n s = N}) LeadsTo    
-                     (moving Int Req n Int {s. metric n s < N})"
+     "0<N ==> Lift \<in> (closed \<inter> Req n \<inter> {s. metric n s = N}) LeadsTo    
+                     (moving \<inter> Req n \<inter> {s. metric n s < N})"
 apply (rule LeadsTo_Trans [OF subset_imp_LeadsTo
                               LeadsTo_Un [OF E_thm16a E_thm16b]])
 apply (drule E_thm16c, auto)
@@ -383,37 +383,37 @@
 
 (*lemma used to prove lem_lift_3_1*)
 lemma (in Floor) metric_eq_0D [dest]:
-     "[| metric n s = 0;  Min <= floor s;  floor s <= Max |] ==> floor s = n"
+     "[| metric n s = 0;  Min \<le> floor s;  floor s \<le> Max |] ==> floor s = n"
 by (force simp add: metric_def)
 
 
 (*lem_lift_3_1*)
-lemma (in Floor) E_thm11: "Lift : (moving Int Req n Int {s. metric n s = 0}) LeadsTo    
-                       (stopped Int atFloor n)"
+lemma (in Floor) E_thm11: "Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = 0}) LeadsTo    
+                       (stopped \<inter> atFloor n)"
 apply (cut_tac bounded)
 apply (unfold Lift_def, ensures_tac "request_act", auto)
 done
 
 (*lem_lift_3_5*)
 lemma (in Floor) E_thm13: 
-  "Lift : (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s})  
-  LeadsTo (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s})"
+  "Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> {s. floor s \<in> req s})  
+  LeadsTo (stopped \<inter> Req n \<inter> {s. metric n s = N} \<inter> {s. floor s \<in> req s})"
 apply (unfold Lift_def, ensures_tac "request_act")
 apply (auto simp add: metric_def)
 done
 
 (*lem_lift_3_6*)
 lemma (in Floor) E_thm14: "0 < N ==>  
-      Lift :  
-        (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s})  
-        LeadsTo (opened Int Req n Int {s. metric n s = N})"
+      Lift \<in>  
+        (stopped \<inter> Req n \<inter> {s. metric n s = N} \<inter> {s. floor s \<in> req s})  
+        LeadsTo (opened \<inter> Req n \<inter> {s. metric n s = N})"
 apply (unfold Lift_def, ensures_tac "open_act")
 apply (auto simp add: metric_def)
 done
 
 (*lem_lift_3_7*)
-lemma (in Floor) E_thm15: "Lift : (opened Int Req n Int {s. metric n s = N})   
-             LeadsTo (closed Int Req n Int {s. metric n s = N})"
+lemma (in Floor) E_thm15: "Lift \<in> (opened \<inter> Req n \<inter> {s. metric n s = N})   
+             LeadsTo (closed \<inter> Req n \<inter> {s. metric n s = N})"
 apply (unfold Lift_def, ensures_tac "close_act")
 apply (auto simp add: metric_def)
 done
@@ -422,15 +422,15 @@
 (** the final steps **)
 
 lemma (in Floor) lift_3_Req: "0 < N ==>  
-      Lift :  
-        (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s})    
-        LeadsTo (moving Int Req n Int {s. metric n s < N})"
+      Lift \<in>  
+        (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> {s. floor s \<in> req s})    
+        LeadsTo (moving \<inter> Req n \<inter> {s. metric n s < N})"
 apply (blast intro!: E_thm13 E_thm14 E_thm15 lift_5 intro: LeadsTo_Trans)
 done
 
 
 (*Now we observe that our integer metric is really a natural number*)
-lemma (in Floor) Always_nonneg: "Lift : Always {s. 0 <= metric n s}"
+lemma (in Floor) Always_nonneg: "Lift \<in> Always {s. 0 \<le> metric n s}"
 apply (rule bounded [THEN Always_weaken])
 apply (auto simp add: metric_def)
 done
@@ -438,10 +438,10 @@
 lemmas (in Floor) R_thm11 = Always_LeadsTo_weaken [OF Always_nonneg E_thm11]
 
 lemma (in Floor) lift_3:
-     "Lift : (moving Int Req n) LeadsTo (stopped Int atFloor n)"
+     "Lift \<in> (moving \<inter> Req n) LeadsTo (stopped \<inter> atFloor n)"
 apply (rule Always_nonneg [THEN integ_0_le_induct])
 apply (case_tac "0 < z")
-(*If z <= 0 then actually z = 0*)
+(*If z \<le> 0 then actually z = 0*)
 prefer 2 apply (force intro: R_thm11 order_antisym simp add: linorder_not_less)
 apply (rule LeadsTo_weaken_R [OF asm_rl Un_upper1])
 apply (rule LeadsTo_Trans [OF subset_imp_LeadsTo
@@ -449,7 +449,7 @@
 done
 
 
-lemma (in Floor) lift_1: "Lift : (Req n) LeadsTo (opened Int atFloor n)"
+lemma (in Floor) lift_1: "Lift \<in> (Req n) LeadsTo (opened \<inter> atFloor n)"
 apply (rule LeadsTo_Trans)
  prefer 2
  apply (rule LeadsTo_Un [OF E_thm04 LeadsTo_Un_post])