# HG changeset patch # User blanchet # Date 1392582808 -3600 # Node ID 70b7e91fa1f99e7fd1324843f1e8f2b71573c1a0 # Parent f41ef840f09d50ca320ecd300ab093b60b9611db folded 'rel_option' into 'option_rel' diff -r f41ef840f09d -r 70b7e91fa1f9 NEWS --- a/NEWS Sun Feb 16 21:33:28 2014 +0100 +++ b/NEWS Sun Feb 16 21:33:28 2014 +0100 @@ -135,6 +135,7 @@ Renamed constants: Option.set ~> set_option Option.map ~> map_option + option_rel ~> rel_option Renamed theorems: map_def ~> map_rec[abs_def] Option.map_def ~> map_option_case[abs_def] (with "case_option" instead of "rec_option") diff -r f41ef840f09d -r 70b7e91fa1f9 src/HOL/Library/Mapping.thy --- a/src/HOL/Library/Mapping.thy Sun Feb 16 21:33:28 2014 +0100 +++ b/src/HOL/Library/Mapping.thy Sun Feb 16 21:33:28 2014 +0100 @@ -14,46 +14,46 @@ begin interpretation lifting_syntax . -lemma empty_transfer: "(A ===> option_rel B) Map.empty Map.empty" by transfer_prover +lemma empty_transfer: "(A ===> rel_option B) Map.empty Map.empty" by transfer_prover lemma lookup_transfer: "((A ===> B) ===> A ===> B) (\m k. m k) (\m k. m k)" by transfer_prover lemma update_transfer: assumes [transfer_rule]: "bi_unique A" - shows "(A ===> B ===> (A ===> option_rel B) ===> A ===> option_rel B) + shows "(A ===> B ===> (A ===> rel_option B) ===> A ===> rel_option B) (\k v m. m(k \ v)) (\k v m. m(k \ v))" by transfer_prover lemma delete_transfer: assumes [transfer_rule]: "bi_unique A" - shows "(A ===> (A ===> option_rel B) ===> A ===> option_rel B) + shows "(A ===> (A ===> rel_option B) ===> A ===> rel_option B) (\k m. m(k := None)) (\k m. m(k := None))" by transfer_prover definition equal_None :: "'a option \ bool" where "equal_None x \ x = None" -lemma [transfer_rule]: "(option_rel A ===> op=) equal_None equal_None" -unfolding fun_rel_def option_rel_def equal_None_def by (auto split: option.split) +lemma [transfer_rule]: "(rel_option A ===> op=) equal_None equal_None" +unfolding fun_rel_def rel_option_iff equal_None_def by (auto split: option.split) lemma dom_transfer: assumes [transfer_rule]: "bi_total A" - shows "((A ===> option_rel B) ===> set_rel A) dom dom" + shows "((A ===> rel_option B) ===> set_rel A) dom dom" unfolding dom_def[abs_def] equal_None_def[symmetric] by transfer_prover lemma map_of_transfer [transfer_rule]: assumes [transfer_rule]: "bi_unique R1" - shows "(list_all2 (prod_rel R1 R2) ===> R1 ===> option_rel R2) map_of map_of" + shows "(list_all2 (prod_rel R1 R2) ===> R1 ===> rel_option R2) map_of map_of" unfolding map_of_def by transfer_prover lemma tabulate_transfer: assumes [transfer_rule]: "bi_unique A" - shows "(list_all2 A ===> (A ===> B) ===> A ===> option_rel B) + shows "(list_all2 A ===> (A ===> B) ===> A ===> rel_option B) (\ks f. (map_of (List.map (\k. (k, f k)) ks))) (\ks f. (map_of (List.map (\k. (k, f k)) ks)))" by transfer_prover lemma bulkload_transfer: - "(list_all2 A ===> op= ===> option_rel A) + "(list_all2 A ===> op= ===> rel_option A) (\xs k. if k < length xs then Some (xs ! k) else None) (\xs k. if k < length xs then Some (xs ! k) else None)" unfolding fun_rel_def apply clarsimp @@ -64,13 +64,13 @@ by (auto dest: list_all2_lengthD list_all2_nthD) lemma map_transfer: - "((A ===> B) ===> (C ===> D) ===> (B ===> option_rel C) ===> A ===> option_rel D) + "((A ===> B) ===> (C ===> D) ===> (B ===> rel_option C) ===> A ===> rel_option D) (\f g m. (map_option g \ m \ f)) (\f g m. (map_option g \ m \ f))" by transfer_prover lemma map_entry_transfer: assumes [transfer_rule]: "bi_unique A" - shows "(A ===> (B ===> B) ===> (A ===> option_rel B) ===> A ===> option_rel B) + shows "(A ===> (B ===> B) ===> (A ===> rel_option B) ===> A ===> rel_option B) (\k f m. (case m k of None \ m | Some v \ m (k \ (f v)))) (\k f m. (case m k of None \ m | Some v \ m (k \ (f v))))" diff -r f41ef840f09d -r 70b7e91fa1f9 src/HOL/Library/Quotient_Option.thy --- a/src/HOL/Library/Quotient_Option.thy Sun Feb 16 21:33:28 2014 +0100 +++ b/src/HOL/Library/Quotient_Option.thy Sun Feb 16 21:33:28 2014 +0100 @@ -10,55 +10,57 @@ subsection {* Rules for the Quotient package *} -lemma option_rel_map1: - "option_rel R (map_option f x) y \ option_rel (\x. R (f x)) x y" - by (simp add: option_rel_def split: option.split) +lemma rel_option_map1: + "rel_option R (map_option f x) y \ rel_option (\x. R (f x)) x y" + by (simp add: rel_option_iff split: option.split) -lemma option_rel_map2: - "option_rel R x (map_option f y) \ option_rel (\x y. R x (f y)) x y" - by (simp add: option_rel_def split: option.split) +lemma rel_option_map2: + "rel_option R x (map_option f y) \ rel_option (\x y. R x (f y)) x y" + by (simp add: rel_option_iff split: option.split) declare map_option.id [id_simps] - option_rel_eq [id_simps] + rel_option_eq [id_simps] lemma option_symp: - "symp R \ symp (option_rel R)" - unfolding symp_def split_option_all option_rel_simps by fast + "symp R \ symp (rel_option R)" + unfolding symp_def split_option_all + by (simp only: option.rel_inject option.rel_distinct) fast lemma option_transp: - "transp R \ transp (option_rel R)" - unfolding transp_def split_option_all option_rel_simps by fast + "transp R \ transp (rel_option R)" + unfolding transp_def split_option_all + by (simp only: option.rel_inject option.rel_distinct) fast lemma option_equivp [quot_equiv]: - "equivp R \ equivp (option_rel R)" - by (blast intro: equivpI reflp_option_rel option_symp option_transp elim: equivpE) + "equivp R \ equivp (rel_option R)" + by (blast intro: equivpI reflp_rel_option option_symp option_transp elim: equivpE) lemma option_quotient [quot_thm]: assumes "Quotient3 R Abs Rep" - shows "Quotient3 (option_rel R) (map_option Abs) (map_option Rep)" + shows "Quotient3 (rel_option R) (map_option Abs) (map_option Rep)" apply (rule Quotient3I) - 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]) + 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]) using Quotient3_rel [OF assms] - apply (simp add: option_rel_def split: option.split) + apply (simp add: rel_option_iff split: option.split) done -declare [[mapQ3 option = (option_rel, option_quotient)]] +declare [[mapQ3 option = (rel_option, option_quotient)]] lemma option_None_rsp [quot_respect]: assumes q: "Quotient3 R Abs Rep" - shows "option_rel R None None" + shows "rel_option R None None" by (rule None_transfer) lemma option_Some_rsp [quot_respect]: assumes q: "Quotient3 R Abs Rep" - shows "(R ===> option_rel R) Some Some" + shows "(R ===> rel_option R) Some Some" by (rule Some_transfer) lemma option_None_prs [quot_preserve]: assumes q: "Quotient3 R Abs Rep" shows "map_option Abs None = None" - by simp + by (rule Option.option.map(1)) lemma option_Some_prs [quot_preserve]: assumes q: "Quotient3 R Abs Rep" diff -r f41ef840f09d -r 70b7e91fa1f9 src/HOL/Lifting_Option.thy --- a/src/HOL/Lifting_Option.thy Sun Feb 16 21:33:28 2014 +0100 +++ b/src/HOL/Lifting_Option.thy Sun Feb 16 21:33:28 2014 +0100 @@ -11,81 +11,73 @@ subsection {* Relator and predicator properties *} -definition - option_rel :: "('a \ 'b \ bool) \ 'a option \ 'b option \ bool" -where - "option_rel R x y = (case (x, y) of (None, None) \ True +lemma rel_option_iff: + "rel_option R x y = (case (x, y) of (None, None) \ True | (Some x, Some y) \ R x y | _ \ False)" - -lemma option_rel_simps[simp]: - "option_rel R None None = True" - "option_rel R (Some x) None = False" - "option_rel R None (Some y) = False" - "option_rel R (Some x) (Some y) = R x y" - unfolding option_rel_def by simp_all +by (auto split: prod.split option.split) abbreviation (input) option_pred :: "('a \ bool) \ 'a option \ bool" where "option_pred \ case_option True" -lemma option_rel_eq [relator_eq]: - "option_rel (op =) = (op =)" - by (simp add: option_rel_def fun_eq_iff split: option.split) +lemma rel_option_eq [relator_eq]: + "rel_option (op =) = (op =)" + by (simp add: rel_option_iff fun_eq_iff split: option.split) -lemma option_rel_mono[relator_mono]: +lemma rel_option_mono[relator_mono]: assumes "A \ B" - shows "(option_rel A) \ (option_rel B)" -using assms by (auto simp: option_rel_def split: option.splits) + shows "(rel_option A) \ (rel_option B)" +using assms by (auto simp: rel_option_iff split: option.splits) -lemma option_rel_OO[relator_distr]: - "(option_rel A) OO (option_rel B) = option_rel (A OO B)" -by (rule ext)+ (auto simp: option_rel_def OO_def split: option.split) +lemma rel_option_OO[relator_distr]: + "(rel_option A) OO (rel_option B) = rel_option (A OO B)" +by (rule ext)+ (auto simp: rel_option_iff OO_def split: option.split) lemma Domainp_option[relator_domain]: assumes "Domainp A = P" - shows "Domainp (option_rel A) = (option_pred P)" -using assms unfolding Domainp_iff[abs_def] option_rel_def[abs_def] + shows "Domainp (rel_option A) = (option_pred P)" +using assms unfolding Domainp_iff[abs_def] rel_option_iff[abs_def] by (auto iff: fun_eq_iff split: option.split) -lemma reflp_option_rel[reflexivity_rule]: - "reflp R \ reflp (option_rel R)" +lemma reflp_rel_option[reflexivity_rule]: + "reflp R \ reflp (rel_option R)" unfolding reflp_def split_option_all by simp -lemma left_total_option_rel[reflexivity_rule]: - "left_total R \ left_total (option_rel R)" +lemma left_total_rel_option[reflexivity_rule]: + "left_total R \ left_total (rel_option R)" unfolding left_total_def split_option_all split_option_ex by simp -lemma left_unique_option_rel [reflexivity_rule]: - "left_unique R \ left_unique (option_rel R)" +lemma left_unique_rel_option [reflexivity_rule]: + "left_unique R \ left_unique (rel_option R)" unfolding left_unique_def split_option_all by simp -lemma right_total_option_rel [transfer_rule]: - "right_total R \ right_total (option_rel R)" +lemma right_total_rel_option [transfer_rule]: + "right_total R \ right_total (rel_option R)" unfolding right_total_def split_option_all split_option_ex by simp -lemma right_unique_option_rel [transfer_rule]: - "right_unique R \ right_unique (option_rel R)" +lemma right_unique_rel_option [transfer_rule]: + "right_unique R \ right_unique (rel_option R)" unfolding right_unique_def split_option_all by simp -lemma bi_total_option_rel [transfer_rule]: - "bi_total R \ bi_total (option_rel R)" +lemma bi_total_rel_option [transfer_rule]: + "bi_total R \ bi_total (rel_option R)" unfolding bi_total_def split_option_all split_option_ex by simp -lemma bi_unique_option_rel [transfer_rule]: - "bi_unique R \ bi_unique (option_rel R)" +lemma bi_unique_rel_option [transfer_rule]: + "bi_unique R \ bi_unique (rel_option R)" unfolding bi_unique_def split_option_all by simp lemma option_invariant_commute [invariant_commute]: - "option_rel (Lifting.invariant P) = Lifting.invariant (option_pred P)" + "rel_option (Lifting.invariant P) = Lifting.invariant (option_pred P)" by (auto simp add: fun_eq_iff Lifting.invariant_def split_option_all) subsection {* Quotient theorem for the Lifting package *} lemma Quotient_option[quot_map]: assumes "Quotient R Abs Rep T" - shows "Quotient (option_rel R) (map_option Abs) - (map_option Rep) (option_rel T)" - using assms unfolding Quotient_alt_def option_rel_def + shows "Quotient (rel_option R) (map_option Abs) + (map_option Rep) (rel_option T)" + using assms unfolding Quotient_alt_def rel_option_iff by (simp split: option.split) subsection {* Transfer rules for the Transfer package *} @@ -94,22 +86,22 @@ begin interpretation lifting_syntax . -lemma None_transfer [transfer_rule]: "(option_rel A) None None" - by simp +lemma None_transfer [transfer_rule]: "(rel_option A) None None" + by (rule option.rel_inject) -lemma Some_transfer [transfer_rule]: "(A ===> option_rel A) Some Some" +lemma Some_transfer [transfer_rule]: "(A ===> rel_option A) Some Some" unfolding fun_rel_def by simp lemma case_option_transfer [transfer_rule]: - "(B ===> (A ===> B) ===> option_rel A ===> B) case_option case_option" + "(B ===> (A ===> B) ===> rel_option A ===> B) case_option case_option" unfolding fun_rel_def split_option_all by simp lemma map_option_transfer [transfer_rule]: - "((A ===> B) ===> option_rel A ===> option_rel B) map_option map_option" + "((A ===> B) ===> rel_option A ===> rel_option B) map_option map_option" unfolding map_option_case[abs_def] by transfer_prover lemma option_bind_transfer [transfer_rule]: - "(option_rel A ===> (A ===> option_rel B) ===> option_rel B) + "(rel_option A ===> (A ===> rel_option B) ===> rel_option B) Option.bind Option.bind" unfolding fun_rel_def split_option_all by simp diff -r f41ef840f09d -r 70b7e91fa1f9 src/HOL/List.thy --- a/src/HOL/List.thy Sun Feb 16 21:33:28 2014 +0100 +++ b/src/HOL/List.thy Sun Feb 16 21:33:28 2014 +0100 @@ -6779,7 +6779,7 @@ unfolding List.insert_def [abs_def] by transfer_prover lemma find_transfer [transfer_rule]: - "((A ===> op =) ===> list_all2 A ===> option_rel A) List.find List.find" + "((A ===> op =) ===> list_all2 A ===> rel_option A) List.find List.find" unfolding List.find_def by transfer_prover lemma remove1_transfer [transfer_rule]: