equal
deleted
inserted
replaced
100 lemma eval_minus [simp]: |
100 lemma eval_minus [simp]: |
101 "eval (P - Q) = eval P - eval Q" |
101 "eval (P - Q) = eval P - eval Q" |
102 by (simp add: minus_pred_def) |
102 by (simp add: minus_pred_def) |
103 |
103 |
104 instance proof |
104 instance proof |
|
105 fix A::"'a pred set set" |
|
106 show "INFIMUM A Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf" |
|
107 proof (simp add: less_eq_pred_def Sup_fun_def Inf_fun_def, safe) |
|
108 fix w |
|
109 assume A: "\<forall>x\<in>A. \<exists>f\<in>x. eval f w" |
|
110 define F where "F = (\<lambda> x . SOME f . f \<in> x \<and> eval f w)" |
|
111 have [simp]: "(\<forall>f\<in> (F ` A). eval f w)" |
|
112 by (metis (no_types, lifting) A F_def image_iff some_eq_ex) |
|
113 show "\<exists>x. (\<exists>f. x = f ` A \<and> (\<forall>Y\<in>A. f Y \<in> Y)) \<and> (\<forall>f\<in>x. eval f w)" |
|
114 apply (rule_tac x = "F ` A" in exI, simp) |
|
115 using A by (metis (no_types, lifting) F_def someI)+ |
|
116 qed |
105 qed (auto intro!: pred_eqI) |
117 qed (auto intro!: pred_eqI) |
106 |
118 |
107 end |
119 end |
108 |
120 |
109 definition single :: "'a \<Rightarrow> 'a pred" where |
121 definition single :: "'a \<Rightarrow> 'a pred" where |