src/HOL/Library/Mapping.thy
changeset 55525 70b7e91fa1f9
parent 55467 a5c9002bc54d
child 55938 f20d1db5aa3c
     1.1 --- a/src/HOL/Library/Mapping.thy	Sun Feb 16 21:33:28 2014 +0100
     1.2 +++ b/src/HOL/Library/Mapping.thy	Sun Feb 16 21:33:28 2014 +0100
     1.3 @@ -14,46 +14,46 @@
     1.4  begin
     1.5  interpretation lifting_syntax .
     1.6  
     1.7 -lemma empty_transfer: "(A ===> option_rel B) Map.empty Map.empty" by transfer_prover
     1.8 +lemma empty_transfer: "(A ===> rel_option B) Map.empty Map.empty" by transfer_prover
     1.9  
    1.10  lemma lookup_transfer: "((A ===> B) ===> A ===> B) (\<lambda>m k. m k) (\<lambda>m k. m k)" by transfer_prover
    1.11  
    1.12  lemma update_transfer:
    1.13    assumes [transfer_rule]: "bi_unique A"
    1.14 -  shows "(A ===> B ===> (A ===> option_rel B) ===> A ===> option_rel B) 
    1.15 +  shows "(A ===> B ===> (A ===> rel_option B) ===> A ===> rel_option B) 
    1.16            (\<lambda>k v m. m(k \<mapsto> v)) (\<lambda>k v m. m(k \<mapsto> v))"
    1.17  by transfer_prover
    1.18  
    1.19  lemma delete_transfer:
    1.20    assumes [transfer_rule]: "bi_unique A"
    1.21 -  shows "(A ===> (A ===> option_rel B) ===> A ===> option_rel B) 
    1.22 +  shows "(A ===> (A ===> rel_option B) ===> A ===> rel_option B) 
    1.23            (\<lambda>k m. m(k := None)) (\<lambda>k m. m(k := None))"
    1.24  by transfer_prover
    1.25  
    1.26  definition equal_None :: "'a option \<Rightarrow> bool" where "equal_None x \<equiv> x = None"
    1.27  
    1.28 -lemma [transfer_rule]: "(option_rel A ===> op=) equal_None equal_None" 
    1.29 -unfolding fun_rel_def option_rel_def equal_None_def by (auto split: option.split)
    1.30 +lemma [transfer_rule]: "(rel_option A ===> op=) equal_None equal_None" 
    1.31 +unfolding fun_rel_def rel_option_iff equal_None_def by (auto split: option.split)
    1.32  
    1.33  lemma dom_transfer:
    1.34    assumes [transfer_rule]: "bi_total A"
    1.35 -  shows "((A ===> option_rel B) ===> set_rel A) dom dom" 
    1.36 +  shows "((A ===> rel_option B) ===> set_rel A) dom dom" 
    1.37  unfolding dom_def[abs_def] equal_None_def[symmetric] 
    1.38  by transfer_prover
    1.39  
    1.40  lemma map_of_transfer [transfer_rule]:
    1.41    assumes [transfer_rule]: "bi_unique R1"
    1.42 -  shows "(list_all2 (prod_rel R1 R2) ===> R1 ===> option_rel R2) map_of map_of"
    1.43 +  shows "(list_all2 (prod_rel R1 R2) ===> R1 ===> rel_option R2) map_of map_of"
    1.44  unfolding map_of_def by transfer_prover
    1.45  
    1.46  lemma tabulate_transfer: 
    1.47    assumes [transfer_rule]: "bi_unique A"
    1.48 -  shows "(list_all2 A ===> (A ===> B) ===> A ===> option_rel B) 
    1.49 +  shows "(list_all2 A ===> (A ===> B) ===> A ===> rel_option B) 
    1.50      (\<lambda>ks f. (map_of (List.map (\<lambda>k. (k, f k)) ks))) (\<lambda>ks f. (map_of (List.map (\<lambda>k. (k, f k)) ks)))"
    1.51  by transfer_prover
    1.52  
    1.53  lemma bulkload_transfer: 
    1.54 -  "(list_all2 A ===> op= ===> option_rel A) 
    1.55 +  "(list_all2 A ===> op= ===> rel_option A) 
    1.56      (\<lambda>xs k. if k < length xs then Some (xs ! k) else None) (\<lambda>xs k. if k < length xs then Some (xs ! k) else None)"
    1.57  unfolding fun_rel_def 
    1.58  apply clarsimp 
    1.59 @@ -64,13 +64,13 @@
    1.60  by (auto dest: list_all2_lengthD list_all2_nthD)
    1.61  
    1.62  lemma map_transfer: 
    1.63 -  "((A ===> B) ===> (C ===> D) ===> (B ===> option_rel C) ===> A ===> option_rel D) 
    1.64 +  "((A ===> B) ===> (C ===> D) ===> (B ===> rel_option C) ===> A ===> rel_option D) 
    1.65      (\<lambda>f g m. (map_option g \<circ> m \<circ> f)) (\<lambda>f g m. (map_option g \<circ> m \<circ> f))"
    1.66  by transfer_prover
    1.67  
    1.68  lemma map_entry_transfer:
    1.69    assumes [transfer_rule]: "bi_unique A"
    1.70 -  shows "(A ===> (B ===> B) ===> (A ===> option_rel B) ===> A ===> option_rel B) 
    1.71 +  shows "(A ===> (B ===> B) ===> (A ===> rel_option B) ===> A ===> rel_option B) 
    1.72      (\<lambda>k f m. (case m k of None \<Rightarrow> m
    1.73        | Some v \<Rightarrow> m (k \<mapsto> (f v)))) (\<lambda>k f m. (case m k of None \<Rightarrow> m
    1.74        | Some v \<Rightarrow> m (k \<mapsto> (f v))))"