equal
deleted
inserted
replaced
140 "finfun_Ball_except xs (K$ b) P \<longleftrightarrow> \<not> b \<or> is_list_UNIV xs \<or> Code.abort (STR ''finfun_ball_except'') (\<lambda>u. finfun_Ball_except xs (K$ b) P)" |
140 "finfun_Ball_except xs (K$ b) P \<longleftrightarrow> \<not> b \<or> is_list_UNIV xs \<or> Code.abort (STR ''finfun_ball_except'') (\<lambda>u. finfun_Ball_except xs (K$ b) P)" |
141 by(auto simp add: finfun_Ball_except_def is_list_UNIV_iff) |
141 by(auto simp add: finfun_Ball_except_def is_list_UNIV_iff) |
142 |
142 |
143 lemma finfun_Ball_except_update: |
143 lemma finfun_Ball_except_update: |
144 "finfun_Ball_except xs (A(a $:= b)) P = ((a \<in> set xs \<or> (b \<longrightarrow> P a)) \<and> finfun_Ball_except (a # xs) A P)" |
144 "finfun_Ball_except xs (A(a $:= b)) P = ((a \<in> set xs \<or> (b \<longrightarrow> P a)) \<and> finfun_Ball_except (a # xs) A P)" |
145 by(fastforce simp add: finfun_Ball_except_def finfun_upd_apply split: split_if_asm) |
145 by(fastforce simp add: finfun_Ball_except_def finfun_upd_apply split: if_split_asm) |
146 |
146 |
147 lemma finfun_Ball_except_update_code [code]: |
147 lemma finfun_Ball_except_update_code [code]: |
148 fixes a :: "'a :: card_UNIV" |
148 fixes a :: "'a :: card_UNIV" |
149 shows "finfun_Ball_except xs (finfun_update_code f a b) P = ((a \<in> set xs \<or> (b \<longrightarrow> P a)) \<and> finfun_Ball_except (a # xs) f P)" |
149 shows "finfun_Ball_except xs (finfun_update_code f a b) P = ((a \<in> set xs \<or> (b \<longrightarrow> P a)) \<and> finfun_Ball_except (a # xs) f P)" |
150 by(simp add: finfun_Ball_except_update) |
150 by(simp add: finfun_Ball_except_update) |
167 "finfun_Bex_except xs (K$ b) P \<longleftrightarrow> b \<and> \<not> is_list_UNIV xs \<and> Code.abort (STR ''finfun_Bex_except'') (\<lambda>u. finfun_Bex_except xs (K$ b) P)" |
167 "finfun_Bex_except xs (K$ b) P \<longleftrightarrow> b \<and> \<not> is_list_UNIV xs \<and> Code.abort (STR ''finfun_Bex_except'') (\<lambda>u. finfun_Bex_except xs (K$ b) P)" |
168 by(auto simp add: finfun_Bex_except_def is_list_UNIV_iff) |
168 by(auto simp add: finfun_Bex_except_def is_list_UNIV_iff) |
169 |
169 |
170 lemma finfun_Bex_except_update: |
170 lemma finfun_Bex_except_update: |
171 "finfun_Bex_except xs (A(a $:= b)) P \<longleftrightarrow> (a \<notin> set xs \<and> b \<and> P a) \<or> finfun_Bex_except (a # xs) A P" |
171 "finfun_Bex_except xs (A(a $:= b)) P \<longleftrightarrow> (a \<notin> set xs \<and> b \<and> P a) \<or> finfun_Bex_except (a # xs) A P" |
172 by(fastforce simp add: finfun_Bex_except_def finfun_upd_apply dest: bspec split: split_if_asm) |
172 by(fastforce simp add: finfun_Bex_except_def finfun_upd_apply dest: bspec split: if_split_asm) |
173 |
173 |
174 lemma finfun_Bex_except_update_code [code]: |
174 lemma finfun_Bex_except_update_code [code]: |
175 fixes a :: "'a :: card_UNIV" |
175 fixes a :: "'a :: card_UNIV" |
176 shows "finfun_Bex_except xs (finfun_update_code f a b) P \<longleftrightarrow> ((a \<notin> set xs \<and> b \<and> P a) \<or> finfun_Bex_except (a # xs) f P)" |
176 shows "finfun_Bex_except xs (finfun_update_code f a b) P \<longleftrightarrow> ((a \<notin> set xs \<and> b \<and> P a) \<or> finfun_Bex_except (a # xs) f P)" |
177 by(simp add: finfun_Bex_except_update) |
177 by(simp add: finfun_Bex_except_update) |