82 apply blast+ |
82 apply blast+ |
83 done |
83 done |
84 |
84 |
85 lemma [pred_set_conv]: |
85 lemma [pred_set_conv]: |
86 "((\<lambda>x x' y y'. ((x, x'), (y, y')) \<in> R) <= (\<lambda>x x' y y'. ((x, x'), (y, y')) \<in> S)) = (R <= S)" |
86 "((\<lambda>x x' y y'. ((x, x'), (y, y')) \<in> R) <= (\<lambda>x x' y y'. ((x, x'), (y, y')) \<in> S)) = (R <= S)" |
87 by (auto simp add: le_fun_def le_bool_def mem_def) |
87 unfolding subset_eq |
|
88 by (auto simp add: le_fun_def le_bool_def) |
88 |
89 |
89 lemma [pred_set_conv]: |
90 lemma [pred_set_conv]: |
90 "((\<lambda>x x' y. ((x, x'), y) \<in> R) <= (\<lambda>x x' y. ((x, x'), y) \<in> S)) = (R <= S)" |
91 "((\<lambda>x x' y. ((x, x'), y) \<in> R) <= (\<lambda>x x' y. ((x, x'), y) \<in> S)) = (R <= S)" |
91 by (auto simp add: le_fun_def le_bool_def mem_def) |
92 unfolding subset_eq |
|
93 by (auto simp add: le_fun_def le_bool_def) |
92 |
94 |
93 text{*Command execution is functional (deterministic) provided evaluation is*} |
95 text{*Command execution is functional (deterministic) provided evaluation is*} |
94 theorem single_valued_exec: "single_valued ev ==> single_valued(exec ev)" |
96 theorem single_valued_exec: "single_valued ev ==> single_valued(exec ev)" |
95 apply (simp add: single_valued_def) |
97 apply (simp add: single_valued_def) |
96 apply (intro allI) |
98 apply (intro allI) |