equal
deleted
inserted
replaced
67 "e1 +_(lift2 f) e2 == lift2 f e1 e2" |
67 "e1 +_(lift2 f) e2 == lift2 f e1 e2" |
68 by (simp add: plussub_def) |
68 by (simp add: plussub_def) |
69 |
69 |
70 |
70 |
71 lemma plus_eq_Err_conv [simp]: |
71 lemma plus_eq_Err_conv [simp]: |
72 assumes "x:A" and "y:A" |
72 assumes "x \<in> A" and "y \<in> A" |
73 and "semilat(err A, Err.le r, lift2 f)" |
73 and "semilat(err A, Err.le r, lift2 f)" |
74 shows "(x +_f y = Err) = (~(? z:A. x <=_r z & y <=_r z))" |
74 shows "(x +_f y = Err) = (\<not>(\<exists>z\<in>A. x <=_r z & y <=_r z))" |
75 proof - |
75 proof - |
76 have plus_le_conv2: |
76 have plus_le_conv2: |
77 "\<And>r f z. \<lbrakk> z : err A; semilat (err A, r, f); OK x : err A; OK y : err A; |
77 "\<And>r f z. \<lbrakk> z \<in> err A; semilat (err A, r, f); OK x \<in> err A; OK y \<in> err A; |
78 OK x +_f OK y <=_r z\<rbrakk> \<Longrightarrow> OK x <=_r z \<and> OK y <=_r z" |
78 OK x +_f OK y <=_r z\<rbrakk> \<Longrightarrow> OK x <=_r z \<and> OK y <=_r z" |
79 by (rule Semilat.plus_le_conv [OF Semilat.intro, THEN iffD1]) |
79 by (rule Semilat.plus_le_conv [OF Semilat.intro, THEN iffD1]) |
80 from assms show ?thesis |
80 from assms show ?thesis |
81 apply (rule_tac iffI) |
81 apply (rule_tac iffI) |
82 apply clarify |
82 apply clarify |
90 apply simp |
90 apply simp |
91 apply simp |
91 apply simp |
92 apply (case_tac "x +_f y") |
92 apply (case_tac "x +_f y") |
93 apply assumption |
93 apply assumption |
94 apply (rename_tac "z") |
94 apply (rename_tac "z") |
95 apply (subgoal_tac "OK z: err A") |
95 apply (subgoal_tac "OK z \<in> err A") |
96 apply (frule plus_le_conv2) |
96 apply (frule plus_le_conv2) |
97 apply assumption |
97 apply assumption |
98 apply simp |
98 apply simp |
99 apply blast |
99 apply blast |
100 apply simp |
100 apply simp |