2 theory Paper |
2 theory Paper |
3 imports "../Implementation" |
3 imports "../Implementation" |
4 "../Correctness" |
4 "../Correctness" |
5 "~~/src/HOL/Library/LaTeXsugar" |
5 "~~/src/HOL/Library/LaTeXsugar" |
6 begin |
6 begin |
|
7 |
|
8 ML {* Scan.succeed *} |
|
9 |
|
10 ML {* |
|
11 fun strip_quants ctxt trm = |
|
12 case trm of |
|
13 Const("HOL.Trueprop", _) $ t => strip_quants ctxt t |
|
14 | Const("Pure.imp", _) $ _ $ t => strip_quants ctxt t |
|
15 | Const("Pure.all", _) $ Abs(n, T, t) => |
|
16 strip_quants ctxt (subst_bound (Free (n, T), t)) |
|
17 | Const("HOL.All", _) $ Abs(n, T, t) => |
|
18 strip_quants ctxt (subst_bound (Free (n, T), t)) |
|
19 | Const("HOL.Ex", _) $ Abs(n, T, t) => |
|
20 strip_quants ctxt (subst_bound (Free (n, T), t)) |
|
21 | _ => trm |
|
22 *} |
|
23 |
|
24 |
|
25 setup {* Term_Style.setup @{binding "no_quants"} (Scan.succeed strip_quants) *} |
|
26 |
7 |
27 |
8 declare [[show_question_marks = false]] |
28 declare [[show_question_marks = false]] |
9 |
29 |
10 notation (latex output) |
30 notation (latex output) |
11 Cons ("_::_" [78,77] 73) and |
31 Cons ("_::_" [78,77] 73) and |
24 cp ("cprec") and |
44 cp ("cprec") and |
25 holdents ("resources") and |
45 holdents ("resources") and |
26 DUMMY ("\<^raw:\mbox{$\_\!\_$}>") and |
46 DUMMY ("\<^raw:\mbox{$\_\!\_$}>") and |
27 cntP ("c\<^bsub>P\<^esub>") and |
47 cntP ("c\<^bsub>P\<^esub>") and |
28 cntV ("c\<^bsub>V\<^esub>") |
48 cntV ("c\<^bsub>V\<^esub>") |
|
49 |
29 |
50 |
30 (*>*) |
51 (*>*) |
31 |
52 |
32 section {* Introduction *} |
53 section {* Introduction *} |
33 |
54 |
1019 by definition, is currently the @{term running}-thread. However, we |
1040 by definition, is currently the @{term running}-thread. However, we |
1020 are going to show in the next lemma slightly more: this running |
1041 are going to show in the next lemma slightly more: this running |
1021 thread is exactly @{term "th'"}. |
1042 thread is exactly @{term "th'"}. |
1022 |
1043 |
1023 \begin{lemma} |
1044 \begin{lemma} |
1024 If @{thm (prem 1) th_blockedE_pretty} then |
1045 If @{thm (prem 1) th_blockedE_pretty} then there exists a thread @{text "th'"} |
1025 @{thm (concl) th_blockedE_pretty}. |
1046 such that @{thm (no_quants) th_blockedE_pretty}. |
1026 \end{lemma} |
1047 \end{lemma} |
1027 |
1048 |
1028 \begin{proof} |
1049 \begin{proof} |
|
1050 We know that @{term th} cannot be in @{term readys}, because it has |
|
1051 the highest precedence and therefore must be running. This violates our |
|
1052 assumption. So by ?? we have that there must be a @{term "th'"} such that |
|
1053 @{term "th' \<in> readys (t @ s)"} and @{term "(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+"}. |
|
1054 We are going to first show that this @{term "th'"} must be running. For this we |
|
1055 need to show that @{term th'} holds the highest @{term cp}-value. |
|
1056 By ?? we know that the @{term "cp"}-value of @{term "th'"} must |
|
1057 be the highest all precedences of all thread nodes in its @{term tRAG}-subtree. |
|
1058 That is |
|
1059 |
|
1060 \begin{center} |
|
1061 @{term "cp (t @ s) th' = Max (the_preced (t @ s) ` |
|
1062 (the_thread ` subtree (tRAG (t @ s)) (Th th')))"} |
|
1063 \end{center} |
|
1064 |
|
1065 But since @{term th} is in this subtree the right-hand side is equal |
|
1066 to @{term "preced th (t @ s)"}. |
|
1067 |
1029 %Let me distinguish between cp (current precedence) and assigned precedence (the precedence the |
1068 %Let me distinguish between cp (current precedence) and assigned precedence (the precedence the |
1030 %thread ``normally'' has). |
1069 %thread ``normally'' has). |
1031 %So we want to show what the cp of th' is in state t @ s. |
1070 %So we want to show what the cp of th' is in state t @ s. |
1032 %We look at all the assingned precedences in the subgraph starting from th' |
1071 %We look at all the assingned precedences in the subgraph starting from th' |
1033 %We are looking for the maximum of these assigned precedences. |
1072 %We are looking for the maximum of these assigned precedences. |