--- a/src/HOL/BNF_Def.thy Wed Feb 11 14:53:56 2015 +0100
+++ b/src/HOL/BNF_Def.thy Wed Feb 11 15:04:23 2015 +0100
@@ -41,6 +41,14 @@
shows "B (f x) (g y)"
using assms by (simp add: rel_fun_def)
+lemma rel_fun_mono:
+ "\<lbrakk> rel_fun X A f g; \<And>x y. Y x y \<longrightarrow> X x y; \<And>x y. A x y \<Longrightarrow> B x y \<rbrakk> \<Longrightarrow> rel_fun Y B f g"
+by(simp add: rel_fun_def)
+
+lemma rel_fun_mono' [mono]:
+ "\<lbrakk> \<And>x y. Y x y \<longrightarrow> X x y; \<And>x y. A x y \<longrightarrow> B x y \<rbrakk> \<Longrightarrow> rel_fun X A f g \<longrightarrow> rel_fun Y B f g"
+by(simp add: rel_fun_def)
+
definition rel_set :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> bool"
where "rel_set R = (\<lambda>A B. (\<forall>x\<in>A. \<exists>y\<in>B. R x y) \<and> (\<forall>y\<in>B. \<exists>x\<in>A. R x y))"
--- a/src/HOL/Finite_Set.thy Wed Feb 11 14:53:56 2015 +0100
+++ b/src/HOL/Finite_Set.thy Wed Feb 11 15:04:23 2015 +0100
@@ -315,14 +315,11 @@
"finite F \<Longrightarrow> inj h \<Longrightarrow> finite (h -` F)"
using finite_vimage_IntI[of F h UNIV] by auto
-lemma finite_vimageD:
- assumes fin: "finite (h -` F)" and surj: "surj h"
- shows "finite F"
-proof -
- have "finite (h ` (h -` F))" using fin by (rule finite_imageI)
- also have "h ` (h -` F) = F" using surj by (rule surj_image_vimage_eq)
- finally show "finite F" .
-qed
+lemma finite_vimageD': "\<lbrakk> finite (f -` A); A \<subseteq> range f \<rbrakk> \<Longrightarrow> finite A"
+by(auto simp add: subset_image_iff intro: finite_subset[rotated])
+
+lemma finite_vimageD: "\<lbrakk> finite (h -` F); surj h \<rbrakk> \<Longrightarrow> finite F"
+by(auto dest: finite_vimageD')
lemma finite_vimage_iff: "bij h \<Longrightarrow> finite (h -` F) \<longleftrightarrow> finite F"
unfolding bij_def by (auto elim: finite_vimageD finite_vimageI)
@@ -1641,6 +1638,8 @@
shows "finite A"
using assms finite_imageD finite_subset by blast
+lemma card_vimage_inj: "\<lbrakk> inj f; A \<subseteq> range f \<rbrakk> \<Longrightarrow> card (f -` A) = card A"
+by(auto 4 3 simp add: subset_image_iff inj_vimage_image_eq intro: card_image[symmetric, OF subset_inj_on])
subsubsection {* Pigeonhole Principles *}
--- a/src/HOL/Fun.thy Wed Feb 11 14:53:56 2015 +0100
+++ b/src/HOL/Fun.thy Wed Feb 11 15:04:23 2015 +0100
@@ -88,6 +88,12 @@
lemma image_eq_imp_comp: "f ` A = g ` B \<Longrightarrow> (h o f) ` A = (h o g) ` B"
by (auto simp: comp_def elim!: equalityE)
+lemma image_bind: "f ` (Set.bind A g) = Set.bind A (op ` f \<circ> g)"
+by(auto simp add: Set.bind_def)
+
+lemma bind_image: "Set.bind (f ` A) g = Set.bind A (g \<circ> f)"
+by(auto simp add: Set.bind_def)
+
code_printing
constant comp \<rightharpoonup> (SML) infixl 5 "o" and (Haskell) infixr 9 "."
--- a/src/HOL/List.thy Wed Feb 11 14:53:56 2015 +0100
+++ b/src/HOL/List.thy Wed Feb 11 15:04:23 2015 +0100
@@ -6795,6 +6795,21 @@
shows "(rel_set (rel_prod A A) ===> rel_set (rel_prod A A)) rtrancl rtrancl"
unfolding rtrancl_def by transfer_prover
+lemma monotone_parametric [transfer_rule]:
+ assumes [transfer_rule]: "bi_total A"
+ shows "((A ===> A ===> op =) ===> (B ===> B ===> op =) ===> (A ===> B) ===> op =) monotone monotone"
+unfolding monotone_def[abs_def] by transfer_prover
+
+lemma fun_ord_parametric [transfer_rule]:
+ assumes [transfer_rule]: "bi_total C"
+ shows "((A ===> B ===> op =) ===> (C ===> A) ===> (C ===> B) ===> op =) fun_ord fun_ord"
+unfolding fun_ord_def[abs_def] by transfer_prover
+
+lemma fun_lub_parametric [transfer_rule]:
+ assumes [transfer_rule]: "bi_total A" "bi_unique A"
+ shows "((rel_set A ===> B) ===> rel_set (C ===> A) ===> C ===> B) fun_lub fun_lub"
+unfolding fun_lub_def[abs_def] by transfer_prover
+
end
end
--- a/src/HOL/Option.thy Wed Feb 11 14:53:56 2015 +0100
+++ b/src/HOL/Option.thy Wed Feb 11 15:04:23 2015 +0100
@@ -62,6 +62,22 @@
lemma UNIV_option_conv: "UNIV = insert None (range Some)"
by(auto intro: classical)
+lemma rel_option_None1 [simp]: "rel_option P None x \<longleftrightarrow> x = None"
+by(cases x) simp_all
+
+lemma rel_option_None2 [simp]: "rel_option P x None \<longleftrightarrow> x = None"
+by(cases x) simp_all
+
+lemma rel_option_inf: "inf (rel_option A) (rel_option B) = rel_option (inf A B)" (is "?lhs = ?rhs")
+proof(rule antisym)
+ show "?lhs \<le> ?rhs" by(auto elim!: option.rel_cases)
+qed(auto elim: option.rel_mono_strong)
+
+lemma rel_option_reflI:
+ "(\<And>x. x \<in> set_option y \<Longrightarrow> P x x) \<Longrightarrow> rel_option P y y"
+by(cases y) auto
+
+
subsubsection {* Operations *}
lemma ospec [dest]: "(ALL x:set_option A. P x) ==> A = Some x ==> P x"
@@ -93,22 +109,8 @@
lemma map_option_cong: "x = y \<Longrightarrow> (\<And>a. y = Some a \<Longrightarrow> f a = g a) \<Longrightarrow> map_option f x = map_option g y"
by (cases x) auto
-functor map_option: map_option proof -
- fix f g
- show "map_option f \<circ> map_option g = map_option (f \<circ> g)"
- proof
- fix x
- show "(map_option f \<circ> map_option g) x= map_option (f \<circ> g) x"
- by (cases x) simp_all
- qed
-next
- show "map_option id = id"
- proof
- fix x
- show "map_option id x = id x"
- by (cases x) simp_all
- qed
-qed
+functor map_option: map_option
+by(simp_all add: option.map_comp fun_eq_iff option.map_id)
lemma case_map_option [simp]:
"case_option g h (map_option f x) = case_option g (h \<circ> f) x"
@@ -120,10 +122,43 @@
| _ \<Rightarrow> False)"
by (auto split: prod.split option.split)
+definition is_none :: "'a option \<Rightarrow> bool"
+where [code_post]: "is_none x \<longleftrightarrow> x = None"
+
+lemma is_none_simps [simp]:
+ "is_none None"
+ "\<not> is_none (Some x)"
+by(simp_all add: is_none_def)
+
+lemma is_none_code [code]:
+ "is_none None = True"
+ "is_none (Some x) = False"
+by simp_all
+
+lemma rel_option_unfold:
+ "rel_option R x y \<longleftrightarrow>
+ (is_none x \<longleftrightarrow> is_none y) \<and> (\<not> is_none x \<longrightarrow> \<not> is_none y \<longrightarrow> R (the x) (the y))"
+by(simp add: rel_option_iff split: option.split)
+
+lemma rel_optionI:
+ "\<lbrakk> is_none x \<longleftrightarrow> is_none y; \<lbrakk> \<not> is_none x; \<not> is_none y \<rbrakk> \<Longrightarrow> P (the x) (the y) \<rbrakk>
+ \<Longrightarrow> rel_option P x y"
+by(simp add: rel_option_unfold)
+
+lemma is_none_map_option [simp]: "is_none (map_option f x) \<longleftrightarrow> is_none x"
+by(simp add: is_none_def)
+
+lemma the_map_option: "\<not> is_none x \<Longrightarrow> the (map_option f x) = f (the x)"
+by(clarsimp simp add: is_none_def)
+
+
primrec bind :: "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option" where
bind_lzero: "bind None f = None" |
bind_lunit: "bind (Some x) f = f x"
+lemma is_none_bind: "is_none (bind f g) \<longleftrightarrow> is_none f \<or> is_none (g (the f))"
+by(cases f) simp_all
+
lemma bind_runit[simp]: "bind x Some = x"
by (cases x) auto
@@ -147,6 +182,24 @@
lemmas bind_splits = bind_split bind_split_asm
+lemma bind_eq_Some_conv: "bind f g = Some x \<longleftrightarrow> (\<exists>y. f = Some y \<and> g y = Some x)"
+by(cases f) simp_all
+
+lemma map_option_bind: "map_option f (bind x g) = bind x (map_option f \<circ> g)"
+by(cases x) simp_all
+
+lemma bind_option_cong:
+ "\<lbrakk> x = y; \<And>z. z \<in> set_option y \<Longrightarrow> f z = g z \<rbrakk> \<Longrightarrow> bind x f = bind y g"
+by(cases y) simp_all
+
+lemma bind_option_cong_simp:
+ "\<lbrakk> x = y; \<And>z. z \<in> set_option y =simp=> f z = g z \<rbrakk> \<Longrightarrow> bind x f = bind y g"
+unfolding simp_implies_def by(rule bind_option_cong)
+
+lemma bind_option_cong_code: "x = y \<Longrightarrow> bind x f = bind y f" by simp
+setup \<open>Code_Simp.map_ss (Simplifier.add_cong @{thm bind_option_cong_code})\<close>
+
+
definition these :: "'a option set \<Rightarrow> 'a set"
where
"these A = the ` {x \<in> A. x \<noteq> None}"
@@ -209,6 +262,10 @@
Option.bind Option.bind"
unfolding rel_fun_def split_option_all by simp
+lemma pred_option_parametric [transfer_rule]:
+ "((A ===> op =) ===> rel_option A ===> op =) pred_option pred_option"
+by(rule rel_funI)+(auto simp add: rel_option_unfold is_none_def dest: rel_funD)
+
end
@@ -224,15 +281,7 @@
subsubsection {* Code generator setup *}
-definition is_none :: "'a option \<Rightarrow> bool" where
- [code_post]: "is_none x \<longleftrightarrow> x = None"
-
-lemma is_none_code [code]:
- shows "is_none None \<longleftrightarrow> True"
- and "is_none (Some x) \<longleftrightarrow> False"
- unfolding is_none_def by simp_all
-
-lemma [code_unfold]:
+lemma equal_None_code_unfold [code_unfold]:
"HOL.equal x None \<longleftrightarrow> is_none x"
"HOL.equal None = is_none"
by (auto simp add: equal is_none_def)
--- a/src/HOL/Partial_Function.thy Wed Feb 11 14:53:56 2015 +0100
+++ b/src/HOL/Partial_Function.thy Wed Feb 11 15:04:23 2015 +0100
@@ -236,6 +236,15 @@
qed
qed (auto simp: flat_ord_def)
+lemma flat_ordI: "(x \<noteq> a \<Longrightarrow> x = y) \<Longrightarrow> flat_ord a x y"
+by(auto simp add: flat_ord_def)
+
+lemma flat_ord_antisym: "\<lbrakk> flat_ord a x y; flat_ord a y x \<rbrakk> \<Longrightarrow> x = y"
+by(auto simp add: flat_ord_def)
+
+lemma antisymP_flat_ord: "antisymP (flat_ord a)"
+by(rule antisymI)(auto dest: flat_ord_antisym)
+
interpretation tailrec!:
partial_function_definitions "flat_ord undefined" "flat_lub undefined"
where "flat_lub undefined {} \<equiv> undefined"
--- a/src/HOL/Relation.thy Wed Feb 11 14:53:56 2015 +0100
+++ b/src/HOL/Relation.thy Wed Feb 11 15:04:23 2015 +0100
@@ -426,6 +426,8 @@
"transp r \<longleftrightarrow> trans {(x, y). r x y}"
by (simp add: trans_def transp_def)
+lemma transp_equality [simp]: "transp op ="
+by(auto intro: transpI)
subsubsection {* Totality *}
--- a/src/HOL/Transfer.thy Wed Feb 11 14:53:56 2015 +0100
+++ b/src/HOL/Transfer.thy Wed Feb 11 15:04:23 2015 +0100
@@ -154,6 +154,14 @@
lemma right_uniqueD: "\<lbrakk> right_unique A; A x y; A x z \<rbrakk> \<Longrightarrow> y = z"
unfolding right_unique_def by fast
+lemma right_totalI: "(\<And>y. \<exists>x. A x y) \<Longrightarrow> right_total A"
+by(simp add: right_total_def)
+
+lemma right_totalE:
+ assumes "right_total A"
+ obtains x where "A x y"
+using assms by(auto simp add: right_total_def)
+
lemma right_total_alt_def2:
"right_total R \<longleftrightarrow> ((R ===> op \<longrightarrow>) ===> op \<longrightarrow>) All All"
unfolding right_total_def rel_fun_def
@@ -452,6 +460,11 @@
shows "((A ===> op =) ===> op =) Ex Ex"
using assms unfolding bi_total_def rel_fun_def by fast
+lemma Ex1_parametric [transfer_rule]:
+ assumes [transfer_rule]: "bi_unique A" "bi_total A"
+ shows "((A ===> op =) ===> op =) Ex1 Ex1"
+unfolding Ex1_def[abs_def] by transfer_prover
+
declare If_transfer [transfer_rule]
lemma Let_transfer [transfer_rule]: "(A ===> (A ===> B) ===> B) Let Let"
@@ -520,13 +533,35 @@
by fast+
lemma right_unique_transfer [transfer_rule]:
- assumes [transfer_rule]: "right_total A"
- assumes [transfer_rule]: "right_total B"
- assumes [transfer_rule]: "bi_unique B"
- shows "((A ===> B ===> op=) ===> implies) right_unique right_unique"
-using assms unfolding right_unique_def[abs_def] right_total_def bi_unique_def rel_fun_def
+ "\<lbrakk> right_total A; right_total B; bi_unique B \<rbrakk>
+ \<Longrightarrow> ((A ===> B ===> op=) ===> implies) right_unique right_unique"
+unfolding right_unique_def[abs_def] right_total_def bi_unique_def rel_fun_def
by metis
+lemma left_total_parametric [transfer_rule]:
+ assumes [transfer_rule]: "bi_total A" "bi_total B"
+ shows "((A ===> B ===> op =) ===> op =) left_total left_total"
+unfolding left_total_def[abs_def] by transfer_prover
+
+lemma right_total_parametric [transfer_rule]:
+ assumes [transfer_rule]: "bi_total A" "bi_total B"
+ shows "((A ===> B ===> op =) ===> op =) right_total right_total"
+unfolding right_total_def[abs_def] by transfer_prover
+
+lemma left_unique_parametric [transfer_rule]:
+ assumes [transfer_rule]: "bi_unique A" "bi_total A" "bi_total B"
+ shows "((A ===> B ===> op =) ===> op =) left_unique left_unique"
+unfolding left_unique_def[abs_def] by transfer_prover
+
+lemma prod_pred_parametric [transfer_rule]:
+ "((A ===> op =) ===> (B ===> op =) ===> rel_prod A B ===> op =) pred_prod pred_prod"
+unfolding pred_prod_def[abs_def] Basic_BNFs.fsts_def Basic_BNFs.snds_def fstsp.simps sndsp.simps
+by simp transfer_prover
+
+lemma apfst_parametric [transfer_rule]:
+ "((A ===> B) ===> rel_prod A C ===> rel_prod B C) apfst apfst"
+unfolding apfst_def[abs_def] by transfer_prover
+
lemma rel_fun_eq_eq_onp: "(op= ===> eq_onp P) = eq_onp (\<lambda>f. \<forall>x. P(f x))"
unfolding eq_onp_def rel_fun_def by auto
@@ -578,6 +613,11 @@
}
qed
+lemma right_unique_parametric [transfer_rule]:
+ assumes [transfer_rule]: "bi_total A" "bi_unique B" "bi_total B"
+ shows "((A ===> B ===> op =) ===> op =) right_unique right_unique"
+unfolding right_unique_def[abs_def] by transfer_prover
+
end
end