1183 end |
1183 end |
1184 |
1184 |
1185 section {* The change of @{term RAG} *} |
1185 section {* The change of @{term RAG} *} |
1186 |
1186 |
1187 text {* |
1187 text {* |
|
1188 The whole of PIP resides on the understanding of the formation |
|
1189 of @{term RAG}. In this section, we are going to investigate how |
|
1190 @{term RAG} is changed with the execution of every event (or operation). |
|
1191 The effect of every event on @{text RAG} is derived in its respective |
|
1192 locale named @{text "RAG_es"} with all lemmas before auxiliary. |
|
1193 |
|
1194 The derivation of these @{text "RAG_es"}s forms the very basis |
|
1195 to show the well-formedness of @{term RAG}, |
|
1196 for example, @{term RAG} is finite, acyclic, and single-valued, etc. |
|
1197 |
|
1198 *} |
|
1199 |
|
1200 text {* |
1188 The following three lemmas show that @{text "RAG"} does not change |
1201 The following three lemmas show that @{text "RAG"} does not change |
1189 by the happening of @{text "Set"}, @{text "Create"} and @{text "Exit"} |
1202 by the happening of @{text "Set"}, @{text "Create"} and @{text "Exit"} |
1190 events, respectively. |
1203 events, respectively. |
1191 *} |
1204 *} |
1192 |
1205 |
1193 lemma (in valid_trace_set) RAG_unchanged [simp]: "(RAG (e # s)) = RAG s" |
1206 lemma (in valid_trace_set) RAG_es [simp]: "(RAG (e # s)) = RAG s" |
1194 by (unfold is_set s_RAG_def s_waiting_def wq_def, simp add:Let_def) |
1207 by (unfold is_set s_RAG_def s_waiting_def wq_def, simp add:Let_def) |
1195 |
1208 |
1196 lemma (in valid_trace_create) RAG_unchanged [simp]: "(RAG (e # s)) = RAG s" |
1209 lemma (in valid_trace_create) RAG_es [simp]: "(RAG (e # s)) = RAG s" |
1197 by (unfold is_create s_RAG_def s_waiting_def wq_def, simp add:Let_def) |
1210 by (unfold is_create s_RAG_def s_waiting_def wq_def, simp add:Let_def) |
1198 |
1211 |
1199 lemma (in valid_trace_exit) RAG_unchanged[simp]: "(RAG (e # s)) = RAG s" |
1212 lemma (in valid_trace_exit) RAG_es[simp]: "(RAG (e # s)) = RAG s" |
1200 by (unfold is_exit s_RAG_def s_waiting_def wq_def, simp add:Let_def) |
1213 by (unfold is_exit s_RAG_def s_waiting_def wq_def, simp add:Let_def) |
1201 |
1214 |
1202 context valid_trace_v |
1215 context valid_trace_v |
1203 begin |
1216 begin |
1204 |
1217 |
1699 qed |
1712 qed |
1700 qed |
1713 qed |
1701 qed |
1714 qed |
1702 qed |
1715 qed |
1703 |
1716 |
1704 lemma |
|
1705 finite_RAG_kept: |
|
1706 assumes "finite (RAG s)" |
|
1707 shows "finite (RAG (e#s))" |
|
1708 proof(cases "rest = []") |
|
1709 case True |
|
1710 interpret vt: valid_trace_v_e using True |
|
1711 by (unfold_locales, simp) |
|
1712 show ?thesis using assms |
|
1713 by (unfold RAG_es vt.waiting_set_eq vt.holding_set_eq, simp) |
|
1714 next |
|
1715 case False |
|
1716 interpret vt: valid_trace_v_n using False |
|
1717 by (unfold_locales, simp) |
|
1718 show ?thesis using assms |
|
1719 by (unfold RAG_es vt.waiting_set_eq vt.holding_set_eq, simp) |
|
1720 qed |
|
1721 |
|
1722 end |
1717 end |
1723 |
1718 |
1724 context valid_trace_p |
1719 context valid_trace_p |
1725 begin |
1720 begin |
1726 |
1721 |
1978 qed |
1973 qed |
1979 |
1974 |
1980 end |
1975 end |
1981 |
1976 |
1982 section {* RAG is finite *} |
1977 section {* RAG is finite *} |
|
1978 |
|
1979 context valid_trace_v |
|
1980 begin |
|
1981 |
|
1982 lemma |
|
1983 finite_RAG_kept: |
|
1984 assumes "finite (RAG s)" |
|
1985 shows "finite (RAG (e#s))" |
|
1986 proof(cases "rest = []") |
|
1987 case True |
|
1988 interpret vt: valid_trace_v_e using True |
|
1989 by (unfold_locales, simp) |
|
1990 show ?thesis using assms |
|
1991 by (unfold RAG_es vt.waiting_set_eq vt.holding_set_eq, simp) |
|
1992 next |
|
1993 case False |
|
1994 interpret vt: valid_trace_v_n using False |
|
1995 by (unfold_locales, simp) |
|
1996 show ?thesis using assms |
|
1997 by (unfold RAG_es vt.waiting_set_eq vt.holding_set_eq, simp) |
|
1998 qed |
|
1999 |
|
2000 end |
1983 |
2001 |
1984 context valid_trace |
2002 context valid_trace |
1985 begin |
2003 begin |
1986 |
2004 |
1987 lemma finite_RAG: |
2005 lemma finite_RAG: |