folded 'rel_option' into 'option_rel'
authorblanchet
Sun Feb 16 21:33:28 2014 +0100 (2014-02-16)
changeset 5552570b7e91fa1f9
parent 55524 f41ef840f09d
child 55526 39708e59f4b0
folded 'rel_option' into 'option_rel'
NEWS
src/HOL/Library/Mapping.thy
src/HOL/Library/Quotient_Option.thy
src/HOL/Lifting_Option.thy
src/HOL/List.thy
     1.1 --- a/NEWS	Sun Feb 16 21:33:28 2014 +0100
     1.2 +++ b/NEWS	Sun Feb 16 21:33:28 2014 +0100
     1.3 @@ -135,6 +135,7 @@
     1.4    Renamed constants:
     1.5      Option.set ~> set_option
     1.6      Option.map ~> map_option
     1.7 +    option_rel ~> rel_option
     1.8    Renamed theorems:
     1.9      map_def ~> map_rec[abs_def]
    1.10      Option.map_def ~> map_option_case[abs_def] (with "case_option" instead of "rec_option")
     2.1 --- a/src/HOL/Library/Mapping.thy	Sun Feb 16 21:33:28 2014 +0100
     2.2 +++ b/src/HOL/Library/Mapping.thy	Sun Feb 16 21:33:28 2014 +0100
     2.3 @@ -14,46 +14,46 @@
     2.4  begin
     2.5  interpretation lifting_syntax .
     2.6  
     2.7 -lemma empty_transfer: "(A ===> option_rel B) Map.empty Map.empty" by transfer_prover
     2.8 +lemma empty_transfer: "(A ===> rel_option B) Map.empty Map.empty" by transfer_prover
     2.9  
    2.10  lemma lookup_transfer: "((A ===> B) ===> A ===> B) (\<lambda>m k. m k) (\<lambda>m k. m k)" by transfer_prover
    2.11  
    2.12  lemma update_transfer:
    2.13    assumes [transfer_rule]: "bi_unique A"
    2.14 -  shows "(A ===> B ===> (A ===> option_rel B) ===> A ===> option_rel B) 
    2.15 +  shows "(A ===> B ===> (A ===> rel_option B) ===> A ===> rel_option B) 
    2.16            (\<lambda>k v m. m(k \<mapsto> v)) (\<lambda>k v m. m(k \<mapsto> v))"
    2.17  by transfer_prover
    2.18  
    2.19  lemma delete_transfer:
    2.20    assumes [transfer_rule]: "bi_unique A"
    2.21 -  shows "(A ===> (A ===> option_rel B) ===> A ===> option_rel B) 
    2.22 +  shows "(A ===> (A ===> rel_option B) ===> A ===> rel_option B) 
    2.23            (\<lambda>k m. m(k := None)) (\<lambda>k m. m(k := None))"
    2.24  by transfer_prover
    2.25  
    2.26  definition equal_None :: "'a option \<Rightarrow> bool" where "equal_None x \<equiv> x = None"
    2.27  
    2.28 -lemma [transfer_rule]: "(option_rel A ===> op=) equal_None equal_None" 
    2.29 -unfolding fun_rel_def option_rel_def equal_None_def by (auto split: option.split)
    2.30 +lemma [transfer_rule]: "(rel_option A ===> op=) equal_None equal_None" 
    2.31 +unfolding fun_rel_def rel_option_iff equal_None_def by (auto split: option.split)
    2.32  
    2.33  lemma dom_transfer:
    2.34    assumes [transfer_rule]: "bi_total A"
    2.35 -  shows "((A ===> option_rel B) ===> set_rel A) dom dom" 
    2.36 +  shows "((A ===> rel_option B) ===> set_rel A) dom dom" 
    2.37  unfolding dom_def[abs_def] equal_None_def[symmetric] 
    2.38  by transfer_prover
    2.39  
    2.40  lemma map_of_transfer [transfer_rule]:
    2.41    assumes [transfer_rule]: "bi_unique R1"
    2.42 -  shows "(list_all2 (prod_rel R1 R2) ===> R1 ===> option_rel R2) map_of map_of"
    2.43 +  shows "(list_all2 (prod_rel R1 R2) ===> R1 ===> rel_option R2) map_of map_of"
    2.44  unfolding map_of_def by transfer_prover
    2.45  
    2.46  lemma tabulate_transfer: 
    2.47    assumes [transfer_rule]: "bi_unique A"
    2.48 -  shows "(list_all2 A ===> (A ===> B) ===> A ===> option_rel B) 
    2.49 +  shows "(list_all2 A ===> (A ===> B) ===> A ===> rel_option B) 
    2.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)))"
    2.51  by transfer_prover
    2.52  
    2.53  lemma bulkload_transfer: 
    2.54 -  "(list_all2 A ===> op= ===> option_rel A) 
    2.55 +  "(list_all2 A ===> op= ===> rel_option A) 
    2.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)"
    2.57  unfolding fun_rel_def 
    2.58  apply clarsimp 
    2.59 @@ -64,13 +64,13 @@
    2.60  by (auto dest: list_all2_lengthD list_all2_nthD)
    2.61  
    2.62  lemma map_transfer: 
    2.63 -  "((A ===> B) ===> (C ===> D) ===> (B ===> option_rel C) ===> A ===> option_rel D) 
    2.64 +  "((A ===> B) ===> (C ===> D) ===> (B ===> rel_option C) ===> A ===> rel_option D) 
    2.65      (\<lambda>f g m. (map_option g \<circ> m \<circ> f)) (\<lambda>f g m. (map_option g \<circ> m \<circ> f))"
    2.66  by transfer_prover
    2.67  
    2.68  lemma map_entry_transfer:
    2.69    assumes [transfer_rule]: "bi_unique A"
    2.70 -  shows "(A ===> (B ===> B) ===> (A ===> option_rel B) ===> A ===> option_rel B) 
    2.71 +  shows "(A ===> (B ===> B) ===> (A ===> rel_option B) ===> A ===> rel_option B) 
    2.72      (\<lambda>k f m. (case m k of None \<Rightarrow> m
    2.73        | Some v \<Rightarrow> m (k \<mapsto> (f v)))) (\<lambda>k f m. (case m k of None \<Rightarrow> m
    2.74        | Some v \<Rightarrow> m (k \<mapsto> (f v))))"
     3.1 --- a/src/HOL/Library/Quotient_Option.thy	Sun Feb 16 21:33:28 2014 +0100
     3.2 +++ b/src/HOL/Library/Quotient_Option.thy	Sun Feb 16 21:33:28 2014 +0100
     3.3 @@ -10,55 +10,57 @@
     3.4  
     3.5  subsection {* Rules for the Quotient package *}
     3.6  
     3.7 -lemma option_rel_map1:
     3.8 -  "option_rel R (map_option f x) y \<longleftrightarrow> option_rel (\<lambda>x. R (f x)) x y"
     3.9 -  by (simp add: option_rel_def split: option.split)
    3.10 +lemma rel_option_map1:
    3.11 +  "rel_option R (map_option f x) y \<longleftrightarrow> rel_option (\<lambda>x. R (f x)) x y"
    3.12 +  by (simp add: rel_option_iff split: option.split)
    3.13  
    3.14 -lemma option_rel_map2:
    3.15 -  "option_rel R x (map_option f y) \<longleftrightarrow> option_rel (\<lambda>x y. R x (f y)) x y"
    3.16 -  by (simp add: option_rel_def split: option.split)
    3.17 +lemma rel_option_map2:
    3.18 +  "rel_option R x (map_option f y) \<longleftrightarrow> rel_option (\<lambda>x y. R x (f y)) x y"
    3.19 +  by (simp add: rel_option_iff split: option.split)
    3.20  
    3.21  declare
    3.22    map_option.id [id_simps]
    3.23 -  option_rel_eq [id_simps]
    3.24 +  rel_option_eq [id_simps]
    3.25  
    3.26  lemma option_symp:
    3.27 -  "symp R \<Longrightarrow> symp (option_rel R)"
    3.28 -  unfolding symp_def split_option_all option_rel_simps by fast
    3.29 +  "symp R \<Longrightarrow> symp (rel_option R)"
    3.30 +  unfolding symp_def split_option_all
    3.31 +  by (simp only: option.rel_inject option.rel_distinct) fast
    3.32  
    3.33  lemma option_transp:
    3.34 -  "transp R \<Longrightarrow> transp (option_rel R)"
    3.35 -  unfolding transp_def split_option_all option_rel_simps by fast
    3.36 +  "transp R \<Longrightarrow> transp (rel_option R)"
    3.37 +  unfolding transp_def split_option_all
    3.38 +  by (simp only: option.rel_inject option.rel_distinct) fast
    3.39  
    3.40  lemma option_equivp [quot_equiv]:
    3.41 -  "equivp R \<Longrightarrow> equivp (option_rel R)"
    3.42 -  by (blast intro: equivpI reflp_option_rel option_symp option_transp elim: equivpE)
    3.43 +  "equivp R \<Longrightarrow> equivp (rel_option R)"
    3.44 +  by (blast intro: equivpI reflp_rel_option option_symp option_transp elim: equivpE)
    3.45  
    3.46  lemma option_quotient [quot_thm]:
    3.47    assumes "Quotient3 R Abs Rep"
    3.48 -  shows "Quotient3 (option_rel R) (map_option Abs) (map_option Rep)"
    3.49 +  shows "Quotient3 (rel_option R) (map_option Abs) (map_option Rep)"
    3.50    apply (rule Quotient3I)
    3.51 -  apply (simp_all add: option.map_comp comp_def option.map_id[unfolded id_def] option_rel_eq option_rel_map1 option_rel_map2 Quotient3_abs_rep [OF assms] Quotient3_rel_rep [OF assms])
    3.52 +  apply (simp_all add: option.map_comp comp_def option.map_id[unfolded id_def] rel_option_eq rel_option_map1 rel_option_map2 Quotient3_abs_rep [OF assms] Quotient3_rel_rep [OF assms])
    3.53    using Quotient3_rel [OF assms]
    3.54 -  apply (simp add: option_rel_def split: option.split)
    3.55 +  apply (simp add: rel_option_iff split: option.split)
    3.56    done
    3.57  
    3.58 -declare [[mapQ3 option = (option_rel, option_quotient)]]
    3.59 +declare [[mapQ3 option = (rel_option, option_quotient)]]
    3.60  
    3.61  lemma option_None_rsp [quot_respect]:
    3.62    assumes q: "Quotient3 R Abs Rep"
    3.63 -  shows "option_rel R None None"
    3.64 +  shows "rel_option R None None"
    3.65    by (rule None_transfer)
    3.66  
    3.67  lemma option_Some_rsp [quot_respect]:
    3.68    assumes q: "Quotient3 R Abs Rep"
    3.69 -  shows "(R ===> option_rel R) Some Some"
    3.70 +  shows "(R ===> rel_option R) Some Some"
    3.71    by (rule Some_transfer)
    3.72  
    3.73  lemma option_None_prs [quot_preserve]:
    3.74    assumes q: "Quotient3 R Abs Rep"
    3.75    shows "map_option Abs None = None"
    3.76 -  by simp
    3.77 +  by (rule Option.option.map(1))
    3.78  
    3.79  lemma option_Some_prs [quot_preserve]:
    3.80    assumes q: "Quotient3 R Abs Rep"
     4.1 --- a/src/HOL/Lifting_Option.thy	Sun Feb 16 21:33:28 2014 +0100
     4.2 +++ b/src/HOL/Lifting_Option.thy	Sun Feb 16 21:33:28 2014 +0100
     4.3 @@ -11,81 +11,73 @@
     4.4  
     4.5  subsection {* Relator and predicator properties *}
     4.6  
     4.7 -definition
     4.8 -  option_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> 'b option \<Rightarrow> bool"
     4.9 -where
    4.10 -  "option_rel R x y = (case (x, y) of (None, None) \<Rightarrow> True
    4.11 +lemma rel_option_iff:
    4.12 +  "rel_option R x y = (case (x, y) of (None, None) \<Rightarrow> True
    4.13      | (Some x, Some y) \<Rightarrow> R x y
    4.14      | _ \<Rightarrow> False)"
    4.15 -
    4.16 -lemma option_rel_simps[simp]:
    4.17 -  "option_rel R None None = True"
    4.18 -  "option_rel R (Some x) None = False"
    4.19 -  "option_rel R None (Some y) = False"
    4.20 -  "option_rel R (Some x) (Some y) = R x y"
    4.21 -  unfolding option_rel_def by simp_all
    4.22 +by (auto split: prod.split option.split)
    4.23  
    4.24  abbreviation (input) option_pred :: "('a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> bool" where
    4.25    "option_pred \<equiv> case_option True"
    4.26  
    4.27 -lemma option_rel_eq [relator_eq]:
    4.28 -  "option_rel (op =) = (op =)"
    4.29 -  by (simp add: option_rel_def fun_eq_iff split: option.split)
    4.30 +lemma rel_option_eq [relator_eq]:
    4.31 +  "rel_option (op =) = (op =)"
    4.32 +  by (simp add: rel_option_iff fun_eq_iff split: option.split)
    4.33  
    4.34 -lemma option_rel_mono[relator_mono]:
    4.35 +lemma rel_option_mono[relator_mono]:
    4.36    assumes "A \<le> B"
    4.37 -  shows "(option_rel A) \<le> (option_rel B)"
    4.38 -using assms by (auto simp: option_rel_def split: option.splits)
    4.39 +  shows "(rel_option A) \<le> (rel_option B)"
    4.40 +using assms by (auto simp: rel_option_iff split: option.splits)
    4.41  
    4.42 -lemma option_rel_OO[relator_distr]:
    4.43 -  "(option_rel A) OO (option_rel B) = option_rel (A OO B)"
    4.44 -by (rule ext)+ (auto simp: option_rel_def OO_def split: option.split)
    4.45 +lemma rel_option_OO[relator_distr]:
    4.46 +  "(rel_option A) OO (rel_option B) = rel_option (A OO B)"
    4.47 +by (rule ext)+ (auto simp: rel_option_iff OO_def split: option.split)
    4.48  
    4.49  lemma Domainp_option[relator_domain]:
    4.50    assumes "Domainp A = P"
    4.51 -  shows "Domainp (option_rel A) = (option_pred P)"
    4.52 -using assms unfolding Domainp_iff[abs_def] option_rel_def[abs_def]
    4.53 +  shows "Domainp (rel_option A) = (option_pred P)"
    4.54 +using assms unfolding Domainp_iff[abs_def] rel_option_iff[abs_def]
    4.55  by (auto iff: fun_eq_iff split: option.split)
    4.56  
    4.57 -lemma reflp_option_rel[reflexivity_rule]:
    4.58 -  "reflp R \<Longrightarrow> reflp (option_rel R)"
    4.59 +lemma reflp_rel_option[reflexivity_rule]:
    4.60 +  "reflp R \<Longrightarrow> reflp (rel_option R)"
    4.61    unfolding reflp_def split_option_all by simp
    4.62  
    4.63 -lemma left_total_option_rel[reflexivity_rule]:
    4.64 -  "left_total R \<Longrightarrow> left_total (option_rel R)"
    4.65 +lemma left_total_rel_option[reflexivity_rule]:
    4.66 +  "left_total R \<Longrightarrow> left_total (rel_option R)"
    4.67    unfolding left_total_def split_option_all split_option_ex by simp
    4.68  
    4.69 -lemma left_unique_option_rel [reflexivity_rule]:
    4.70 -  "left_unique R \<Longrightarrow> left_unique (option_rel R)"
    4.71 +lemma left_unique_rel_option [reflexivity_rule]:
    4.72 +  "left_unique R \<Longrightarrow> left_unique (rel_option R)"
    4.73    unfolding left_unique_def split_option_all by simp
    4.74  
    4.75 -lemma right_total_option_rel [transfer_rule]:
    4.76 -  "right_total R \<Longrightarrow> right_total (option_rel R)"
    4.77 +lemma right_total_rel_option [transfer_rule]:
    4.78 +  "right_total R \<Longrightarrow> right_total (rel_option R)"
    4.79    unfolding right_total_def split_option_all split_option_ex by simp
    4.80  
    4.81 -lemma right_unique_option_rel [transfer_rule]:
    4.82 -  "right_unique R \<Longrightarrow> right_unique (option_rel R)"
    4.83 +lemma right_unique_rel_option [transfer_rule]:
    4.84 +  "right_unique R \<Longrightarrow> right_unique (rel_option R)"
    4.85    unfolding right_unique_def split_option_all by simp
    4.86  
    4.87 -lemma bi_total_option_rel [transfer_rule]:
    4.88 -  "bi_total R \<Longrightarrow> bi_total (option_rel R)"
    4.89 +lemma bi_total_rel_option [transfer_rule]:
    4.90 +  "bi_total R \<Longrightarrow> bi_total (rel_option R)"
    4.91    unfolding bi_total_def split_option_all split_option_ex by simp
    4.92  
    4.93 -lemma bi_unique_option_rel [transfer_rule]:
    4.94 -  "bi_unique R \<Longrightarrow> bi_unique (option_rel R)"
    4.95 +lemma bi_unique_rel_option [transfer_rule]:
    4.96 +  "bi_unique R \<Longrightarrow> bi_unique (rel_option R)"
    4.97    unfolding bi_unique_def split_option_all by simp
    4.98  
    4.99  lemma option_invariant_commute [invariant_commute]:
   4.100 -  "option_rel (Lifting.invariant P) = Lifting.invariant (option_pred P)"
   4.101 +  "rel_option (Lifting.invariant P) = Lifting.invariant (option_pred P)"
   4.102    by (auto simp add: fun_eq_iff Lifting.invariant_def split_option_all)
   4.103  
   4.104  subsection {* Quotient theorem for the Lifting package *}
   4.105  
   4.106  lemma Quotient_option[quot_map]:
   4.107    assumes "Quotient R Abs Rep T"
   4.108 -  shows "Quotient (option_rel R) (map_option Abs)
   4.109 -    (map_option Rep) (option_rel T)"
   4.110 -  using assms unfolding Quotient_alt_def option_rel_def
   4.111 +  shows "Quotient (rel_option R) (map_option Abs)
   4.112 +    (map_option Rep) (rel_option T)"
   4.113 +  using assms unfolding Quotient_alt_def rel_option_iff
   4.114    by (simp split: option.split)
   4.115  
   4.116  subsection {* Transfer rules for the Transfer package *}
   4.117 @@ -94,22 +86,22 @@
   4.118  begin
   4.119  interpretation lifting_syntax .
   4.120  
   4.121 -lemma None_transfer [transfer_rule]: "(option_rel A) None None"
   4.122 -  by simp
   4.123 +lemma None_transfer [transfer_rule]: "(rel_option A) None None"
   4.124 +  by (rule option.rel_inject)
   4.125  
   4.126 -lemma Some_transfer [transfer_rule]: "(A ===> option_rel A) Some Some"
   4.127 +lemma Some_transfer [transfer_rule]: "(A ===> rel_option A) Some Some"
   4.128    unfolding fun_rel_def by simp
   4.129  
   4.130  lemma case_option_transfer [transfer_rule]:
   4.131 -  "(B ===> (A ===> B) ===> option_rel A ===> B) case_option case_option"
   4.132 +  "(B ===> (A ===> B) ===> rel_option A ===> B) case_option case_option"
   4.133    unfolding fun_rel_def split_option_all by simp
   4.134  
   4.135  lemma map_option_transfer [transfer_rule]:
   4.136 -  "((A ===> B) ===> option_rel A ===> option_rel B) map_option map_option"
   4.137 +  "((A ===> B) ===> rel_option A ===> rel_option B) map_option map_option"
   4.138    unfolding map_option_case[abs_def] by transfer_prover
   4.139  
   4.140  lemma option_bind_transfer [transfer_rule]:
   4.141 -  "(option_rel A ===> (A ===> option_rel B) ===> option_rel B)
   4.142 +  "(rel_option A ===> (A ===> rel_option B) ===> rel_option B)
   4.143      Option.bind Option.bind"
   4.144    unfolding fun_rel_def split_option_all by simp
   4.145  
     5.1 --- a/src/HOL/List.thy	Sun Feb 16 21:33:28 2014 +0100
     5.2 +++ b/src/HOL/List.thy	Sun Feb 16 21:33:28 2014 +0100
     5.3 @@ -6779,7 +6779,7 @@
     5.4    unfolding List.insert_def [abs_def] by transfer_prover
     5.5  
     5.6  lemma find_transfer [transfer_rule]:
     5.7 -  "((A ===> op =) ===> list_all2 A ===> option_rel A) List.find List.find"
     5.8 +  "((A ===> op =) ===> list_all2 A ===> rel_option A) List.find List.find"
     5.9    unfolding List.find_def by transfer_prover
    5.10  
    5.11  lemma remove1_transfer [transfer_rule]: