--- a/src/HOL/Library/Mapping.thy Tue Aug 13 15:59:22 2013 +0200
+++ b/src/HOL/Library/Mapping.thy Tue Aug 13 15:59:22 2013 +0200
@@ -5,11 +5,15 @@
header {* An abstract view on maps for code generation. *}
theory Mapping
-imports Main Quotient_Option Quotient_List
+imports Main
begin
subsection {* Parametricity transfer rules *}
+context
+begin
+interpretation lifting_syntax .
+
lemma empty_transfer: "(A ===> option_rel B) Map.empty Map.empty" by transfer_prover
lemma lookup_transfer: "((A ===> B) ===> A ===> B) (\<lambda>m k. m k) (\<lambda>m k. m k)" by transfer_prover
@@ -72,6 +76,8 @@
| Some v \<Rightarrow> m (k \<mapsto> (f v))))"
by transfer_prover
+end
+
subsection {* Type definition and primitive operations *}
typedef ('a, 'b) mapping = "UNIV :: ('a \<rightharpoonup> 'b) set"
@@ -154,12 +160,17 @@
end
+context
+begin
+interpretation lifting_syntax .
+
lemma [transfer_rule]:
assumes [transfer_rule]: "bi_total A"
assumes [transfer_rule]: "bi_unique B"
- shows "fun_rel (pcr_mapping A B) (fun_rel (pcr_mapping A B) HOL.iff) HOL.eq HOL.equal"
+ shows "(pcr_mapping A B ===> pcr_mapping A B ===> op=) HOL.eq HOL.equal"
by (unfold equal) transfer_prover
+end
subsection {* Properties *}