# Theory Lift

Up to index of Isabelle/HOL/UNITY

theory Lift
imports UNITY_Main
begin

    (*  Title:      HOL/UNITY/Lift.thy
        ID:         $Id: Lift.thy,v 1.8 2005/06/02 11:47:08 paulson Exp $
        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"            --{*current position of the lift*}
      "open" :: "bool"          --{*whether the door is opened at floor*}
      stop  :: "bool"           --{*whether the lift is stopped at floor*}
      req   :: "int set"        --{*for each floor, whether the lift is requested*}
      up    :: "bool"           --{*current direction of movement*}
      move  :: "bool"           --{*whether moving takes precedence over opening*}

    consts
      Min :: "int"       --{*least and greatest floors*}
      Max :: "int"       --{*least and greatest floors*}

    axioms
      Min_le_Max [iff]: "Min ≤ Max"

    constdefs

      --{*Abbreviations: the "always" part*}

      above :: "state set"
        "above == {s. ∃i. floor s < i & i ≤ Max & i ∈ req s}"

      below :: "state set"
        "below == {s. ∃i. Min ≤ i & i < floor s & i ∈ req s}"

      queueing :: "state set"
        "queueing == above ∪ below"

      goingup :: "state set"
        "goingup   == above ∩ ({s. up s}  ∪ -below)"

      goingdown :: "state set"
        "goingdown == below ∩ ({s. ~ up s} ∪ -above)"

      ready :: "state set"
        "ready == {s. stop s & ~ open s & move s}"

      --{*Further abbreviations*}

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

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

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

      closed :: "state set"  --{*but this is the same as ready!!*}
        "closed ==  {s. stop s  & ~ open s &  move s}"

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

      Req :: "int => state set"
        "Req n ==  {s. n ∈ req s}"

      --{*The program*}

      request_act :: "(state*state) set"
        "request_act == {(s,s'). s' = s (|stop:=True, move:=False|)
                                      & ~ stop s & floor s ∈ 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)}"

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

      req_up :: "(state*state) set"
        "req_up ==
             {(s,s'). s' = s (|stop  :=False,
                               floor := floor s + 1,
                               up    := True|)
                           & s ∈ (ready ∩ goingup)}"

      req_down :: "(state*state) set"
        "req_down ==
             {(s,s'). s' = s (|stop  :=False,
                               floor := floor s - 1,
                               up    := False|)
                           & s ∈ (ready ∩ goingdown)}"

      move_up :: "(state*state) set"
        "move_up ==
             {(s,s'). s' = s (|floor := floor s + 1|)
                           & ~ stop s & up s & floor s ∉ 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}"

      button_press  :: "(state*state) set"
          --{*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.*}
        "button_press ==
             {(s,s'). ∃n. s' = s (|req := insert n (req s)|)
                            & Min ≤ n & n ≤ Max}"

      Lift :: "state program"
        --{*for the moment, we OMIT @{text button_press}*}
        "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)"

      --{*Invariants*}

      bounded :: "state set"
        "bounded == {s. Min ≤ floor s & floor s ≤ Max}"

      open_stop :: "state set"
        "open_stop == {s. open s --> stop s}"

      open_move :: "state set"
        "open_move == {s. open s --> move s}"

      stop_floor :: "state set"
        "stop_floor == {s. stop s & ~ move s --> floor s ∈ req s}"

      moving_up :: "state set"
        "moving_up == {s. ~ stop s & up s -->
                       (∃f. floor s ≤ f & f ≤ Max & f ∈ req s)}"

      moving_down :: "state set"
        "moving_down == {s. ~ stop s & ~ up s -->
                         (∃f. Min ≤ f & f ≤ floor s & f ∈ req s)}"

      metric :: "[int,state] => int"
        "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{*Progress*}

    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{*The HUG'93 paper mistakenly omits the Req n from these!*}

    (** 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 ∩ 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 ∩ 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 ∩ 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]

    lemmas (in Floor) le_MinD = Min_le_n [THEN order_antisym]
                  and Max_leD = n_le_Max [THEN [2] order_antisym]

    declare (in Floor) 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 (in Floor) E_thm05c:
        "Lift ∈ (Req n ∩ closed - (atFloor n - queueing))
                 LeadsTo ((closed ∩ goingup ∩ Req n)  ∪
                          (closed ∩ goingdown ∩ Req n))"
    by (auto intro!: subset_imp_LeadsTo simp add: linorder_neq_iff)

    (*lift_2*)
    lemma (in Floor) lift_2: "Lift ∈ (Req n ∩ closed - (atFloor n - queueing))
                 LeadsTo (moving ∩ 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 split_if_asm [split]

    (*lem_lift_4_1 *)
    lemma (in Floor) E_thm12a:
         "0 < N ==>
          Lift ∈ (moving ∩ Req n ∩ {s. metric n s = N} ∩
                  {s. floor s ∉ req s} ∩ {s. up s})
                 LeadsTo
                   (moving ∩ Req n ∩ {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*)
    apply (erule linorder_leI [THEN order_antisym, symmetric])
    apply (auto simp add: metric_def)
    done

    (*lem_lift_4_3 *)
    lemma (in Floor) E_thm12b: "0 < N ==>
          Lift ∈ (moving ∩ Req n ∩ {s. metric n s = N} ∩
                  {s. floor s ∉ req s} - {s. up s})
                 LeadsTo (moving ∩ Req n ∩ {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*)
    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 ∩ Req n ∩ {s. metric n s = N} ∩
                                {s. floor s ∉ req s}) LeadsTo
                               (moving ∩ Req n ∩ {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 (in Floor) E_thm16a: "0<N
      ==> Lift ∈ (closed ∩ Req n ∩ {s. metric n s = N} ∩ goingup) LeadsTo
                 (moving ∩ Req n ∩ {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 (in Floor) E_thm16b: "0<N ==>
          Lift ∈ (closed ∩ Req n ∩ {s. metric n s = N} ∩ goingdown) LeadsTo
                       (moving ∩ Req n ∩ {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 (in Floor) E_thm16c:
         "0<N ==> Req n ∩ {s. metric n s = N} ⊆ goingup ∪ goingdown"
    by (force simp add: metric_def)

    (*lift_5*)
    lemma (in Floor) lift_5:
         "0<N ==> Lift ∈ (closed ∩ Req n ∩ {s. metric n s = N}) LeadsTo
                         (moving ∩ Req n ∩ {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 (in Floor) 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 (in Floor) E_thm11: "Lift ∈ (moving ∩ Req n ∩ {s. metric n s = 0}) LeadsTo
                           (stopped ∩ 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 ∩ Req n ∩ {s. metric n s = N} ∩ {s. floor s ∈ req s})
      LeadsTo (stopped ∩ Req n ∩ {s. metric n s = N} ∩ {s. floor s ∈ 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 ∩ Req n ∩ {s. metric n s = N} ∩ {s. floor s ∈ req s})
            LeadsTo (opened ∩ Req n ∩ {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 ∩ Req n ∩ {s. metric n s = N})
                 LeadsTo (closed ∩ Req n ∩ {s. metric n s = N})"
    apply (unfold Lift_def, ensures_tac "close_act")
    apply (auto simp add: metric_def)
    done

    (** the final steps **)

    lemma (in Floor) lift_3_Req: "0 < N ==>
          Lift ∈
            (moving ∩ Req n ∩ {s. metric n s = N} ∩ {s. floor s ∈ req s})
            LeadsTo (moving ∩ Req n ∩ {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}"
    apply (rule bounded [THEN Always_weaken])
    apply (auto simp add: metric_def)
    done

    lemmas (in Floor) R_thm11 = Always_LeadsTo_weaken [OF Always_nonneg E_thm11]

    lemma (in Floor) 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 ≤ 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 (in Floor) 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

lemma not_mem_distinct:

      [| x ∉ A; y ∈ A |] ==> x ≠ y

lemma open_stop:

      Lift ∈ Always open_stop

lemma stop_floor:

      Lift ∈ Always stop_floor

lemma open_move:

      Lift ∈ Always open_move

lemma moving_up:

      Lift ∈ Always moving_up

lemma moving_down:

      Lift ∈ Always moving_down

lemma bounded:

      Lift ∈ Always bounded

### Progress

lemma E_thm01:

      Lift ∈ stopped ∩ atFloor n LeadsTo opened ∩ atFloor n

lemma E_thm02:

      Lift ∈ Req n ∩ stopped - atFloor n LeadsTo Req n ∩ opened - atFloor n

lemma E_thm03:

      Lift
      ∈ Req n ∩ opened - atFloor n LeadsTo
        Req n ∩ Lift.closed - (atFloor n - queueing)

lemma E_thm04:

      Lift ∈ Req n ∩ Lift.closed ∩ (atFloor n - queueing) LeadsTo opened ∩ atFloor n

lemmas linorder_leI:

      ¬ x1 < y1 ==> y1 ≤ x1

lemmas linorder_leI:

      ¬ x1 < y1 ==> y1 ≤ x1

lemmas le_MinD:

      [| Floor n; n ≤ Lift.Min |] ==> Lift.Min = n

and Max_leD:

      [| Floor n; Lift.Max ≤ n |] ==> Lift.Max = n

lemma E_thm05c:

      Floor n
      ==> Lift
          ∈ Req n ∩ Lift.closed - (atFloor n - queueing) LeadsTo
            Lift.closed ∩ goingup ∩ Req n ∪ Lift.closed ∩ goingdown ∩ Req n

lemma lift_2:

      Floor n
      ==> Lift ∈ Req n ∩ Lift.closed - (atFloor n - queueing) LeadsTo moving ∩ Req n

lemma E_thm12a:

      [| Floor n; 0 < N |]
      ==> Lift
          ∈ moving ∩ Req n ∩ {s. metric n s = N} ∩ {s. floor s ∉ req s} ∩
            {s. up s} LeadsTo
            moving ∩ Req n ∩ {s. metric n s < N}

lemma E_thm12b:

      [| Floor n; 0 < N |]
      ==> Lift
          ∈ moving ∩ Req n ∩ {s. metric n s = N} ∩ {s. floor s ∉ req s} -
            {s. up s} LeadsTo
            moving ∩ Req n ∩ {s. metric n s < N}

lemma lift_4:

      [| Floor n; 0 < N |]
      ==> Lift
          ∈ moving ∩ Req n ∩ {s. metric n s = N} ∩ {s. floor s ∉ req s} LeadsTo
            moving ∩ Req n ∩ {s. metric n s < N}

lemma E_thm16a:

      [| Floor n; 0 < N |]
      ==> Lift
          ∈ Lift.closed ∩ Req n ∩ {s. metric n s = N} ∩ goingup LeadsTo
            moving ∩ Req n ∩ {s. metric n s < N}

lemma E_thm16b:

      [| Floor n; 0 < N |]
      ==> Lift
          ∈ Lift.closed ∩ Req n ∩ {s. metric n s = N} ∩ goingdown LeadsTo
            moving ∩ Req n ∩ {s. metric n s < N}

lemma E_thm16c:

      [| Floor n; 0 < N |] ==> Req n ∩ {s. metric n s = N} ⊆ goingup ∪ goingdown

lemma lift_5:

      [| Floor n; 0 < N |]
      ==> Lift
          ∈ Lift.closed ∩ Req n ∩ {s. metric n s = N} LeadsTo
            moving ∩ Req n ∩ {s. metric n s < N}

lemma metric_eq_0D:

      [| Floor n; metric n s = 0; Lift.Min ≤ floor s; floor s ≤ Lift.Max |]
      ==> floor s = n

lemma E_thm11:

      Floor n
      ==> Lift ∈ moving ∩ Req n ∩ {s. metric n s = 0} LeadsTo stopped ∩ atFloor n

lemma E_thm13:

      Floor n
      ==> Lift
          ∈ moving ∩ Req n ∩ {s. metric n s = N} ∩ {s. floor s ∈ req s} LeadsTo
            stopped ∩ Req n ∩ {s. metric n s = N} ∩ {s. floor s ∈ req s}

lemma E_thm14:

      [| Floor n; 0 < N |]
      ==> Lift
          ∈ stopped ∩ Req n ∩ {s. metric n s = N} ∩ {s. floor s ∈ req s} LeadsTo
            opened ∩ Req n ∩ {s. metric n s = N}

lemma E_thm15:

      Floor n
      ==> Lift
          ∈ opened ∩ Req n ∩ {s. metric n s = N} LeadsTo
            Lift.closed ∩ Req n ∩ {s. metric n s = N}

lemma lift_3_Req:

      [| Floor n; 0 < N |]
      ==> Lift
          ∈ moving ∩ Req n ∩ {s. metric n s = N} ∩ {s. floor s ∈ req s} LeadsTo
            moving ∩ Req n ∩ {s. metric n s < N}

lemma Always_nonneg:

      Floor n ==> Lift ∈ Always {s. 0 ≤ metric n s}

lemmas R_thm11:

      [| Floor n; {s. 0 ≤ metric n s} ∩ B ⊆ moving ∩ Req n ∩ {s. metric n s = 0};
         {s. 0 ≤ metric n s} ∩ (stopped ∩ atFloor n) ⊆ B' |]
      ==> Lift ∈ B LeadsTo B'

lemma lift_3:

      Floor n ==> Lift ∈ moving ∩ Req n LeadsTo stopped ∩ atFloor n

lemma lift_1:

      Floor n ==> Lift ∈ Req n LeadsTo opened ∩ atFloor n