Gedichte Musik Bilder Quellcodebibliothek Diashow Normaldarstellung
Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/HOL/UNITY/Simple/   (Beweissystem Isabelle Version 2025-1©)  Datei vom 16.11.2025 mit Größe 15 kB image not shown  

SSL Lift.thy   Interaktion und
PortierbarkeitIsabelle

 
(*  Title:      HOL/UNITY/Simple/Lift.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1998  University of Cambridge

The Lift-Control Example.
*)

theory Lift
imports "../UNITY_Main"
begin

record state =
  floor :: "int"            \<comment> \<open>current position of the lift\<close>
  "open" :: "bool"          \<comment> \<open>whether the door is opened at floor\<close>
  stop  :: "bool"           \<comment> \<open>whether the lift is stopped at floor\<close>
  req   :: "int set"        \<comment> \<open>for each floor, whether the lift is requested\<close>
  up    :: "bool"           \<comment> \<open>current direction of movement\<close>
  move  :: "bool"           \<comment> \<open>whether moving takes precedence over opening\<close>

axiomatization
  Min :: "int" and   \<comment> \<open>least and greatest floors\<close>
  Max :: "int"       \<comment> \<open>least and greatest floors\<close>
where
  Min_le_Max [iff]: "Min \ Max"
  
  
  \<comment> \<open>Abbreviations: the "always" part\<close>
  
definition
  above :: "state set"
  where "above = {s. \i. floor s < i & i \ Max & i \ req s}"

definition
  below :: "state set"
  where "below = {s. \i. Min \ i & i < floor s & i \ req s}"

definition
  queueing :: "state set"
  where "queueing = above \ below"

definition
  goingup :: "state set"
  where "goingup = above \ ({s. up s} \ -below)"

definition
  goingdown :: "state set"
  where "goingdown = below \ ({s. ~ up s} \ -above)"

definition
  ready :: "state set"
  where "ready = {s. stop s & ~ open s & move s}"
 
  \<comment> \<open>Further abbreviations\<close>

definition
  moving :: "state set"
  where "moving = {s. ~ stop s & ~ open s}"

definition
  stopped :: "state set"
  where "stopped = {s. stop s & ~ open s & ~ move s}"

definition
  opened :: "state set"
  where "opened = {s. stop s & open s & move s}"

definition
  closed :: "state set"  \<comment> \<open>but this is the same as ready!!\<close>
  where "closed = {s. stop s & ~ open s & move s}"

definition
  atFloor :: "int => state set"
  where "atFloor n = {s. floor s = n}"

definition
  Req :: "int => state set"
  where "Req n = {s. n \ req s}"


  
  \<comment> \<open>The program\<close>
  
definition
  request_act :: "(state*state) set"
  where "request_act = {(s,s'). s' = s (|stop:=True, move:=False|)
                                  & ~ stop s & floor s \<in> req s}"

definition
  open_act :: "(state*state) set"
  where "open_act =
         {(s,s'). s' = s (|open :=True,
                           req  := req s - {floor s},
                           move := True|)
                       & stop s & ~ open s & floor s \<in> req s
                       & ~(move s & s \<in> queueing)}"

definition
  close_act :: "(state*state) set"
  where "close_act = {(s,s'). s' = s (|open := False|) & open s}"

definition
  req_up :: "(state*state) set"
  where "req_up =
         {(s,s'). s' = s (|stop  :=False,
                           floor := floor s + 1,
                           up    := True|)
                       & s \<in> (ready \<inter> goingup)}"

definition
  req_down :: "(state*state) set"
  where "req_down =
         {(s,s'). s' = s (|stop  :=False,
                           floor := floor s - 1,
                           up    := False|)
                       & s \<in> (ready \<inter> goingdown)}"

definition
  move_up :: "(state*state) set"
  where "move_up =
         {(s,s'). s' = s (|floor := floor s + 1|)
                       & ~ stop s & up s & floor s \<notin> req s}"

definition
  move_down :: "(state*state) set"
  where "move_down =
         {(s,s'). s' = s (|floor := floor s - 1|)
                       & ~ stop s & ~ up s & floor s \<notin> req s}"

definition
  button_press  :: "(state*state) set"
      \<comment> \<open>This action is omitted from prior treatments, which therefore are
        unrealistic: nobody asks the lift to do anything!  But adding this
        action invalidates many of the existing progress arguments: various
        "ensures" properties fail. Maybe it should be constrained to only
        allow button presses in the current direction of travel, like in a
        real lift.\<close>
  where "button_press =
         {(s,s'). \n. s' = s (|req := insert n (req s)|)
                        & Min \<le> n & n \<le> Max}"


definition
  Lift :: "state program"
    \<comment> \<open>for the moment, we OMIT \<open>button_press\<close>\<close>
  where "Lift = mk_total_program
                ({s. floor s = Min & ~ up s & move s & stop s &
                          ~ open s & req s = {}},
                 {request_act, open_act, close_act,
                  req_up, req_down, move_up, move_down},
                 UNIV)"


  \<comment> \<open>Invariants\<close>

definition
  bounded :: "state set"
  where "bounded = {s. Min \ floor s & floor s \ Max}"

definition
  open_stop :: "state set"
  where "open_stop = {s. open s --> stop s}"
  
definition
  open_move :: "state set"
  where "open_move = {s. open s --> move s}"
  
definition
  stop_floor :: "state set"
  where "stop_floor = {s. stop s & ~ move s --> floor s \ req s}"
  
definition
  moving_up :: "state set"
  where "moving_up = {s. ~ stop s & up s -->
                   (\<exists>f. floor s \<le> f & f \<le> Max & f \<in> req s)}"
  
definition
  moving_down :: "state set"
  where "moving_down = {s. ~ stop s & ~ up s -->
                     (\<exists>f. Min \<le> f & f \<le> floor s & f \<in> req s)}"
  
definition
  metric :: "[int,state] => int"
  where "metric =
       (%n s. if floor s < n then (if up s then n - floor s
                                  else (floor s - Min) + (n-Min))
             else
             if n < floor s then (if up s then (Max - floor s) + (Max-n)
                                  else floor s - n)
             else 0)"

locale Floor =
  fixes n
  assumes Min_le_n [iff]: "Min \ n"
      and n_le_Max [iff]: "n \ Max"

lemma not_mem_distinct: "[| x \ A; y \ A |] ==> x \ y"
by blast


declare Lift_def [THEN def_prg_Init, simp]

declare request_act_def [THEN def_act_simp, simp]
declare open_act_def [THEN def_act_simp, simp]
declare close_act_def [THEN def_act_simp, simp]
declare req_up_def [THEN def_act_simp, simp]
declare req_down_def [THEN def_act_simp, simp]
declare move_up_def [THEN def_act_simp, simp]
declare move_down_def [THEN def_act_simp, simp]
declare button_press_def [THEN def_act_simp, simp]

(*The ALWAYS properties*)
declare above_def [THEN def_set_simp, simp]
declare below_def [THEN def_set_simp, simp]
declare queueing_def [THEN def_set_simp, simp]
declare goingup_def [THEN def_set_simp, simp]
declare goingdown_def [THEN def_set_simp, simp]
declare ready_def [THEN def_set_simp, simp]

(*Basic definitions*)
declare bounded_def [simp] 
        open_stop_def [simp] 
        open_move_def [simp] 
        stop_floor_def [simp]
        moving_up_def [simp]
        moving_down_def [simp]

lemma open_stop: "Lift \ Always open_stop"
apply (rule AlwaysI, force) 
apply (unfold Lift_def, safety)
done

lemma stop_floor: "Lift \ Always stop_floor"
apply (rule AlwaysI, force) 
apply (unfold Lift_def, safety)
done

(*This one needs open_stop, which was proved above*)
lemma open_move: "Lift \ Always open_move"
apply (cut_tac open_stop)
apply (rule AlwaysI, force) 
apply (unfold Lift_def, safety)
done

lemma moving_up: "Lift \ Always moving_up"
apply (rule AlwaysI, force) 
apply (unfold Lift_def, safety)
apply (auto dest: order_le_imp_less_or_eq simp add: add1_zle_eq)
done

lemma moving_down: "Lift \ Always moving_down"
apply (rule AlwaysI, force) 
apply (unfold Lift_def, safety)
apply (blast dest: order_le_imp_less_or_eq)
done

lemma bounded: "Lift \ Always bounded"
apply (cut_tac moving_up moving_down)
apply (rule AlwaysI, force) 
apply (unfold Lift_def, safety, auto)
apply (drule not_mem_distinct, assumption, arith)+
done


subsection\<open>Progress\<close>

declare moving_def [THEN def_set_simp, simp]
declare stopped_def [THEN def_set_simp, simp]
declare opened_def [THEN def_set_simp, simp]
declare closed_def [THEN def_set_simp, simp]
declare atFloor_def [THEN def_set_simp, simp]
declare Req_def [THEN def_set_simp, simp]


text\<open>The HUG'93 paper mistakenly omits the Req n from these!\<close>

(** Lift_1 **)
lemma E_thm01: "Lift \ (stopped \ atFloor n) LeadsTo (opened \ 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 \ 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 \ 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 \ closed \ (atFloor n - queueing))
                       LeadsTo (opened \<inter> atFloor n)"
apply (unfold Lift_def, ensures_tac "open_act")
done  (*lem_lift_1_7*)


(** Lift 2.  Statements of thm05a and thm05b were wrong! **)

lemmas linorder_leI = linorder_not_less [THEN iffD1]

context Floor
begin

lemmas le_MinD = Min_le_n [THEN order_antisym]
  and Max_leD = n_le_Max [THEN [2] order_antisym]

declare le_MinD [dest!]
  and linorder_leI [THEN le_MinD, dest!]
  and Max_leD [dest!]
  and linorder_leI [THEN Max_leD, dest!]


(*lem_lift_2_0 
  NOT an ensures_tac property, but a mere inclusion
  don't know why script lift_2.uni says ENSURES*)
lemma E_thm05c: 
    "Lift \ (Req n \ closed - (atFloor n - queueing))
             LeadsTo ((closed \<inter> goingup \<inter> Req n)  \<union> 
                      (closed \<inter> goingdown \<inter> Req n))"
by (auto intro!: subset_imp_LeadsTo simp add: linorder_neq_iff)

(*lift_2*)
lemma lift_2: "Lift \ (Req n \ 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")
apply (ensures_tac "req_up", auto)
done


(** Towards lift_4 ***)
 
declare if_split_asm [split]


(*lem_lift_4_1 *)
lemma E_thm12a:
     "0 < N ==>
      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 \<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' \<le> metric n s*)
apply (erule linorder_leI [THEN order_antisym, symmetric])
apply (auto simp add: metric_def)
done


(*lem_lift_4_3 *)
lemma E_thm12b: "0 < 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' \<le> metric n s*)
apply (erule linorder_leI [THEN order_antisym, symmetric])
apply (auto simp add: metric_def)
done

(*lift_4*)
lemma lift_4:
     "0 Lift \ (moving \ Req n \ {s. metric n s = N} \
                            {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


(** towards lift_5 **)

(*lem_lift_5_3*)
lemma E_thm16a: "0
  ==> 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)
done


(*lem_lift_5_1 has ~goingup instead of goingdown*)
lemma E_thm16b: "0
      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)
done


(*lem_lift_5_0 proves an intersection involving ~goingup and goingup,
  i.e. the trivial disjunction, leading to an asymmetrical proof.*)
lemma E_thm16c:
     "0 Req n \ {s. metric n s = N} \ goingup \ goingdown"
by (force simp add: metric_def)


(*lift_5*)
lemma lift_5:
     "0 Lift \ (closed \ Req n \ {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)
done


(** towards lift_3 **)

(*lemma used to prove lem_lift_3_1*)
lemma metric_eq_0D [dest]:
     "[| metric n s = 0; Min \ floor s; floor s \ Max |] ==> floor s = n"
by (force simp add: metric_def)


(*lem_lift_3_1*)
lemma E_thm11: "Lift \ (moving \ Req n \ {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 E_thm13: 
  "Lift \ (moving \ Req n \ {s. metric n s = N} \ {s. floor s \ 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 E_thm14: "0 < 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 E_thm15: "Lift \ (opened \ Req n \ {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


(** the final steps **)

lemma lift_3_Req: "0 < 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 Always_nonneg: "Lift \ Always {s. 0 \ metric n s}"
apply (rule bounded [THEN Always_weaken])
apply (auto simp add: metric_def)
done

lemmas R_thm11 = Always_LeadsTo_weaken [OF Always_nonneg E_thm11]

lemma lift_3: "Lift \ (moving \ Req n) LeadsTo (stopped \ atFloor n)"
apply (rule Always_nonneg [THEN integ_0_le_induct])
apply (case_tac "0 < z")
(*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
                              LeadsTo_Un [OF lift_4 lift_3_Req]], auto)
done


lemma lift_1: "Lift \ (Req n) LeadsTo (opened \ atFloor n)"
apply (rule LeadsTo_Trans)
 prefer 2
 apply (rule LeadsTo_Un [OF E_thm04 LeadsTo_Un_post])
 apply (rule E_thm01 [THEN [2] LeadsTo_Trans_Un])
 apply (rule lift_3 [THEN [2] LeadsTo_Trans_Un])
 apply (rule lift_2 [THEN [2] LeadsTo_Trans_Un])
 apply (rule LeadsTo_Trans_Un [OF E_thm02 E_thm03])
apply (rule open_move [THEN Always_LeadsToI])
apply (rule Always_LeadsToI [OF open_stop subset_imp_LeadsTo], clarify)
(*The case split is not essential but makes the proof much faster.*)
apply (case_tac "open x", auto)
done

end

end

100%


¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.13Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤

*Eine klare Vorstellung vom Zielzustand




Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.