equal
deleted
inserted
replaced
243 |
243 |
244 lemma cons_left_idem: |
244 lemma cons_left_idem: |
245 "x # x # xs \<approx> x # xs" |
245 "x # x # xs \<approx> x # xs" |
246 by auto |
246 by auto |
247 |
247 |
248 lemma none_mem_nil: |
248 lemma none_memb_nil: |
249 "(\<forall>x. x \<notin> set xs) = (xs \<approx> [])" |
249 "(\<forall>x. \<not> memb x xs) = (xs \<approx> [])" |
250 by simp |
250 by (simp add: memb_def) |
251 |
251 |
252 lemma fset_raw_strong_cases: |
252 lemma fset_raw_strong_cases: |
253 "(xs = []) \<or> (\<exists>x ys. ((\<not> memb x ys) \<and> (xs \<approx> x # ys)))" |
253 "(xs = []) \<or> (\<exists>x ys. ((\<not> memb x ys) \<and> (xs \<approx> x # ys)))" |
254 apply (induct xs) |
254 apply (induct xs) |
255 apply (simp) |
255 apply (simp) |
337 done |
337 done |
338 |
338 |
339 lemma ffold_raw_rsp_pre: |
339 lemma ffold_raw_rsp_pre: |
340 "\<forall>e. memb e a = memb e b \<Longrightarrow> ffold_raw f z a = ffold_raw f z b" |
340 "\<forall>e. memb e a = memb e b \<Longrightarrow> ffold_raw f z a = ffold_raw f z b" |
341 apply (induct a arbitrary: b) |
341 apply (induct a arbitrary: b) |
342 apply (simp add: hd_in_set memb_absorb memb_def none_mem_nil) |
342 apply (simp add: hd_in_set memb_absorb memb_def none_memb_nil) |
343 apply (simp add: ffold_raw.simps) |
343 apply (simp add: ffold_raw.simps) |
344 apply (rule conjI) |
344 apply (rule conjI) |
345 apply (rule_tac [!] impI) |
345 apply (rule_tac [!] impI) |
346 apply (rule_tac [!] conjI) |
346 apply (rule_tac [!] conjI) |
347 apply (rule_tac [!] impI) |
347 apply (rule_tac [!] impI) |
484 lemma in_fset_to_set: |
484 lemma in_fset_to_set: |
485 "x \<in> fset_to_set S \<equiv> x |\<in>| S" |
485 "x \<in> fset_to_set S \<equiv> x |\<in>| S" |
486 by (lifting memb_def[symmetric]) |
486 by (lifting memb_def[symmetric]) |
487 |
487 |
488 lemma none_fin_fempty: |
488 lemma none_fin_fempty: |
489 "(\<forall>x. x \<notin> fset_to_set S) = (S = {||})" |
489 "(\<forall>x. x |\<notin>| S) = (S = {||})" |
490 by (lifting none_mem_nil) |
490 by (lifting none_memb_nil) |
491 |
491 |
492 lemma fset_cong: |
492 lemma fset_cong: |
493 "(fset_to_set S = fset_to_set T) = (S = T)" |
493 "(fset_to_set S = fset_to_set T) = (S = T)" |
494 by (lifting set_cong) |
494 by (lifting set_cong) |
495 |
495 |