--- a/Admin/components/components.sha1 Wed Feb 11 18:16:33 2015 +0100
+++ b/Admin/components/components.sha1 Fri Feb 13 23:39:25 2015 +0100
@@ -1,5 +1,6 @@
70105fd6fbfd1a868383fc510772b95234325d31 csdp-6.x.tar.gz
2f6417b8e96a0e4e8354fe0f1a253c18fb55d9a7 cvc3-2.4.1.tar.gz
+03aec2ec5757301c9df149f115d1f4f1d2cafd9e cvc4-1.5pre.tar.gz
842d9526f37b928cf9e22f141884365129990d63 cygwin-20130110.tar.gz
cb3b0706d208f104b800267697204f6d82f7b48a cygwin-20130114.tar.gz
3b44cca04855016d5f8cfb5101b2e0579ab80197 cygwin-20130117.tar.gz
--- a/Admin/components/main Wed Feb 11 18:16:33 2015 +0100
+++ b/Admin/components/main Fri Feb 13 23:39:25 2015 +0100
@@ -1,6 +1,6 @@
#main components for everyday use, without big impact on overall build time
-cvc3-2.4.1
csdp-6.x
+cvc4-1.5pre
e-1.8
exec_process-1.0.3
Haskabelle-2014
--- a/NEWS Wed Feb 11 18:16:33 2015 +0100
+++ b/NEWS Fri Feb 13 23:39:25 2015 +0100
@@ -159,6 +159,8 @@
operations.
* Sledgehammer:
+ - CVC4 is now included with Isabelle instead of CVC3 and run by
+ default.
- Minimization is now always enabled by default.
Removed subcommand:
min
--- a/src/Doc/Sledgehammer/document/root.tex Wed Feb 11 18:16:33 2015 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex Fri Feb 13 23:39:25 2015 +0100
@@ -164,7 +164,7 @@
\begin{sloppy}
\begin{enum}
\item[\labelitemi] If you installed an official Isabelle package, it should
-already include properly setup executables for CVC3, E, SPASS, and Z3, ready to use.%
+already include properly setup executables for CVC4, E, SPASS, and Z3, ready to use.%
\footnote{Vampire's license prevents us from doing the same for
this otherwise remarkable tool.}
For Z3, you must additionally set the variable
@@ -174,13 +174,14 @@
via the ``Z3 Non Commercial'' option under ``Plugins > Plugin Options
> Isabelle > General'' in Isabelle/jEdit.
-\item[\labelitemi] Alternatively, you can download the Isabelle-aware CVC3, E,
-SPASS, and Z3 binary packages from \download. Extract the archives, then add a
-line to your \texttt{\$ISABELLE\_HOME\_USER\slash etc\slash components}%
+\item[\labelitemi] Alternatively, you can download the Isabelle-aware CVC3,
+CVC4, E, SPASS, and Z3 binary packages from \download. Extract the archives,
+then add a line to your \texttt{\$ISABELLE\_HOME\_USER\slash etc\slash
+components}%
\footnote{The variable \texttt{\$ISABELLE\_HOME\_USER} is set by Isabelle at
startup. Its value can be retrieved by executing \texttt{isabelle}
\texttt{getenv} \texttt{ISABELLE\_HOME\_USER} on the command line.}
-file with the absolute path to CVC3, E, SPASS, or Z3. For example, if the
+file with the absolute path to CVC3, CVC4, E, SPASS, or Z3. For example, if the
\texttt{components} file does not exist yet and you extracted SPASS to
\texttt{/usr/local/spass-3.8ds}, create it with the single line
@@ -942,13 +943,10 @@
runs on Geoff Sutcliffe's Miami servers.
\end{enum}
-By default, Sledgehammer runs a selection of CVC3, E, E-SInE, SPASS, Vampire,
-and Z3 in parallel---either locally or remotely, depending on the number of
-processor cores available.
-
-It is generally a good idea to run several provers in parallel. Running E,
-SPASS, and Vampire for 5~seconds yields a similar success rate to running the
-most effective of these for 120~seconds \cite{boehme-nipkow-2010}.
+By default, Sledgehammer runs a subset of CVC4, E, E-SInE, SPASS, Vampire,
+veriT, and Z3 in parallel---either locally or remotely, depending on the number
+of processor cores available and on which provers are actually installed.
+It is generally a good idea to run several provers in parallel.
\opnodefault{prover}{string}
Alias for \textit{provers}.
--- a/src/HOL/BNF_Def.thy Wed Feb 11 18:16:33 2015 +0100
+++ b/src/HOL/BNF_Def.thy Fri Feb 13 23:39:25 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/Equiv_Relations.thy Wed Feb 11 18:16:33 2015 +0100
+++ b/src/HOL/Equiv_Relations.thy Fri Feb 13 23:39:25 2015 +0100
@@ -160,6 +160,32 @@
apply blast
done
+subsection {* Refinement of one equivalence relation WRT another *}
+
+lemma refines_equiv_class_eq:
+ "\<lbrakk>R \<subseteq> S; equiv A R; equiv A S\<rbrakk> \<Longrightarrow> R``(S``{a}) = S``{a}"
+ by (auto simp: equiv_class_eq_iff)
+
+lemma refines_equiv_class_eq2:
+ "\<lbrakk>R \<subseteq> S; equiv A R; equiv A S\<rbrakk> \<Longrightarrow> S``(R``{a}) = S``{a}"
+ by (auto simp: equiv_class_eq_iff)
+
+lemma refines_equiv_image_eq:
+ "\<lbrakk>R \<subseteq> S; equiv A R; equiv A S\<rbrakk> \<Longrightarrow> (\<lambda>X. S``X) ` (A//R) = A//S"
+ by (auto simp: quotient_def image_UN refines_equiv_class_eq2)
+
+lemma finite_refines_finite:
+ "\<lbrakk>finite (A//R); R \<subseteq> S; equiv A R; equiv A S\<rbrakk> \<Longrightarrow> finite (A//S)"
+ apply (erule finite_surj [where f = "\<lambda>X. S``X"])
+ apply (simp add: refines_equiv_image_eq)
+ done
+
+lemma finite_refines_card_le:
+ "\<lbrakk>finite (A//R); R \<subseteq> S; equiv A R; equiv A S\<rbrakk> \<Longrightarrow> card (A//S) \<le> card (A//R)"
+ apply (subst refines_equiv_image_eq [of R S A, symmetric])
+ apply (auto simp: card_image_le [where f = "\<lambda>X. S``X"])
+ done
+
subsection {* Defining unary operations upon equivalence classes *}
--- a/src/HOL/Finite_Set.thy Wed Feb 11 18:16:33 2015 +0100
+++ b/src/HOL/Finite_Set.thy Fri Feb 13 23:39:25 2015 +0100
@@ -262,6 +262,10 @@
"finite {x. P x} \<Longrightarrow> finite { f x | x. P x }"
by (simp add: image_Collect [symmetric])
+lemma finite_image_set2:
+ "finite {x. P x} \<Longrightarrow> finite {y. Q y} \<Longrightarrow> finite {f x y | x y. P x \<and> Q y}"
+ by (rule finite_subset [where B = "\<Union>x \<in> {x. P x}. \<Union>y \<in> {y. Q y}. {f x y}"]) auto
+
lemma finite_imageD:
assumes "finite (f ` A)" and "inj_on f A"
shows "finite A"
@@ -311,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)
@@ -1618,6 +1619,9 @@
by (force intro: card_mono simp: card_image [symmetric])
qed
+lemma surj_card_le: "finite A \<Longrightarrow> B \<subseteq> f ` A \<Longrightarrow> card B \<le> card A"
+ by (blast intro: card_image_le card_mono le_trans)
+
lemma card_bij_eq:
"[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A;
finite A; finite B |] ==> card A = card B"
@@ -1634,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 18:16:33 2015 +0100
+++ b/src/HOL/Fun.thy Fri Feb 13 23:39:25 2015 +0100
@@ -15,6 +15,12 @@
"f x = u \<Longrightarrow> (\<And>x. P x \<Longrightarrow> g (f x) = x) \<Longrightarrow> P x \<Longrightarrow> x = g u"
by auto
+text{*Uniqueness, so NOT the axiom of choice.*}
+lemma uniq_choice: "\<forall>x. \<exists>!y. Q x y \<Longrightarrow> \<exists>f. \<forall>x. Q x (f x)"
+ by (force intro: theI')
+
+lemma b_uniq_choice: "\<forall>x\<in>S. \<exists>!y. Q x y \<Longrightarrow> \<exists>f. \<forall>x\<in>S. Q x (f x)"
+ by (force intro: theI')
subsection {* The Identity Function @{text id} *}
@@ -79,6 +85,15 @@
"f -` (g -` x) = (g \<circ> f) -` x"
by auto
+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 "."
@@ -477,14 +492,17 @@
lemma image_set_diff: "inj f ==> f`(A-B) = f`A - f`B"
by (simp add: inj_on_def, blast)
-lemma inj_image_mem_iff: "inj f ==> (f a : f`A) = (a : A)"
-by (blast dest: injD)
+lemma inj_on_image_mem_iff: "\<lbrakk>inj_on f B; a \<in> B; A \<subseteq> B\<rbrakk> \<Longrightarrow> f a \<in> f`A \<longleftrightarrow> a \<in> A"
+ by (auto simp: inj_on_def)
+
+lemma inj_image_mem_iff: "inj f \<Longrightarrow> f a \<in> f`A \<longleftrightarrow> a \<in> A"
+ by (blast dest: injD)
lemma inj_image_subset_iff: "inj f ==> (f`A <= f`B) = (A<=B)"
-by (simp add: inj_on_def, blast)
+ by (blast dest: injD)
lemma inj_image_eq_iff: "inj f ==> (f`A = f`B) = (A = B)"
-by (blast dest: injD)
+ by (blast dest: injD)
lemma surj_Compl_image_subset: "surj f ==> -(f`A) <= f`(-A)"
by auto
--- a/src/HOL/HOL.thy Wed Feb 11 18:16:33 2015 +0100
+++ b/src/HOL/HOL.thy Fri Feb 13 23:39:25 2015 +0100
@@ -550,63 +550,6 @@
done
-subsubsection {*THE: definite description operator*}
-
-lemma the_equality:
- assumes prema: "P a"
- and premx: "!!x. P x ==> x=a"
- shows "(THE x. P x) = a"
-apply (rule trans [OF _ the_eq_trivial])
-apply (rule_tac f = "The" in arg_cong)
-apply (rule ext)
-apply (rule iffI)
- apply (erule premx)
-apply (erule ssubst, rule prema)
-done
-
-lemma theI:
- assumes "P a" and "!!x. P x ==> x=a"
- shows "P (THE x. P x)"
-by (iprover intro: assms the_equality [THEN ssubst])
-
-lemma theI': "EX! x. P x ==> P (THE x. P x)"
-apply (erule ex1E)
-apply (erule theI)
-apply (erule allE)
-apply (erule mp)
-apply assumption
-done
-
-(*Easier to apply than theI: only one occurrence of P*)
-lemma theI2:
- assumes "P a" "!!x. P x ==> x=a" "!!x. P x ==> Q x"
- shows "Q (THE x. P x)"
-by (iprover intro: assms theI)
-
-lemma the1I2: assumes "EX! x. P x" "\<And>x. P x \<Longrightarrow> Q x" shows "Q (THE x. P x)"
-by(iprover intro:assms(2) theI2[where P=P and Q=Q] ex1E[OF assms(1)]
- elim:allE impE)
-
-lemma the1_equality [elim?]: "[| EX!x. P x; P a |] ==> (THE x. P x) = a"
-apply (rule the_equality)
-apply assumption
-apply (erule ex1E)
-apply (erule all_dupE)
-apply (drule mp)
-apply assumption
-apply (erule ssubst)
-apply (erule allE)
-apply (erule mp)
-apply assumption
-done
-
-lemma the_sym_eq_trivial: "(THE y. x=y) = x"
-apply (rule the_equality)
-apply (rule refl)
-apply (erule sym)
-done
-
-
subsubsection {*Classical intro rules for disjunction and existential quantifiers*}
lemma disjCI:
@@ -876,7 +819,6 @@
declare ex_ex1I [intro!]
and allI [intro!]
- and the_equality [intro]
and exI [intro]
declare exE [elim!]
@@ -925,6 +867,39 @@
*}
+subsubsection {*THE: definite description operator*}
+
+lemma the_equality [intro]:
+ assumes "P a"
+ and "!!x. P x ==> x=a"
+ shows "(THE x. P x) = a"
+ by (blast intro: assms trans [OF arg_cong [where f=The] the_eq_trivial])
+
+lemma theI:
+ assumes "P a" and "!!x. P x ==> x=a"
+ shows "P (THE x. P x)"
+by (iprover intro: assms the_equality [THEN ssubst])
+
+lemma theI': "EX! x. P x ==> P (THE x. P x)"
+ by (blast intro: theI)
+
+(*Easier to apply than theI: only one occurrence of P*)
+lemma theI2:
+ assumes "P a" "!!x. P x ==> x=a" "!!x. P x ==> Q x"
+ shows "Q (THE x. P x)"
+by (iprover intro: assms theI)
+
+lemma the1I2: assumes "EX! x. P x" "\<And>x. P x \<Longrightarrow> Q x" shows "Q (THE x. P x)"
+by(iprover intro:assms(2) theI2[where P=P and Q=Q] ex1E[OF assms(1)]
+ elim:allE impE)
+
+lemma the1_equality [elim?]: "[| EX!x. P x; P a |] ==> (THE x. P x) = a"
+ by blast
+
+lemma the_sym_eq_trivial: "(THE y. x=y) = x"
+ by blast
+
+
subsubsection {* Simplifier *}
lemma eta_contract_eq: "(%s. f s) = f" ..
@@ -1100,8 +1075,7 @@
lemma if_bool_eq_disj: "(if P then Q else R) = ((P&Q) | (~P&R))"
-- {* And this form is useful for expanding @{text "if"}s on the LEFT. *}
- apply (simplesubst split_if, blast)
- done
+ by (simplesubst split_if) blast
lemma Eq_TrueI: "P ==> P == True" by (unfold atomize_eq) iprover
lemma Eq_FalseI: "~P ==> P == False" by (unfold atomize_eq) iprover
--- a/src/HOL/Library/Infinite_Set.thy Wed Feb 11 18:16:33 2015 +0100
+++ b/src/HOL/Library/Infinite_Set.thy Fri Feb 13 23:39:25 2015 +0100
@@ -238,7 +238,7 @@
from inf have "infinite {x. P x}" unfolding Inf_many_def .
moreover from q have "{x. P x} \<subseteq> {x. Q x}" by auto
ultimately show ?thesis
- by (simp add: Inf_many_def infinite_super)
+ using Inf_many_def infinite_super by blast
qed
lemma MOST_mono: "\<forall>\<^sub>\<infinity>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> \<forall>\<^sub>\<infinity>x. Q x"
--- a/src/HOL/Library/Nat_Bijection.thy Wed Feb 11 18:16:33 2015 +0100
+++ b/src/HOL/Library/Nat_Bijection.thy Fri Feb 13 23:39:25 2015 +0100
@@ -293,6 +293,9 @@
lemma set_encode_empty [simp]: "set_encode {} = 0"
by (simp add: set_encode_def)
+lemma set_encode_inf: "~ finite A \<Longrightarrow> set_encode A = 0"
+ by (simp add: set_encode_def)
+
lemma set_encode_insert [simp]:
"\<lbrakk>finite A; n \<notin> A\<rbrakk> \<Longrightarrow> set_encode (insert n A) = 2^n + set_encode A"
by (simp add: set_encode_def)
--- a/src/HOL/List.thy Wed Feb 11 18:16:33 2015 +0100
+++ b/src/HOL/List.thy Fri Feb 13 23:39:25 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 18:16:33 2015 +0100
+++ b/src/HOL/Option.thy Fri Feb 13 23:39:25 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 18:16:33 2015 +0100
+++ b/src/HOL/Partial_Function.thy Fri Feb 13 23:39:25 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/Probability/Giry_Monad.thy Wed Feb 11 18:16:33 2015 +0100
+++ b/src/HOL/Probability/Giry_Monad.thy Fri Feb 13 23:39:25 2015 +0100
@@ -142,6 +142,20 @@
"subprob_space (null_measure M) \<longleftrightarrow> space M \<noteq> {}"
by (auto intro!: subprob_spaceI dest: subprob_space.subprob_not_empty)
+lemma subprob_space_restrict_space:
+ assumes M: "subprob_space M"
+ and A: "A \<inter> space M \<in> sets M" "A \<inter> space M \<noteq> {}"
+ shows "subprob_space (restrict_space M A)"
+proof(rule subprob_spaceI)
+ have "emeasure (restrict_space M A) (space (restrict_space M A)) = emeasure M (A \<inter> space M)"
+ using A by(simp add: emeasure_restrict_space space_restrict_space)
+ also have "\<dots> \<le> 1" by(rule subprob_space.subprob_emeasure_le_1)(rule M)
+ finally show "emeasure (restrict_space M A) (space (restrict_space M A)) \<le> 1" .
+next
+ show "space (restrict_space M A) \<noteq> {}"
+ using A by(simp add: space_restrict_space)
+qed
+
definition subprob_algebra :: "'a measure \<Rightarrow> 'a measure measure" where
"subprob_algebra K =
(\<Squnion>\<^sub>\<sigma> A\<in>sets K. vimage_algebra {M. subprob_space M \<and> sets M = sets K} (\<lambda>M. emeasure M A) borel)"
--- a/src/HOL/Probability/Probability_Mass_Function.thy Wed Feb 11 18:16:33 2015 +0100
+++ b/src/HOL/Probability/Probability_Mass_Function.thy Fri Feb 13 23:39:25 2015 +0100
@@ -502,6 +502,12 @@
shows "(\<integral>x. f x \<partial>bernoulli_pmf p) = f True * p + f False * (1 - p)"
by (subst integral_measure_pmf[of UNIV]) (auto simp: UNIV_bool)
+lemma pmf_bernoulli_half [simp]: "pmf (bernoulli_pmf (1 / 2)) x = 1 / 2"
+by(cases x) simp_all
+
+lemma measure_pmf_bernoulli_half: "measure_pmf (bernoulli_pmf (1 / 2)) = uniform_count_measure UNIV"
+by(rule measure_eqI)(simp_all add: nn_integral_pmf[symmetric] emeasure_uniform_count_measure nn_integral_count_space_finite sets_uniform_count_measure)
+
subsubsection \<open> Geometric Distribution \<close>
lift_definition geometric_pmf :: "nat pmf" is "\<lambda>n. 1 / 2^Suc n"
@@ -639,7 +645,7 @@
"(\<lambda>x. measure_pmf (M x)) \<in> measurable (count_space UNIV) (subprob_algebra (count_space UNIV))"
by (auto simp: space_subprob_algebra intro!: prob_space_imp_subprob_space) unfold_locales
-lemma bind_pmf_cong:
+lemma bind_measure_pmf_cong:
assumes "\<And>x. A x \<in> space (subprob_algebra N)" "\<And>x. B x \<in> space (subprob_algebra N)"
assumes "\<And>i. i \<in> set_pmf x \<Longrightarrow> A i = B i"
shows "bind (measure_pmf x) A = bind (measure_pmf x) B"
@@ -879,6 +885,16 @@
unfolding bind_return_pmf''[symmetric] join_eq_bind_pmf bind_assoc_pmf
by (simp add: bind_return_pmf'')
+lemma bind_pmf_cong:
+ "\<lbrakk> p = q; \<And>x. x \<in> set_pmf q \<Longrightarrow> f x = g x \<rbrakk>
+ \<Longrightarrow> bind_pmf p f = bind_pmf q g"
+by(simp add: bind_pmf_def cong: map_pmf_cong)
+
+lemma bind_pmf_cong_simp:
+ "\<lbrakk> p = q; \<And>x. x \<in> set_pmf q =simp=> f x = g x \<rbrakk>
+ \<Longrightarrow> bind_pmf p f = bind_pmf q g"
+by(simp add: simp_implies_def cong: bind_pmf_cong)
+
definition "pair_pmf A B = bind_pmf A (\<lambda>x. bind_pmf B (\<lambda>y. return_pmf (x, y)))"
lemma pmf_pair: "pmf (pair_pmf M N) (a, b) = pmf M a * pmf N b"
@@ -1062,29 +1078,32 @@
qed
lemma bind_cond_pmf_cancel:
- assumes in_S: "\<And>x. x \<in> set_pmf p \<Longrightarrow> x \<in> S x"
+ assumes in_S: "\<And>x. x \<in> set_pmf p \<Longrightarrow> x \<in> S x" "\<And>x. x \<in> set_pmf q \<Longrightarrow> x \<in> S x"
assumes S_eq: "\<And>x y. x \<in> S y \<Longrightarrow> S x = S y"
- shows "bind_pmf p (\<lambda>x. cond_pmf p (S x)) = p"
+ and same: "\<And>x. measure (measure_pmf p) (S x) = measure (measure_pmf q) (S x)"
+ shows "bind_pmf p (\<lambda>x. cond_pmf q (S x)) = q" (is "?lhs = _")
proof (rule pmf_eqI)
- have [simp]: "\<And>x. x \<in> p \<Longrightarrow> p \<inter> (S x) \<noteq> {}"
- using in_S by auto
+ { fix x
+ assume "x \<in> set_pmf p"
+ hence "set_pmf p \<inter> (S x) \<noteq> {}" using in_S by auto
+ hence "measure (measure_pmf p) (S x) \<noteq> 0"
+ by(auto simp add: measure_pmf.prob_eq_0 AE_measure_pmf_iff)
+ with same have "measure (measure_pmf q) (S x) \<noteq> 0" by simp
+ hence "set_pmf q \<inter> S x \<noteq> {}"
+ by(auto simp add: measure_pmf.prob_eq_0 AE_measure_pmf_iff) }
+ note [simp] = this
+
fix z
- have pmf_le: "pmf p z \<le> measure p (S z)"
- proof cases
- assume "z \<in> p" from in_S[OF this] show ?thesis
- by (auto intro!: measure_pmf.finite_measure_mono simp: pmf.rep_eq)
- qed (simp add: set_pmf_iff measure_nonneg)
+ have pmf_q_z: "z \<notin> S z \<Longrightarrow> pmf q z = 0"
+ by(erule contrapos_np)(simp add: pmf_eq_0_set_pmf in_S)
- have "ereal (pmf (bind_pmf p (\<lambda>x. cond_pmf p (S x))) z) =
- (\<integral>\<^sup>+ x. ereal (pmf p z / measure p (S z)) * indicator (S z) x \<partial>p)"
- by (subst ereal_pmf_bind)
- (auto intro!: nn_integral_cong_AE dest!: S_eq split: split_indicator
- simp: AE_measure_pmf_iff pmf_cond pmf_eq_0_set_pmf in_S)
- also have "\<dots> = pmf p z"
- using pmf_le pmf_nonneg[of p z]
- by (subst nn_integral_cmult) (simp_all add: measure_nonneg measure_pmf.emeasure_eq_measure)
- finally show "pmf (bind_pmf p (\<lambda>x. cond_pmf p (S x))) z = pmf p z"
- by simp
+ have "ereal (pmf ?lhs z) = \<integral>\<^sup>+ x. ereal (pmf (cond_pmf q (S x)) z) \<partial>measure_pmf p"
+ by(simp add: ereal_pmf_bind)
+ also have "\<dots> = \<integral>\<^sup>+ x. ereal (pmf q z / measure p (S z)) * indicator (S z) x \<partial>measure_pmf p"
+ by(rule nn_integral_cong_AE)(auto simp add: AE_measure_pmf_iff pmf_cond same pmf_q_z in_S dest!: S_eq split: split_indicator)
+ also have "\<dots> = pmf q z" using pmf_nonneg[of q z]
+ by (subst nn_integral_cmult)(auto simp add: measure_nonneg measure_pmf.emeasure_eq_measure same measure_pmf.prob_eq_0 AE_measure_pmf_iff pmf_eq_0_set_pmf in_S)
+ finally show "pmf ?lhs z = pmf q z" by simp
qed
inductive rel_pmf :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a pmf \<Rightarrow> 'b pmf \<Rightarrow> bool"
@@ -1235,5 +1254,140 @@
map_pair)
qed
+lemma rel_pmf_reflI:
+ assumes "\<And>x. x \<in> set_pmf p \<Longrightarrow> P x x"
+ shows "rel_pmf P p p"
+by(rule rel_pmf.intros[where pq="map_pmf (\<lambda>x. (x, x)) p"])(auto simp add: pmf.map_comp o_def set_map_pmf assms)
+
+lemma rel_pmf_joinI:
+ assumes "rel_pmf (rel_pmf P) p q"
+ shows "rel_pmf P (join_pmf p) (join_pmf q)"
+proof -
+ from assms obtain pq where p: "p = map_pmf fst pq"
+ and q: "q = map_pmf snd pq"
+ and P: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> rel_pmf P x y"
+ by cases auto
+ from P obtain PQ
+ where PQ: "\<And>x y a b. \<lbrakk> (x, y) \<in> set_pmf pq; (a, b) \<in> set_pmf (PQ x y) \<rbrakk> \<Longrightarrow> P a b"
+ and x: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> map_pmf fst (PQ x y) = x"
+ and y: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> map_pmf snd (PQ x y) = y"
+ by(metis rel_pmf.simps)
+
+ let ?r = "bind_pmf pq (\<lambda>(x, y). PQ x y)"
+ have "\<And>a b. (a, b) \<in> set_pmf ?r \<Longrightarrow> P a b" by(auto simp add: set_bind_pmf intro: PQ)
+ moreover have "map_pmf fst ?r = join_pmf p" "map_pmf snd ?r = join_pmf q"
+ by(simp_all add: bind_pmf_def map_join_pmf pmf.map_comp o_def split_def p q x y cong: pmf.map_cong)
+ ultimately show ?thesis ..
+qed
+
+lemma rel_pmf_bindI:
+ assumes pq: "rel_pmf R p q"
+ and fg: "\<And>x y. R x y \<Longrightarrow> rel_pmf P (f x) (g y)"
+ shows "rel_pmf P (bind_pmf p f) (bind_pmf q g)"
+unfolding bind_pmf_def
+by(rule rel_pmf_joinI)(auto simp add: pmf.rel_map intro: pmf.rel_mono[THEN le_funD, THEN le_funD, THEN le_boolD, THEN mp, OF _ pq] fg)
+
+text {*
+ Proof that @{const rel_pmf} preserves orders.
+ Antisymmetry proof follows Thm. 1 in N. Saheb-Djahromi, Cpo's of measures for nondeterminism,
+ Theoretical Computer Science 12(1):19--37, 1980,
+ @{url "http://dx.doi.org/10.1016/0304-3975(80)90003-1"}
+*}
+
+lemma
+ assumes *: "rel_pmf R p q"
+ and refl: "reflp R" and trans: "transp R"
+ shows measure_Ici: "measure p {y. R x y} \<le> measure q {y. R x y}" (is ?thesis1)
+ and measure_Ioi: "measure p {y. R x y \<and> \<not> R y x} \<le> measure q {y. R x y \<and> \<not> R y x}" (is ?thesis2)
+proof -
+ from * obtain pq
+ where pq: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> R x y"
+ and p: "p = map_pmf fst pq"
+ and q: "q = map_pmf snd pq"
+ by cases auto
+ show ?thesis1 ?thesis2 unfolding p q map_pmf.rep_eq using refl trans
+ by(auto 4 3 simp add: measure_distr reflpD AE_measure_pmf_iff intro!: measure_pmf.finite_measure_mono_AE dest!: pq elim: transpE)
+qed
+
+lemma rel_pmf_inf:
+ fixes p q :: "'a pmf"
+ assumes 1: "rel_pmf R p q"
+ assumes 2: "rel_pmf R q p"
+ and refl: "reflp R" and trans: "transp R"
+ shows "rel_pmf (inf R R\<inverse>\<inverse>) p q"
+proof
+ let ?E = "\<lambda>x. {y. R x y \<and> R y x}"
+ let ?\<mu>E = "\<lambda>x. measure q (?E x)"
+ { fix x
+ have "measure p (?E x) = measure p ({y. R x y} - {y. R x y \<and> \<not> R y x})"
+ by(auto intro!: arg_cong[where f="measure p"])
+ also have "\<dots> = measure p {y. R x y} - measure p {y. R x y \<and> \<not> R y x}"
+ by (rule measure_pmf.finite_measure_Diff) auto
+ also have "measure p {y. R x y \<and> \<not> R y x} = measure q {y. R x y \<and> \<not> R y x}"
+ using 1 2 refl trans by(auto intro!: Orderings.antisym measure_Ioi)
+ also have "measure p {y. R x y} = measure q {y. R x y}"
+ using 1 2 refl trans by(auto intro!: Orderings.antisym measure_Ici)
+ also have "measure q {y. R x y} - measure q {y. R x y \<and> ~ R y x} =
+ measure q ({y. R x y} - {y. R x y \<and> \<not> R y x})"
+ by(rule measure_pmf.finite_measure_Diff[symmetric]) auto
+ also have "\<dots> = ?\<mu>E x"
+ by(auto intro!: arg_cong[where f="measure q"])
+ also note calculation }
+ note eq = this
+
+ def pq \<equiv> "bind_pmf p (\<lambda>x. bind_pmf (cond_pmf q (?E x)) (\<lambda>y. return_pmf (x, y)))"
+
+ show "map_pmf fst pq = p"
+ by(simp add: pq_def map_bind_pmf map_return_pmf bind_return_pmf')
+
+ show "map_pmf snd pq = q"
+ unfolding pq_def map_bind_pmf map_return_pmf bind_return_pmf' snd_conv
+ by(subst bind_cond_pmf_cancel)(auto simp add: reflpD[OF \<open>reflp R\<close>] eq intro: transpD[OF \<open>transp R\<close>])
+
+ fix x y
+ assume "(x, y) \<in> set_pmf pq"
+ moreover
+ { assume "x \<in> set_pmf p"
+ hence "measure (measure_pmf p) (?E x) \<noteq> 0"
+ by(auto simp add: measure_pmf.prob_eq_0 AE_measure_pmf_iff intro: reflpD[OF \<open>reflp R\<close>])
+ hence "measure (measure_pmf q) (?E x) \<noteq> 0" using eq by simp
+ hence "set_pmf q \<inter> {y. R x y \<and> R y x} \<noteq> {}"
+ by(auto simp add: measure_pmf.prob_eq_0 AE_measure_pmf_iff) }
+ ultimately show "inf R R\<inverse>\<inverse> x y"
+ by(auto simp add: pq_def set_bind_pmf set_return_pmf set_cond_pmf)
+qed
+
+lemma rel_pmf_antisym:
+ fixes p q :: "'a pmf"
+ assumes 1: "rel_pmf R p q"
+ assumes 2: "rel_pmf R q p"
+ and refl: "reflp R" and trans: "transp R" and antisym: "antisymP R"
+ shows "p = q"
+proof -
+ from 1 2 refl trans have "rel_pmf (inf R R\<inverse>\<inverse>) p q" by(rule rel_pmf_inf)
+ also have "inf R R\<inverse>\<inverse> = op ="
+ using refl antisym by(auto intro!: ext simp add: reflpD dest: antisymD)
+ finally show ?thesis unfolding pmf.rel_eq .
+qed
+
+lemma reflp_rel_pmf: "reflp R \<Longrightarrow> reflp (rel_pmf R)"
+by(blast intro: reflpI rel_pmf_reflI reflpD)
+
+lemma antisymP_rel_pmf:
+ "\<lbrakk> reflp R; transp R; antisymP R \<rbrakk>
+ \<Longrightarrow> antisymP (rel_pmf R)"
+by(rule antisymI)(blast intro: rel_pmf_antisym)
+
+lemma transp_rel_pmf:
+ assumes "transp R"
+ shows "transp (rel_pmf R)"
+proof (rule transpI)
+ fix x y z
+ assume "rel_pmf R x y" and "rel_pmf R y z"
+ hence "rel_pmf (R OO R) x z" by (simp add: pmf.rel_compp relcompp.relcompI)
+ thus "rel_pmf R x z"
+ using assms by (metis (no_types) pmf.rel_mono rev_predicate2D transp_relcompp_less_eq)
+qed
+
end
--- a/src/HOL/Relation.thy Wed Feb 11 18:16:33 2015 +0100
+++ b/src/HOL/Relation.thy Fri Feb 13 23:39:25 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/Set.thy Wed Feb 11 18:16:33 2015 +0100
+++ b/src/HOL/Set.thy Fri Feb 13 23:39:25 2015 +0100
@@ -1020,6 +1020,9 @@
"f ` A - f ` B \<subseteq> f ` (A - B)"
by blast
+lemma Setcompr_eq_image: "{f x | x. x \<in> A} = f ` A"
+ by blast
+
lemma ball_imageD:
assumes "\<forall>x\<in>f ` A. P x"
shows "\<forall>x\<in>A. P (f x)"
@@ -1055,7 +1058,7 @@
"{u. \<exists>x. u = f x} = range f"
by auto
-lemma range_composition:
+lemma range_composition:
"range (\<lambda>x. f (g x)) = f ` range g"
by auto
@@ -1241,6 +1244,9 @@
lemma Collect_conj_eq: "{x. P x & Q x} = {x. P x} \<inter> {x. Q x}"
by blast
+lemma Collect_mono_iff: "Collect P \<subseteq> Collect Q \<longleftrightarrow> (\<forall>x. P x \<longrightarrow> Q x)"
+ by blast
+
text {* \medskip @{text insert}. *}
@@ -1803,7 +1809,7 @@
by blast
lemma image_subset_iff_subset_vimage: "f ` A \<subseteq> B \<longleftrightarrow> A \<subseteq> f -` B"
- by blast
+ by blast
lemma vimage_const [simp]: "((\<lambda>x. c) -` A) = (if c \<in> A then UNIV else {})"
by auto
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Wed Feb 11 18:16:33 2015 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Fri Feb 13 23:39:25 2015 +0100
@@ -27,7 +27,8 @@
open Sledgehammer_MaSh
open Sledgehammer
-(* val cvc3N = "cvc3" *)
+val cvc4N = "cvc4"
+val veritN = "verit"
val z3N = "z3"
val runN = "run"
@@ -180,7 +181,7 @@
(* The first ATP of the list is used by Auto Sledgehammer. *)
fun default_provers_param_value mode ctxt =
- [eN, spassN, z3N, vampireN, e_sineN]
+ [spassN, cvc4N, vampireN, eN, z3N, veritN, e_sineN]
|> map_filter (remotify_prover_if_not_installed ctxt)
(* In "try" mode, leave at least one thread to another slow tool (e.g. Nitpick) *)
|> take (Multithreading.max_threads_value () - (if mode = Try then 1 else 0))
--- a/src/HOL/Transfer.thy Wed Feb 11 18:16:33 2015 +0100
+++ b/src/HOL/Transfer.thy Fri Feb 13 23:39:25 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