# HG changeset patch
# User Andreas Lochbihler
# Date 1423663463 -3600
# Node ID 67deb7bed6d3a57c17e178201d35e943e35314f8
# Parent  ef65605a7d9ca70fd3b877140a3758a4a908a9b8# Parent  860fb1c6555302106b6a7fe167beb9f9245c2d70
merged

diff -r ef65605a7d9c -r 67deb7bed6d3 src/HOL/BNF_Def.thy
--- 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))"
 
diff -r ef65605a7d9c -r 67deb7bed6d3 src/HOL/Finite_Set.thy
--- 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 *}
 
diff -r ef65605a7d9c -r 67deb7bed6d3 src/HOL/Fun.thy
--- 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 "."
 
diff -r ef65605a7d9c -r 67deb7bed6d3 src/HOL/List.thy
--- 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
diff -r ef65605a7d9c -r 67deb7bed6d3 src/HOL/Option.thy
--- 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)
diff -r ef65605a7d9c -r 67deb7bed6d3 src/HOL/Partial_Function.thy
--- 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"
diff -r ef65605a7d9c -r 67deb7bed6d3 src/HOL/Relation.thy
--- 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 *}
 
diff -r ef65605a7d9c -r 67deb7bed6d3 src/HOL/Transfer.thy
--- 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