equal
deleted
inserted
replaced
217 by(simp add: \<gamma>_fun_def) |
217 by(simp add: \<gamma>_fun_def) |
218 |
218 |
219 lemma gamma_Step_subcomm: |
219 lemma gamma_Step_subcomm: |
220 assumes "!!x e S. f1 x e (\<gamma>\<^sub>o S) \<subseteq> \<gamma>\<^sub>o (f2 x e S)" "!!b S. g1 b (\<gamma>\<^sub>o S) \<subseteq> \<gamma>\<^sub>o (g2 b S)" |
220 assumes "!!x e S. f1 x e (\<gamma>\<^sub>o S) \<subseteq> \<gamma>\<^sub>o (f2 x e S)" "!!b S. g1 b (\<gamma>\<^sub>o S) \<subseteq> \<gamma>\<^sub>o (g2 b S)" |
221 shows "Step f1 g1 (\<gamma>\<^sub>o S) (\<gamma>\<^sub>c C) \<le> \<gamma>\<^sub>c (Step f2 g2 S C)" |
221 shows "Step f1 g1 (\<gamma>\<^sub>o S) (\<gamma>\<^sub>c C) \<le> \<gamma>\<^sub>c (Step f2 g2 S C)" |
222 proof(induction C arbitrary: S) |
222 by (induction C arbitrary: S) (auto simp: mono_gamma_o assms) |
223 qed (auto simp: mono_gamma_o assms) |
|
224 |
223 |
225 lemma step_step': "step (\<gamma>\<^sub>o S) (\<gamma>\<^sub>c C) \<le> \<gamma>\<^sub>c (step' S C)" |
224 lemma step_step': "step (\<gamma>\<^sub>o S) (\<gamma>\<^sub>c C) \<le> \<gamma>\<^sub>c (step' S C)" |
226 unfolding step_def step'_def |
225 unfolding step_def step'_def |
227 by(rule gamma_Step_subcomm) |
226 by(rule gamma_Step_subcomm) |
228 (auto simp: aval'_correct in_gamma_update asem_def split: option.splits) |
227 (auto simp: aval'_correct in_gamma_update asem_def split: option.splits) |