equal
deleted
inserted
replaced
27 |
27 |
28 lemma PLam_empty [simp]: "PLam {} F = SKIP" |
28 lemma PLam_empty [simp]: "PLam {} F = SKIP" |
29 by (simp add: PLam_def) |
29 by (simp add: PLam_def) |
30 |
30 |
31 lemma PLam_SKIP [simp]: "(plam i : I. SKIP) = SKIP" |
31 lemma PLam_SKIP [simp]: "(plam i : I. SKIP) = SKIP" |
32 by (simp add: PLam_def lift_SKIP JN_constant) |
32 by (simp add: PLam_def JN_constant) |
33 |
33 |
34 lemma PLam_insert: "PLam (insert i I) F = (lift i (F i)) Join (PLam I F)" |
34 lemma PLam_insert: "PLam (insert i I) F = (lift i (F i)) Join (PLam I F)" |
35 by (unfold PLam_def, auto) |
35 by (unfold PLam_def, auto) |
36 |
36 |
37 lemma PLam_component_iff: "((PLam I F) \<le> H) = (\<forall>i \<in> I. lift i (F i) \<le> H)" |
37 lemma PLam_component_iff: "((PLam I F) \<le> H) = (\<forall>i \<in> I. lift i (F i) \<le> H)" |