62 "!!p. basevars (rtrner ch ! p, rs!p) ==> \ |
62 "!!p. basevars (rtrner ch ! p, rs!p) ==> \ |
63 \ |- Calling ch p & (rs!p ~= #NotAResult) \ |
63 \ |- Calling ch p & (rs!p ~= #NotAResult) \ |
64 \ --> Enabled (<MemReturn ch rs p>_(rtrner ch ! p, rs!p))" |
64 \ --> Enabled (<MemReturn ch rs p>_(rtrner ch ! p, rs!p))" |
65 (K [action_simp_tac (simpset()) [MemReturn_change RSN (2,enabled_mono)] [] 1, |
65 (K [action_simp_tac (simpset()) [MemReturn_change RSN (2,enabled_mono)] [] 1, |
66 action_simp_tac (simpset() addsimps [MemReturn_def,Return_def,rtrner_def]) |
66 action_simp_tac (simpset() addsimps [MemReturn_def,Return_def,rtrner_def]) |
67 [] [base_enabled,Pair_inject] 1 |
67 [exI] [base_enabled,Pair_inject] 1 |
68 ]); |
68 ]); |
69 |
69 |
70 qed_goal "ReadInner_enabled" Memory.thy |
70 qed_goal "ReadInner_enabled" Memory.thy |
71 "!!p. basevars (rtrner ch ! p, rs!p) ==> \ |
71 "!!p. basevars (rtrner ch ! p, rs!p) ==> \ |
72 \ |- Calling ch p & (arg<ch!p> = #(read l)) --> Enabled (ReadInner ch mm rs p l)" |
72 \ |- Calling ch p & (arg<ch!p> = #(read l)) --> Enabled (ReadInner ch mm rs p l)" |
73 (fn _ => [case_tac "l : MemLoc" 1, |
73 (fn _ => [case_tac "l : MemLoc" 1, |
74 ALLGOALS |
74 ALLGOALS |
75 (action_simp_tac |
75 (force_tac (mem_css addsimps2 [ReadInner_def,GoodRead_def, |
76 (simpset() addsimps [ReadInner_def,GoodRead_def,BadRead_def, |
76 BadRead_def,RdRequest_def] |
77 RdRequest_def]) |
77 addSIs2 [exI] addSEs2 [base_enabled])) |
78 [] [base_enabled,Pair_inject]) |
|
79 ]); |
78 ]); |
80 |
79 |
81 qed_goal "WriteInner_enabled" Memory.thy |
80 qed_goal "WriteInner_enabled" Memory.thy |
82 "!!p. basevars (mm!l, rtrner ch ! p, rs!p) ==> \ |
81 "!!p. basevars (mm!l, rtrner ch ! p, rs!p) ==> \ |
83 \ |- Calling ch p & (arg<ch!p> = #(write l v)) \ |
82 \ |- Calling ch p & (arg<ch!p> = #(write l v)) \ |
84 \ --> Enabled (WriteInner ch mm rs p l v)" |
83 \ --> Enabled (WriteInner ch mm rs p l v)" |
85 (fn _ => [case_tac "l:MemLoc & v:MemVal" 1, |
84 (fn _ => [case_tac "l:MemLoc & v:MemVal" 1, |
86 ALLGOALS (action_simp_tac |
85 ALLGOALS |
87 (simpset() addsimps [WriteInner_def,GoodWrite_def,BadWrite_def, |
86 (force_tac (mem_css addsimps2 [WriteInner_def,GoodWrite_def, |
88 WrRequest_def] delsimps [disj_not1]) |
87 BadWrite_def,WrRequest_def] |
89 [] [base_enabled,Pair_inject]) |
88 addSIs2 [exI] addSEs2 [base_enabled])) |
90 ]); |
89 ]); |
91 |
90 |
92 qed_goal "ReadResult" Memory.thy |
91 qed_goal "ReadResult" Memory.thy |
93 "|- Read ch mm rs p & (!l. $(MemInv mm l)) --> (rs!p)` ~= #NotAResult" |
92 "|- Read ch mm rs p & (!l. $(MemInv mm l)) --> (rs!p)` ~= #NotAResult" |
94 (fn _ => [force_tac (mem_css addsimps2 |
93 (fn _ => [force_tac (mem_css addsimps2 |