regexp: comparison prio/PrioGDef.thy

equal deleted inserted replaced

-:cab43c4a96d2
+:bc5bf9e9ada2
 {\em schedule state}. It is represented as a record consisting of
 a function assigning waiting queue to resources and a function assigning precedence to
 threads:
 *}
 record schedule_state =
-waiting_queue :: "cs \<Rightarrow> thread list" -- {* The function assigning waiting queue. *}
+wq_fun :: "cs \<Rightarrow> thread list" -- {* The function assigning waiting queue. *}
-cur_preced :: "thread \<Rightarrow> precedence" -- {* The function assigning precedence. *}
+cprec_fun :: "thread \<Rightarrow> precedence" -- {* The function assigning precedence. *}
 text {* \noindent
 The following
 @{text "cpreced s th"} gives the {\em current precedence} of thread @{text "th"} under
 state @{text "s"}. The definition of @{text "cpreced"} reflects the basic idea of
 The following function @{text "schs"} is used to calculate the schedule state @{text "schs s"}.
 It is the key function to model Priority Inheritance:
 *}
 fun schs :: "state \<Rightarrow> schedule_state"
 where
-"schs [] = (| waiting_queue = \<lambda> cs. [],  cur_preced = (\<lambda>_. Prc 0 0) |)" |
+"schs [] = (| wq_fun = \<lambda> cs. [],  cprec_fun = (\<lambda>_. Prc 0 0) |)" |
 -- {*
 \begin{minipage}{0.9\textwidth}
 \begin{enumerate}
 \item @{text "ps"} is the schedule state of last moment.
 put them in the same record so that they can evolve together.
 \end{enumerate}
 \end{minipage}
 *}
 "schs (Create th prio # s) =
-(let wq = waiting_queue (schs s) in
+(let wq = wq_fun (schs s) in
-(|waiting_queue = wq, cur_preced = cpreced wq (Create th prio # s)|))"
+(|wq_fun = wq, cprec_fun = cpreced wq (Create th prio # s)|))"
 |  "schs (Exit th # s) =
-(let wq = waiting_queue (schs s) in
+(let wq = wq_fun (schs s) in
-(|waiting_queue = wq, cur_preced = cpreced wq (Exit th # s)|))"
+(|wq_fun = wq, cprec_fun = cpreced wq (Exit th # s)|))"
 |  "schs (Set th prio # s) =
-(let wq = waiting_queue (schs s) in
+(let wq = wq_fun (schs s) in
-(|waiting_queue = wq, cur_preced = cpreced wq (Set th prio # s)|))"
+(|wq_fun = wq, cprec_fun = cpreced wq (Set th prio # s)|))"
 |  "schs (P th cs # s) =
-(let wq = waiting_queue (schs s) in
+(let wq = wq_fun (schs s) in
 let new_wq = wq(cs := (wq cs @ [th])) in
-(|waiting_queue = new_wq, cur_preced = cpreced new_wq (P th cs # s)|))"
+(|wq_fun = new_wq, cprec_fun = cpreced new_wq (P th cs # s)|))"
 |  "schs (V th cs # s) =
-(let wq = waiting_queue (schs s) in
+(let wq = wq_fun (schs s) in
 let new_wq = wq(cs := release (wq cs)) in
-(|waiting_queue = new_wq, cur_preced = cpreced new_wq (V th cs # s)|))"
+(|wq_fun = new_wq, cprec_fun = cpreced new_wq (V th cs # s)|))"
 lemma cpreced_initial:
 "cpreced (\<lambda> cs. []) [] = (\<lambda>_. (Prc 0 0))"
 apply(simp add: cpreced_def)
 apply(simp add: cs_dependents_def cs_depend_def cs_waiting_def cs_holding_def)
 apply(simp add: preced_def)
 done
 lemma sch_old_def:
 "schs (e#s) = (let ps = schs s in
-let pwq = waiting_queue ps in
+let pwq = wq_fun ps in
 let nwq = case e of
 P th cs \<Rightarrow>  pwq(cs:=(pwq cs @ [th])) |
 V th cs \<Rightarrow> let nq = case (pwq cs) of
 [] \<Rightarrow> [] |
 (_#qs) \<Rightarrow> (SOME q. distinct q \<and> set q = set qs)
 in pwq(cs:=nq)                 |
 _ \<Rightarrow> pwq
 in let ncp = cpreced nwq (e#s) in
-\<lparr>waiting_queue = nwq, cur_preced = ncp\<rparr>
+\<lparr>wq_fun = nwq, cprec_fun = ncp\<rparr>
 )"
 apply(cases e)
 apply(simp_all)
 done
 text {*
 \noindent
-The following @{text "wq"} is a shorthand for @{text "waiting_queue"}.
+The following @{text "wq"} is a shorthand for @{text "wq_fun"}.
 *}
 definition wq :: "state \<Rightarrow> cs \<Rightarrow> thread list"
-where "wq s = waiting_queue (schs s)"
+where "wq s = wq_fun (schs s)"
 text {* \noindent
-The following @{text "cp"} is a shorthand for @{text "cur_preced"}.
+The following @{text "cp"} is a shorthand for @{text "cprec_fun"}.
 *}
 definition cp :: "state \<Rightarrow> thread \<Rightarrow> precedence"
-where "cp s = cur_preced (schs s)"
+where "cp s = cprec_fun (schs s)"
 text {* \noindent
 Functions @{text "holding"}, @{text "waiting"}, @{text "depend"} and
 @{text "dependents"} still have the
 same meaning, but redefined so that they no longer depend on the

changeset 294	bc5bf9e9ada2
parent 291	5ef9f6ebe827
child 295	8e4a5fff2eda