--- 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")
--- 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) (\<lambda>m k. m k) (\<lambda>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)
(\<lambda>k v m. m(k \<mapsto> v)) (\<lambda>k v m. m(k \<mapsto> 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)
(\<lambda>k m. m(k := None)) (\<lambda>k m. m(k := None))"
by transfer_prover
definition equal_None :: "'a option \<Rightarrow> bool" where "equal_None x \<equiv> 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)
(\<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)))"
by transfer_prover
lemma bulkload_transfer:
- "(list_all2 A ===> op= ===> option_rel A)
+ "(list_all2 A ===> op= ===> rel_option A)
(\<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)"
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)
(\<lambda>f g m. (map_option g \<circ> m \<circ> f)) (\<lambda>f g m. (map_option g \<circ> m \<circ> 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)
(\<lambda>k f m. (case m k of None \<Rightarrow> m
| Some v \<Rightarrow> m (k \<mapsto> (f v)))) (\<lambda>k f m. (case m k of None \<Rightarrow> m
| Some v \<Rightarrow> m (k \<mapsto> (f v))))"
--- 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 \<longleftrightarrow> option_rel (\<lambda>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 \<longleftrightarrow> rel_option (\<lambda>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) \<longleftrightarrow> option_rel (\<lambda>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) \<longleftrightarrow> rel_option (\<lambda>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 \<Longrightarrow> symp (option_rel R)"
- unfolding symp_def split_option_all option_rel_simps by fast
+ "symp R \<Longrightarrow> 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 \<Longrightarrow> transp (option_rel R)"
- unfolding transp_def split_option_all option_rel_simps by fast
+ "transp R \<Longrightarrow> 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 \<Longrightarrow> equivp (option_rel R)"
- by (blast intro: equivpI reflp_option_rel option_symp option_transp elim: equivpE)
+ "equivp R \<Longrightarrow> 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"
--- 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 \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> 'b option \<Rightarrow> bool"
-where
- "option_rel R x y = (case (x, y) of (None, None) \<Rightarrow> True
+lemma rel_option_iff:
+ "rel_option R x y = (case (x, y) of (None, None) \<Rightarrow> True
| (Some x, Some y) \<Rightarrow> R x y
| _ \<Rightarrow> 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 \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> bool" where
"option_pred \<equiv> 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 \<le> B"
- shows "(option_rel A) \<le> (option_rel B)"
-using assms by (auto simp: option_rel_def split: option.splits)
+ shows "(rel_option A) \<le> (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 \<Longrightarrow> reflp (option_rel R)"
+lemma reflp_rel_option[reflexivity_rule]:
+ "reflp R \<Longrightarrow> reflp (rel_option R)"
unfolding reflp_def split_option_all by simp
-lemma left_total_option_rel[reflexivity_rule]:
- "left_total R \<Longrightarrow> left_total (option_rel R)"
+lemma left_total_rel_option[reflexivity_rule]:
+ "left_total R \<Longrightarrow> 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 \<Longrightarrow> left_unique (option_rel R)"
+lemma left_unique_rel_option [reflexivity_rule]:
+ "left_unique R \<Longrightarrow> left_unique (rel_option R)"
unfolding left_unique_def split_option_all by simp
-lemma right_total_option_rel [transfer_rule]:
- "right_total R \<Longrightarrow> right_total (option_rel R)"
+lemma right_total_rel_option [transfer_rule]:
+ "right_total R \<Longrightarrow> 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 \<Longrightarrow> right_unique (option_rel R)"
+lemma right_unique_rel_option [transfer_rule]:
+ "right_unique R \<Longrightarrow> right_unique (rel_option R)"
unfolding right_unique_def split_option_all by simp
-lemma bi_total_option_rel [transfer_rule]:
- "bi_total R \<Longrightarrow> bi_total (option_rel R)"
+lemma bi_total_rel_option [transfer_rule]:
+ "bi_total R \<Longrightarrow> 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 \<Longrightarrow> bi_unique (option_rel R)"
+lemma bi_unique_rel_option [transfer_rule]:
+ "bi_unique R \<Longrightarrow> 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
--- 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]: