<br />
<b>Deprecated</b>:  The each() function is deprecated. This message will be suppressed on further calls in <b>/home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php</b> on line <b>456</b><br />
theory Simpson = Main:

datatype wpc = Wpair | Windex | Wdata | Wslot | Wlatest;;
datatype rpc = Rpair | Rreading | Rindex | Rread;;

types global_state = "bool * bool * (bool => bool) * (bool => bool => bool)";;
types rlocal_state = "bool * bool";;
types wlocal_state = "bool * bool";;

types rstate = "rpc * rlocal_state";;
types wstate = "wpc * wlocal_state";;

constdefs rreduce :: "(global_state * rstate) => (global_state * rstate)"
  "rreduce gspcrs == 
  let (gs,(pc,rs)) = gspcrs in
  let (reading,latest,slot,data) = gs in
  let (pair,index) = rs in
    case pc of
      Rpair => 
        let pair = latest in
          (gs,(Rreading,(pair,index)))
      | Rreading => 
        let reading = pair in
	let gs' = (reading,latest,slot,data) in
	  (gs',(Rindex,rs))
      | Rindex => 
        let index = slot pair in
          (gs,(Rread,(pair,index)))
      | Rread => (gs,(Rpair,rs))
  "
;;

constdefs wreduce :: "(global_state * wstate) => (global_state * wstate)"
  "wreduce gspcws == 
  let (gs,(pc,ws)) = gspcws in
  let (reading,latest,slot,data) = gs in
  let (pair,index) = ws in
    case pc of
      Wpair => 
        let pair = ~ reading in
          (gs,(Windex,(pair,index)))
      | Windex => 
        let index = ~ (slot pair) in
          (gs,(Wdata,(pair,index)))
      | Wdata => 
	  let data = data in 
          (* we are only interested in the mutual exclusion aspect of the algorithm, which is why we don't bother updating data *)
	  let gs = (reading,latest,slot,data) in
	    (gs,(Wslot,ws))
      | Wslot => 
	  let slot = slot(pair:=index) in
	  let gs = (reading,latest,slot,data) in
	    (gs,(Wlatest,ws))
      | Wlatest => 
          let latest = pair in
	  let gs = (reading,latest,slot,data) in
	    (gs,(Wpair,ws))
"
;;
	       
types sys_state = "global_state * wstate * rstate";;

constdefs sreduce :: "sys_state => sys_state list"
  "sreduce gswsrs == 
  let (gs,ws,rs) = gswsrs in
  let gsws's = wreduce (gs,ws) in
  let gsrs's = rreduce (gs,rs) in
    [(% (gs',ws'). (gs',ws',rs)) gsws's]@[(% (gs',rs'). (gs',ws,rs')) gsrs's]
  "
;;

constdefs sreduces :: "sys_state list => sys_state list"
  "sreduces ss == (List.concat (List.map sreduce ss))"

constdefs init_gs :: "global_state"
  "init_gs == (False,False,(% (x::bool). False), (% (x::bool). % (y::bool). False))";;

constdefs init_state :: "sys_state"
"(init_state::sys_state) == (
  let gs = init_gs in
  let ws = (Wpair,(False,False)) in
  let rs = (Rpair,(False,False)) in
    (gs,ws,rs)
)"
;;

(* auxiliary obvious invariant facts *)

(* winv basically states that the writer is the only one who updates
slot, i.e. that slot cannot change underneath writer's feet. All we
need is that in Wdata, windex is what it was set to when writer was
just in Windex, i.e. ~ (slot wpair) *)

constdefs winv :: "sys_state => bool"
  "winv s ==
  let (gs,ws,rs) = s in
  let (reading,latest,slot,data) = gs in
  let (wpc,(wpair,windex)) = ws in
  let (rpc,(rpair,rindex)) = rs in 

  ((wpc = Wdata) --> (windex = (~ (slot wpair))))"

(* rinv states a similar property, that reader is the one who updates
reading. We need that if in Rindex or Rread, then reading is what it
was set to when in Rpair, i.e. rpair *)

constdefs rinv :: "sys_state => bool"
  "rinv s ==
  let (gs,ws,rs) = s in
  let (reading,latest,slot,data) = gs in
  let (wpc,(wpair,windex)) = ws in
  let (rpc,(rpair,rindex)) = rs in 

  ((rpc : {Rindex,Rread}) --> (reading = rpair))"

lemma winv: "! s s'. winv s --> s' : set (sreduce s) --> winv s'"
  apply(intro allI impI)
  apply(clarify)
  apply(rename_tac reading latest slot data ac ad ba ae af bb ag ah ai bc aj ak bd al am be)
  apply(rename_tac wpc wpair windex ae af bb ag ah ai bc aj ak bd al am be)
  apply(rename_tac rpc rpair rindex ag ah ai bc aj ak bd al am be)
  apply(rename_tac  reading' latest' slot' data'  aj ak bd al am be)
  apply(rename_tac wpc' wpair' windex' rpc' rpair' rindex')
 
  apply(case_tac rpc)
  apply(case_tac wpc) apply(force simp add: winv_def Let_def sreduce_def rreduce_def wreduce_def)+
  apply(case_tac wpc) apply(force simp add: winv_def Let_def sreduce_def rreduce_def wreduce_def)+
  apply(case_tac wpc) apply(force simp add: winv_def Let_def sreduce_def rreduce_def wreduce_def)+
  apply(case_tac wpc) apply(force simp add: winv_def Let_def sreduce_def rreduce_def wreduce_def)+
  done

lemma rinv: "! s s'. rinv s --> s' : set (sreduce s) --> rinv s'"
  apply(intro allI impI)
  apply(clarify)
  apply(rename_tac reading latest slot data ac ad ba ae af bb ag ah ai bc aj ak bd al am be)
  apply(rename_tac wpc wpair windex ae af bb ag ah ai bc aj ak bd al am be)
  apply(rename_tac rpc rpair rindex ag ah ai bc aj ak bd al am be)
  apply(rename_tac  reading' latest' slot' data'  aj ak bd al am be)
  apply(rename_tac wpc' wpair' windex' rpc' rpair' rindex')
 
  apply(case_tac rpc)
  apply(case_tac wpc) apply(force simp add: rinv_def Let_def sreduce_def rreduce_def wreduce_def)+
  apply(case_tac wpc) apply(force simp add: rinv_def Let_def sreduce_def rreduce_def wreduce_def)+
  apply(case_tac wpc) apply(force simp add: rinv_def Let_def sreduce_def rreduce_def wreduce_def)+
  apply(case_tac wpc) apply(force simp add: rinv_def Let_def sreduce_def rreduce_def wreduce_def)+
  done

(* invariant 
    
    Note that we can't just state the mutual exclusion property,
    because this is not invariant. However, if we look at the state
    that the reader and the writer could be in immediately before they
    move to reading/writing, we can extend the invariant in the
    obvious way. Surprisingly(?) this simple syntactic strengthening
    is the right invariant to have, that is, the strengthening is
    clearly necessary, and it also turns out to be sufficient.  *)

constdefs inv :: "sys_state => bool"  
  "inv s == 
  let (gs,ws,rs) = s in
  let (reading,latest,slot,data) = gs in
  let (wpc,(wpair,windex)) = ws in
  let (rpc,(rpair,rindex)) = rs in 

  let rindex' = (if rpc = Rindex then slot rpair else rindex) in
  let windex' = (if wpc = Windex then ~ (slot wpair) else windex) in
  
  ~ (
  (wpc : {Windex,Wdata})
  & (rpc : {Rindex,Rread})
  & ((wpair,windex') = (rpair,rindex'))

  )
  "

(* if (wpc,rpc) = (Wdata,Rread), this is just out mutual exclusion
property. If rpc = Rindex, and r takes a step, and we want the mutual
exclusion property to hold, we have to place a condition on (slot
rpair), i.e. the value that rindex is about to be set to. Similarly if
wpc = Windex, then we must place a condition on ~(slot wpair),
i.e. the value that windex is about to be set to. *)

lemma disjI2': "(~ A ==> B) ==> (A | B)" by blast

lemmas ss = inv_def Let_def sreduce_def rreduce_def wreduce_def

lemma inv: "! s s'. (inv s & winv s & rinv s) --> s' : set (sreduce s) --> inv s'"
  apply(intro allI impI)
  apply(clarify)
  apply(rename_tac reading latest slot data ac ad ba ae af bb ag ah ai bc aj ak bd al am be)
  apply(rename_tac wpc wpair windex ae af bb ag ah ai bc aj ak bd al am be)
  apply(rename_tac rpc rpair rindex ag ah ai bc aj ak bd al am be)
  apply(rename_tac  reading' latest' slot' data'  aj ak bd al am be)
  apply(rename_tac wpc' wpair' windex' rpc' rpair' rindex')

  apply(simp add: sreduce_def Let_def)
  apply(erule disjE)

  (* w takes a step *)
  apply(simp add: wreduce_def)
  apply(case_tac wpc)

  (* Wpair -> Windex *) 
  apply(case_tac rpc) 
  (* Rpair *)apply(simp add: ss)
  (* Rreading *)apply(simp add: ss) 
  (* Rindex *)apply(simp add: rinv_def ss) 
  (* Rread *)apply(simp add: rinv_def ss) 

  (* Windex -> Wdata *)
  apply(simp add: ss)

  (* Wdata -> Wslot *)
  apply(simp add: ss)
  
  (* Wslot -> Wlatest *)
  apply(simp add: ss)

  (* Wlatest -> Wpair *)
  apply(simp add: ss)

  (* r takes a step *)
  apply(simp add: rreduce_def)
  apply(case_tac rpc)

  (* Rpair -> Rreading *)
  apply(simp add: ss)
  
  (* Rreading -> Rindex *)
  apply(case_tac wpc)
  (* Wpair *) apply(simp add: ss) 
  (* Windex *) apply(simp add: ss) apply(rule disjI2') apply(simp) 
  (* remember, we are not even splitting on booleans, so this use of classical disjI2' still makes for a really very weak proof *)
  (* Wdata *) apply(simp add: winv_def ss) apply(rule disjI2') apply(simp)
  (* Wslot *) apply(simp add: ss)
  (* Wlatest *) apply(simp add: ss)

  (* Rindex -> Rread *)
  apply(simp add: ss)

  (* Rread -> Rpair *)
  apply(simp add: ss)
  done

  (* N.B. this proof uses nothing more powerful than simp... there is
  no force or equivalent here. This really is an extremely weak
  proof. *)

lemma inv_winv_rinv: "! s s'. (inv s & winv s & rinv s) --> s' : set (sreduce s) --> (inv s' & winv s' & rinv s')"
  using inv winv rinv apply(blast)
  done

(* define an execution *)
types exec = "nat => sys_state"

constdefs is_exec :: "exec => bool"
  "is_exec e == (e 0 = init_state)
  & (! n. (e (n+1)) : set (sreduce (e n)))"

(* the system satisfies the mutual exclusion property if the reader
and writer are not both trying to access the same part of the data
array *)

constdefs mutual_exclusion :: "sys_state => bool"
  "mutual_exclusion s == 
  let (gs,ws,rs) = s in
  let (wpc,(wpair,windex)) = ws in
  let (rpc,(rpair,rindex)) = rs in 
  
  ~ (
  (wpc = Wdata)
  & (rpc = Rread)
  & ((wpair,windex) = (rpair,rindex))
  )"

lemma correct: "! e. is_exec e --> (! n. mutual_exclusion (e n))"  
  apply(rule, rule)
  apply(subgoal_tac "! n. inv (e n) & winv (e n) & rinv (e n)")
  apply(subgoal_tac "! f. inv f --> mutual_exclusion f")
  apply(blast)
  apply(intro allI impI) apply(force simp add: inv_def mutual_exclusion_def Let_def)
  apply(rule, induct_tac n)
  apply(simp add: is_exec_def inv_def winv_def rinv_def init_state_def init_gs_def Let_def)
  apply(simp add: is_exec_def)
  apply(elim conjE) apply(drule_tac x=na in spec)
  apply(insert inv_winv_rinv) apply(blast)
  done

end