83 apply blast+ |
83 apply blast+ |
84 done |
84 done |
85 |
85 |
86 lemma [pred_set_conv]: |
86 lemma [pred_set_conv]: |
87 "((\<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 "((\<lambda>x x' y y'. ((x, x'), (y, y')) \<in> R) <= (\<lambda>x x' y y'. ((x, x'), (y, y')) \<in> S)) = (R <= S)" |
88 by (auto simp add: le_fun_def le_bool_def) |
88 by (auto simp add: le_fun_def le_bool_def mem_def) |
89 |
89 |
90 lemma [pred_set_conv]: |
90 lemma [pred_set_conv]: |
91 "((\<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)" |
92 by (auto simp add: le_fun_def le_bool_def) |
92 by (auto simp add: le_fun_def le_bool_def mem_def) |
93 |
93 |
94 declare [[unify_trace_bound = 30, unify_search_bound = 60]] |
94 declare [[unify_trace_bound = 30, unify_search_bound = 60]] |
95 |
95 |
96 text{*Command execution is functional (deterministic) provided evaluation is*} |
96 text{*Command execution is functional (deterministic) provided evaluation is*} |
97 theorem single_valued_exec: "single_valued ev ==> single_valued(exec ev)" |
97 theorem single_valued_exec: "single_valued ev ==> single_valued(exec ev)" |