equal
deleted
inserted
replaced
3 *) |
3 *) |
4 |
4 |
5 header {* An abstract view on maps for code generation. *} |
5 header {* An abstract view on maps for code generation. *} |
6 |
6 |
7 theory Mapping |
7 theory Mapping |
8 imports Main Quotient_Option |
8 imports Main Quotient_Option Quotient_List |
9 begin |
9 begin |
10 |
10 |
11 subsection {* Type definition and primitive operations *} |
11 subsection {* Type definition and primitive operations *} |
12 |
12 |
13 typedef ('a, 'b) mapping = "UNIV :: ('a \<rightharpoonup> 'b) set" |
13 typedef ('a, 'b) mapping = "UNIV :: ('a \<rightharpoonup> 'b) set" |
79 qed (unfold equal_mapping_def, transfer, auto) |
79 qed (unfold equal_mapping_def, transfer, auto) |
80 |
80 |
81 end |
81 end |
82 |
82 |
83 lemma [transfer_rule]: |
83 lemma [transfer_rule]: |
84 "fun_rel cr_mapping (fun_rel cr_mapping HOL.iff) HOL.eq HOL.equal" |
84 "fun_rel (pcr_mapping op= op=) (fun_rel (pcr_mapping op= op=) HOL.iff) HOL.eq HOL.equal" |
85 by (unfold equal) transfer_prover |
85 by (unfold equal) transfer_prover |
86 |
86 |
87 |
87 |
88 subsection {* Properties *} |
88 subsection {* Properties *} |
89 |
89 |