equal
deleted
inserted
replaced
46 apply (induct rule: hfset_induct) |
46 apply (induct rule: hfset_induct) |
47 using Fold by (metis notin_fset) |
47 using Fold by (metis notin_fset) |
48 |
48 |
49 subsection{* Recursion and iteration *} |
49 subsection{* Recursion and iteration *} |
50 |
50 |
51 lemma hfset_rec: |
51 lemma hfset_fld_rec: |
52 "hfset_rec R (Fold hs) = R (map_fset <id, hfset_rec R> hs)" |
52 "hfset_fld_rec R (Fold hs) = R (map_fset <id, hfset_fld_rec R> hs)" |
53 using hfset.rec unfolding Fold_def . |
53 using hfset.fld_rec unfolding Fold_def . |
54 |
54 |
55 (* The iterator has a simpler form: *) |
55 (* The iterator has a simpler form: *) |
56 lemma hfset_iter: |
56 lemma hfset_fld_iter: |
57 "hfset_iter R (Fold hs) = R (map_fset (hfset_iter R) hs)" |
57 "hfset_fld_iter R (Fold hs) = R (map_fset (hfset_fld_iter R) hs)" |
58 using hfset.iter unfolding Fold_def . |
58 using hfset.fld_iter unfolding Fold_def . |
59 |
59 |
60 end |
60 end |