--- a/NEWS Thu Mar 06 15:29:18 2014 +0100
+++ b/NEWS Thu Mar 06 15:40:33 2014 +0100
@@ -195,6 +195,7 @@
map_pair ~> map_prod
prod_rel ~> rel_prod
sum_rel ~> rel_sum
+ fun_rel ~> rel_fun
set_rel ~> rel_set
filter_rel ~> rel_filter
fset_rel ~> rel_fset (in "Library/FSet.thy")
--- a/src/Doc/Datatypes/Datatypes.thy Thu Mar 06 15:29:18 2014 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy Thu Mar 06 15:40:33 2014 +0100
@@ -2380,7 +2380,7 @@
lift_definition
rel_fn :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('d, 'a) fn \<Rightarrow> ('d, 'b) fn \<Rightarrow> bool"
is
- "fun_rel (op =)" .
+ "rel_fun (op =)" .
text {* \blankline *}
@@ -2423,7 +2423,7 @@
next
fix R S
show "rel_fn R OO rel_fn S \<le> rel_fn (R OO S)"
- by (rule, transfer) (auto simp add: fun_rel_def)
+ by (rule, transfer) (auto simp add: rel_fun_def)
next
fix R
show "rel_fn R =
@@ -2431,7 +2431,7 @@
BNF_Util.Grp {x. set_fn x \<subseteq> Collect (split R)} (map_fn snd)"
unfolding Grp_def fun_eq_iff relcompp.simps conversep.simps
apply transfer
- unfolding fun_rel_def subset_iff image_iff
+ unfolding rel_fun_def subset_iff image_iff
by auto (force, metis pair_collapse)
qed
--- a/src/HOL/BNF_Def.thy Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/BNF_Def.thy Thu Mar 06 15:40:33 2014 +0100
@@ -140,8 +140,8 @@
lemma vimage2pI: "R (f x) (g y) \<Longrightarrow> vimage2p f g R x y"
unfolding vimage2p_def by -
-lemma fun_rel_iff_leq_vimage2p: "(fun_rel R S) f g = (R \<le> vimage2p f g S)"
- unfolding fun_rel_def vimage2p_def by auto
+lemma rel_fun_iff_leq_vimage2p: "(rel_fun R S) f g = (R \<le> vimage2p f g S)"
+ unfolding rel_fun_def vimage2p_def by auto
lemma convol_image_vimage2p: "<f o fst, g o snd> ` Collect (split (vimage2p f g R)) \<subseteq> Collect (split R)"
unfolding vimage2p_def convol_def by auto
--- a/src/HOL/BNF_FP_Base.thy Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/BNF_FP_Base.thy Thu Mar 06 15:40:33 2014 +0100
@@ -131,9 +131,9 @@
lemma case_sum_o_map_sum_id: "(case_sum id g o map_sum f id) x = case_sum (f o id) g x"
unfolding case_sum_o_map_sum id_comp comp_id ..
-lemma fun_rel_def_butlast:
- "fun_rel R (fun_rel S T) f g = (\<forall>x y. R x y \<longrightarrow> (fun_rel S T) (f x) (g y))"
- unfolding fun_rel_def ..
+lemma rel_fun_def_butlast:
+ "rel_fun R (rel_fun S T) f g = (\<forall>x y. R x y \<longrightarrow> (rel_fun S T) (f x) (g y))"
+ unfolding rel_fun_def ..
lemma subst_eq_imp: "(\<forall>a b. a = b \<longrightarrow> P a b) \<equiv> (\<forall>a. P a a)"
by auto
--- a/src/HOL/BNF_GFP.thy Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/BNF_GFP.thy Thu Mar 06 15:40:33 2014 +0100
@@ -233,11 +233,11 @@
lemma image2pE: "\<lbrakk>image2p f g R fx gy; (\<And>x y. fx = f x \<Longrightarrow> gy = g y \<Longrightarrow> R x y \<Longrightarrow> P)\<rbrakk> \<Longrightarrow> P"
unfolding image2p_def by blast
-lemma fun_rel_iff_geq_image2p: "fun_rel R S f g = (image2p f g R \<le> S)"
- unfolding fun_rel_def image2p_def by auto
+lemma rel_fun_iff_geq_image2p: "rel_fun R S f g = (image2p f g R \<le> S)"
+ unfolding rel_fun_def image2p_def by auto
-lemma fun_rel_image2p: "fun_rel R (image2p f g R) f g"
- unfolding fun_rel_def image2p_def by auto
+lemma rel_fun_image2p: "rel_fun R (image2p f g R) f g"
+ unfolding rel_fun_def image2p_def by auto
subsection {* Equivalence relations, quotients, and Hilbert's choice *}
--- a/src/HOL/BNF_LFP.thy Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/BNF_LFP.thy Thu Mar 06 15:40:33 2014 +0100
@@ -244,14 +244,14 @@
ultimately show P by (blast intro: assms(3))
qed
-lemma vimage2p_fun_rel: "fun_rel (vimage2p f g R) R f g"
- unfolding fun_rel_def vimage2p_def by auto
+lemma vimage2p_rel_fun: "rel_fun (vimage2p f g R) R f g"
+ unfolding rel_fun_def vimage2p_def by auto
lemma predicate2D_vimage2p: "\<lbrakk>R \<le> vimage2p f g S; R x y\<rbrakk> \<Longrightarrow> S (f x) (g y)"
unfolding vimage2p_def by auto
-lemma id_transfer: "fun_rel A A id id"
- unfolding fun_rel_def by simp
+lemma id_transfer: "rel_fun A A id id"
+ unfolding rel_fun_def by simp
lemma ssubst_Pair_rhs: "\<lbrakk>(r, s) \<in> R; s' = s\<rbrakk> \<Longrightarrow> (r, s') \<in> R"
by (rule ssubst)
--- a/src/HOL/BNF_Util.thy Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/BNF_Util.thy Thu Mar 06 15:40:33 2014 +0100
@@ -13,19 +13,19 @@
begin
definition
- fun_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool"
+ rel_fun :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool"
where
- "fun_rel A B = (\<lambda>f g. \<forall>x y. A x y \<longrightarrow> B (f x) (g y))"
+ "rel_fun A B = (\<lambda>f g. \<forall>x y. A x y \<longrightarrow> B (f x) (g y))"
-lemma fun_relI [intro]:
+lemma rel_funI [intro]:
assumes "\<And>x y. A x y \<Longrightarrow> B (f x) (g y)"
- shows "fun_rel A B f g"
- using assms by (simp add: fun_rel_def)
+ shows "rel_fun A B f g"
+ using assms by (simp add: rel_fun_def)
-lemma fun_relD:
- assumes "fun_rel A B f g" and "A x y"
+lemma rel_funD:
+ assumes "rel_fun A B f g" and "A x y"
shows "B (f x) (g y)"
- using assms by (simp add: fun_rel_def)
+ using assms by (simp add: rel_fun_def)
definition collect where
"collect F x = (\<Union>f \<in> F. f x)"
--- a/src/HOL/Basic_BNFs.thy Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Basic_BNFs.thy Thu Mar 06 15:40:33 2014 +0100
@@ -163,7 +163,7 @@
map: "op \<circ>"
sets: range
bd: "natLeq +c |UNIV :: 'a set|"
- rel: "fun_rel op ="
+ rel: "rel_fun op ="
proof
fix f show "id \<circ> f = id f" by simp
next
@@ -193,13 +193,13 @@
finally show "|range f| \<le>o natLeq +c ?U" .
next
fix R S
- show "fun_rel op = R OO fun_rel op = S \<le> fun_rel op = (R OO S)" by (auto simp: fun_rel_def)
+ show "rel_fun op = R OO rel_fun op = S \<le> rel_fun op = (R OO S)" by (auto simp: rel_fun_def)
next
fix R
- show "fun_rel op = R =
+ show "rel_fun op = R =
(Grp {x. range x \<subseteq> Collect (split R)} (op \<circ> fst))\<inverse>\<inverse> OO
Grp {x. range x \<subseteq> Collect (split R)} (op \<circ> snd)"
- unfolding fun_rel_def Grp_def fun_eq_iff relcompp.simps conversep.simps subset_iff image_iff
+ unfolding rel_fun_def Grp_def fun_eq_iff relcompp.simps conversep.simps subset_iff image_iff
comp_apply mem_Collect_eq split_beta bex_UNIV
proof (safe, unfold fun_eq_iff[symmetric])
fix x xa a b c xb y aa ba
--- a/src/HOL/Code_Numeral.thy Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Code_Numeral.thy Thu Mar 06 15:40:33 2014 +0100
@@ -76,27 +76,27 @@
end
lemma [transfer_rule]:
- "fun_rel HOL.eq pcr_integer (of_nat :: nat \<Rightarrow> int) (of_nat :: nat \<Rightarrow> integer)"
+ "rel_fun HOL.eq pcr_integer (of_nat :: nat \<Rightarrow> int) (of_nat :: nat \<Rightarrow> integer)"
by (unfold of_nat_def [abs_def]) transfer_prover
lemma [transfer_rule]:
- "fun_rel HOL.eq pcr_integer (\<lambda>k :: int. k :: int) (of_int :: int \<Rightarrow> integer)"
+ "rel_fun HOL.eq pcr_integer (\<lambda>k :: int. k :: int) (of_int :: int \<Rightarrow> integer)"
proof -
- have "fun_rel HOL.eq pcr_integer (of_int :: int \<Rightarrow> int) (of_int :: int \<Rightarrow> integer)"
+ have "rel_fun HOL.eq pcr_integer (of_int :: int \<Rightarrow> int) (of_int :: int \<Rightarrow> integer)"
by (unfold of_int_of_nat [abs_def]) transfer_prover
then show ?thesis by (simp add: id_def)
qed
lemma [transfer_rule]:
- "fun_rel HOL.eq pcr_integer (numeral :: num \<Rightarrow> int) (numeral :: num \<Rightarrow> integer)"
+ "rel_fun HOL.eq pcr_integer (numeral :: num \<Rightarrow> int) (numeral :: num \<Rightarrow> integer)"
proof -
- have "fun_rel HOL.eq pcr_integer (numeral :: num \<Rightarrow> int) (\<lambda>n. of_int (numeral n))"
+ have "rel_fun HOL.eq pcr_integer (numeral :: num \<Rightarrow> int) (\<lambda>n. of_int (numeral n))"
by transfer_prover
then show ?thesis by simp
qed
lemma [transfer_rule]:
- "fun_rel HOL.eq (fun_rel HOL.eq pcr_integer) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> int) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> integer)"
+ "rel_fun HOL.eq (rel_fun HOL.eq pcr_integer) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> int) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> integer)"
by (unfold Num.sub_def [abs_def]) transfer_prover
lemma int_of_integer_of_nat [simp]:
@@ -192,11 +192,11 @@
end
lemma [transfer_rule]:
- "fun_rel pcr_integer (fun_rel pcr_integer pcr_integer) (min :: _ \<Rightarrow> _ \<Rightarrow> int) (min :: _ \<Rightarrow> _ \<Rightarrow> integer)"
+ "rel_fun pcr_integer (rel_fun pcr_integer pcr_integer) (min :: _ \<Rightarrow> _ \<Rightarrow> int) (min :: _ \<Rightarrow> _ \<Rightarrow> integer)"
by (unfold min_def [abs_def]) transfer_prover
lemma [transfer_rule]:
- "fun_rel pcr_integer (fun_rel pcr_integer pcr_integer) (max :: _ \<Rightarrow> _ \<Rightarrow> int) (max :: _ \<Rightarrow> _ \<Rightarrow> integer)"
+ "rel_fun pcr_integer (rel_fun pcr_integer pcr_integer) (max :: _ \<Rightarrow> _ \<Rightarrow> int) (max :: _ \<Rightarrow> _ \<Rightarrow> integer)"
by (unfold max_def [abs_def]) transfer_prover
lemma int_of_integer_min [simp]:
@@ -249,7 +249,7 @@
[simp, code_abbrev]: "Pos = numeral"
lemma [transfer_rule]:
- "fun_rel HOL.eq pcr_integer numeral Pos"
+ "rel_fun HOL.eq pcr_integer numeral Pos"
by simp transfer_prover
definition Neg :: "num \<Rightarrow> integer"
@@ -257,7 +257,7 @@
[simp, code_abbrev]: "Neg n = - Pos n"
lemma [transfer_rule]:
- "fun_rel HOL.eq pcr_integer (\<lambda>n. - numeral n) Neg"
+ "rel_fun HOL.eq pcr_integer (\<lambda>n. - numeral n) Neg"
by (simp add: Neg_def [abs_def]) transfer_prover
code_datatype "0::integer" Pos Neg
@@ -680,17 +680,17 @@
end
lemma [transfer_rule]:
- "fun_rel HOL.eq pcr_natural (\<lambda>n::nat. n) (of_nat :: nat \<Rightarrow> natural)"
+ "rel_fun HOL.eq pcr_natural (\<lambda>n::nat. n) (of_nat :: nat \<Rightarrow> natural)"
proof -
- have "fun_rel HOL.eq pcr_natural (of_nat :: nat \<Rightarrow> nat) (of_nat :: nat \<Rightarrow> natural)"
+ have "rel_fun HOL.eq pcr_natural (of_nat :: nat \<Rightarrow> nat) (of_nat :: nat \<Rightarrow> natural)"
by (unfold of_nat_def [abs_def]) transfer_prover
then show ?thesis by (simp add: id_def)
qed
lemma [transfer_rule]:
- "fun_rel HOL.eq pcr_natural (numeral :: num \<Rightarrow> nat) (numeral :: num \<Rightarrow> natural)"
+ "rel_fun HOL.eq pcr_natural (numeral :: num \<Rightarrow> nat) (numeral :: num \<Rightarrow> natural)"
proof -
- have "fun_rel HOL.eq pcr_natural (numeral :: num \<Rightarrow> nat) (\<lambda>n. of_nat (numeral n))"
+ have "rel_fun HOL.eq pcr_natural (numeral :: num \<Rightarrow> nat) (\<lambda>n. of_nat (numeral n))"
by transfer_prover
then show ?thesis by simp
qed
@@ -748,11 +748,11 @@
end
lemma [transfer_rule]:
- "fun_rel pcr_natural (fun_rel pcr_natural pcr_natural) (min :: _ \<Rightarrow> _ \<Rightarrow> nat) (min :: _ \<Rightarrow> _ \<Rightarrow> natural)"
+ "rel_fun pcr_natural (rel_fun pcr_natural pcr_natural) (min :: _ \<Rightarrow> _ \<Rightarrow> nat) (min :: _ \<Rightarrow> _ \<Rightarrow> natural)"
by (unfold min_def [abs_def]) transfer_prover
lemma [transfer_rule]:
- "fun_rel pcr_natural (fun_rel pcr_natural pcr_natural) (max :: _ \<Rightarrow> _ \<Rightarrow> nat) (max :: _ \<Rightarrow> _ \<Rightarrow> natural)"
+ "rel_fun pcr_natural (rel_fun pcr_natural pcr_natural) (max :: _ \<Rightarrow> _ \<Rightarrow> nat) (max :: _ \<Rightarrow> _ \<Rightarrow> natural)"
by (unfold max_def [abs_def]) transfer_prover
lemma nat_of_natural_min [simp]:
--- a/src/HOL/Int.thy Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Int.thy Thu Mar 06 15:40:33 2014 +0100
@@ -78,8 +78,8 @@
simp add: one_int.abs_eq plus_int.abs_eq)
lemma int_transfer [transfer_rule]:
- "(fun_rel (op =) cr_int) (\<lambda>n. (n, 0)) int"
- unfolding fun_rel_def cr_int_def int_def by simp
+ "(rel_fun (op =) cr_int) (\<lambda>n. (n, 0)) int"
+ unfolding rel_fun_def cr_int_def int_def by simp
lemma int_diff_cases:
obtains (diff) m n where "z = int m - int n"
--- a/src/HOL/Library/FSet.thy Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Library/FSet.thy Thu Mar 06 15:40:33 2014 +0100
@@ -878,99 +878,99 @@
lemma finsert_transfer [transfer_rule]:
"(A ===> rel_fset A ===> rel_fset A) finsert finsert"
- unfolding fun_rel_def rel_fset_alt_def by blast
+ unfolding rel_fun_def rel_fset_alt_def by blast
lemma funion_transfer [transfer_rule]:
"(rel_fset A ===> rel_fset A ===> rel_fset A) funion funion"
- unfolding fun_rel_def rel_fset_alt_def by blast
+ unfolding rel_fun_def rel_fset_alt_def by blast
lemma ffUnion_transfer [transfer_rule]:
"(rel_fset (rel_fset A) ===> rel_fset A) ffUnion ffUnion"
- unfolding fun_rel_def rel_fset_alt_def by transfer (simp, fast)
+ unfolding rel_fun_def rel_fset_alt_def by transfer (simp, fast)
lemma fimage_transfer [transfer_rule]:
"((A ===> B) ===> rel_fset A ===> rel_fset B) fimage fimage"
- unfolding fun_rel_def rel_fset_alt_def by simp blast
+ unfolding rel_fun_def rel_fset_alt_def by simp blast
lemma fBall_transfer [transfer_rule]:
"(rel_fset A ===> (A ===> op =) ===> op =) fBall fBall"
- unfolding rel_fset_alt_def fun_rel_def by blast
+ unfolding rel_fset_alt_def rel_fun_def by blast
lemma fBex_transfer [transfer_rule]:
"(rel_fset A ===> (A ===> op =) ===> op =) fBex fBex"
- unfolding rel_fset_alt_def fun_rel_def by blast
+ unfolding rel_fset_alt_def rel_fun_def by blast
(* FIXME transfer doesn't work here *)
lemma fPow_transfer [transfer_rule]:
"(rel_fset A ===> rel_fset (rel_fset A)) fPow fPow"
- unfolding fun_rel_def
- using Pow_transfer[unfolded fun_rel_def, rule_format, Transfer.transferred]
+ unfolding rel_fun_def
+ using Pow_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred]
by blast
lemma rel_fset_transfer [transfer_rule]:
"((A ===> B ===> op =) ===> rel_fset A ===> rel_fset B ===> op =)
rel_fset rel_fset"
- unfolding fun_rel_def
- using rel_set_transfer[unfolded fun_rel_def,rule_format, Transfer.transferred, where A = A and B = B]
+ unfolding rel_fun_def
+ using rel_set_transfer[unfolded rel_fun_def,rule_format, Transfer.transferred, where A = A and B = B]
by simp
lemma bind_transfer [transfer_rule]:
"(rel_fset A ===> (A ===> rel_fset B) ===> rel_fset B) fbind fbind"
- using assms unfolding fun_rel_def
- using bind_transfer[unfolded fun_rel_def, rule_format, Transfer.transferred] by blast
+ using assms unfolding rel_fun_def
+ using bind_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast
text {* Rules requiring bi-unique, bi-total or right-total relations *}
lemma fmember_transfer [transfer_rule]:
assumes "bi_unique A"
shows "(A ===> rel_fset A ===> op =) (op |\<in>|) (op |\<in>|)"
- using assms unfolding fun_rel_def rel_fset_alt_def bi_unique_def by metis
+ using assms unfolding rel_fun_def rel_fset_alt_def bi_unique_def by metis
lemma finter_transfer [transfer_rule]:
assumes "bi_unique A"
shows "(rel_fset A ===> rel_fset A ===> rel_fset A) finter finter"
- using assms unfolding fun_rel_def
- using inter_transfer[unfolded fun_rel_def, rule_format, Transfer.transferred] by blast
+ using assms unfolding rel_fun_def
+ using inter_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast
lemma fminus_transfer [transfer_rule]:
assumes "bi_unique A"
shows "(rel_fset A ===> rel_fset A ===> rel_fset A) (op |-|) (op |-|)"
- using assms unfolding fun_rel_def
- using Diff_transfer[unfolded fun_rel_def, rule_format, Transfer.transferred] by blast
+ using assms unfolding rel_fun_def
+ using Diff_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast
lemma fsubset_transfer [transfer_rule]:
assumes "bi_unique A"
shows "(rel_fset A ===> rel_fset A ===> op =) (op |\<subseteq>|) (op |\<subseteq>|)"
- using assms unfolding fun_rel_def
- using subset_transfer[unfolded fun_rel_def, rule_format, Transfer.transferred] by blast
+ using assms unfolding rel_fun_def
+ using subset_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast
lemma fSup_transfer [transfer_rule]:
"bi_unique A \<Longrightarrow> (rel_set (rel_fset A) ===> rel_fset A) Sup Sup"
- using assms unfolding fun_rel_def
+ using assms unfolding rel_fun_def
apply clarify
apply transfer'
- using Sup_fset_transfer[unfolded fun_rel_def] by blast
+ using Sup_fset_transfer[unfolded rel_fun_def] by blast
(* FIXME: add right_total_fInf_transfer *)
lemma fInf_transfer [transfer_rule]:
assumes "bi_unique A" and "bi_total A"
shows "(rel_set (rel_fset A) ===> rel_fset A) Inf Inf"
- using assms unfolding fun_rel_def
+ using assms unfolding rel_fun_def
apply clarify
apply transfer'
- using Inf_fset_transfer[unfolded fun_rel_def] by blast
+ using Inf_fset_transfer[unfolded rel_fun_def] by blast
lemma ffilter_transfer [transfer_rule]:
assumes "bi_unique A"
shows "((A ===> op=) ===> rel_fset A ===> rel_fset A) ffilter ffilter"
- using assms unfolding fun_rel_def
- using Lifting_Set.filter_transfer[unfolded fun_rel_def, rule_format, Transfer.transferred] by blast
+ using assms unfolding rel_fun_def
+ using Lifting_Set.filter_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast
lemma card_transfer [transfer_rule]:
"bi_unique A \<Longrightarrow> (rel_fset A ===> op =) fcard fcard"
- using assms unfolding fun_rel_def
- using card_transfer[unfolded fun_rel_def, rule_format, Transfer.transferred] by blast
+ using assms unfolding rel_fun_def
+ using card_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast
end
--- a/src/HOL/Library/Float.thy Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Library/Float.thy Thu Mar 06 15:40:33 2014 +0100
@@ -223,15 +223,15 @@
done
lemma transfer_numeral [transfer_rule]:
- "fun_rel (op =) pcr_float (numeral :: _ \<Rightarrow> real) (numeral :: _ \<Rightarrow> float)"
- unfolding fun_rel_def float.pcr_cr_eq cr_float_def by simp
+ "rel_fun (op =) pcr_float (numeral :: _ \<Rightarrow> real) (numeral :: _ \<Rightarrow> float)"
+ unfolding rel_fun_def float.pcr_cr_eq cr_float_def by simp
lemma float_neg_numeral[simp]: "real (- numeral x :: float) = - numeral x"
by simp
lemma transfer_neg_numeral [transfer_rule]:
- "fun_rel (op =) pcr_float (- numeral :: _ \<Rightarrow> real) (- numeral :: _ \<Rightarrow> float)"
- unfolding fun_rel_def float.pcr_cr_eq cr_float_def by simp
+ "rel_fun (op =) pcr_float (- numeral :: _ \<Rightarrow> real) (- numeral :: _ \<Rightarrow> float)"
+ unfolding rel_fun_def float.pcr_cr_eq cr_float_def by simp
lemma
shows float_of_numeral[simp]: "numeral k = float_of (numeral k)"
--- a/src/HOL/Library/Mapping.thy Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Library/Mapping.thy Thu Mar 06 15:40:33 2014 +0100
@@ -33,7 +33,7 @@
definition equal_None :: "'a option \<Rightarrow> bool" where "equal_None x \<equiv> x = None"
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)
+unfolding rel_fun_def rel_option_iff equal_None_def by (auto split: option.split)
lemma dom_transfer:
assumes [transfer_rule]: "bi_total A"
@@ -55,7 +55,7 @@
lemma bulkload_transfer:
"(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
+unfolding rel_fun_def
apply clarsimp
apply (erule list_all2_induct)
apply simp
--- a/src/HOL/Library/Multiset.thy Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Library/Multiset.thy Thu Mar 06 15:40:33 2014 +0100
@@ -2289,7 +2289,7 @@
interpretation lifting_syntax .
lemma set_of_transfer[transfer_rule]: "(pcr_multiset op = ===> op =) (\<lambda>f. {a. 0 < f a}) set_of"
- unfolding set_of_def pcr_multiset_def cr_multiset_def fun_rel_def by auto
+ unfolding set_of_def pcr_multiset_def cr_multiset_def rel_fun_def by auto
end
--- a/src/HOL/Library/Quotient_Set.thy Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Library/Quotient_Set.thy Thu Mar 06 15:40:33 2014 +0100
@@ -50,7 +50,7 @@
lemma collect_rsp[quot_respect]:
assumes "Quotient3 R Abs Rep"
shows "((R ===> op =) ===> rel_vset R) Collect Collect"
- by (intro fun_relI) (simp add: fun_rel_def rel_vset_def)
+ by (intro rel_funI) (simp add: rel_fun_def rel_vset_def)
lemma collect_prs[quot_preserve]:
assumes "Quotient3 R Abs Rep"
@@ -61,7 +61,7 @@
lemma union_rsp[quot_respect]:
assumes "Quotient3 R Abs Rep"
shows "(rel_vset R ===> rel_vset R ===> rel_vset R) op \<union> op \<union>"
- by (intro fun_relI) (simp add: rel_vset_def)
+ by (intro rel_funI) (simp add: rel_vset_def)
lemma union_prs[quot_preserve]:
assumes "Quotient3 R Abs Rep"
@@ -72,7 +72,7 @@
lemma diff_rsp[quot_respect]:
assumes "Quotient3 R Abs Rep"
shows "(rel_vset R ===> rel_vset R ===> rel_vset R) op - op -"
- by (intro fun_relI) (simp add: rel_vset_def)
+ by (intro rel_funI) (simp add: rel_vset_def)
lemma diff_prs[quot_preserve]:
assumes "Quotient3 R Abs Rep"
@@ -83,7 +83,7 @@
lemma inter_rsp[quot_respect]:
assumes "Quotient3 R Abs Rep"
shows "(rel_vset R ===> rel_vset R ===> rel_vset R) op \<inter> op \<inter>"
- by (intro fun_relI) (auto simp add: rel_vset_def)
+ by (intro rel_funI) (auto simp add: rel_vset_def)
lemma inter_prs[quot_preserve]:
assumes "Quotient3 R Abs Rep"
@@ -98,6 +98,6 @@
lemma mem_rsp[quot_respect]:
shows "(R ===> rel_vset R ===> op =) op \<in> op \<in>"
- by (intro fun_relI) (simp add: rel_vset_def)
+ by (intro rel_funI) (simp add: rel_vset_def)
end
--- a/src/HOL/Library/Quotient_Syntax.thy Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Library/Quotient_Syntax.thy Thu Mar 06 15:40:33 2014 +0100
@@ -11,6 +11,6 @@
notation
rel_conj (infixr "OOO" 75) and
map_fun (infixr "--->" 55) and
- fun_rel (infixr "===>" 55)
+ rel_fun (infixr "===>" 55)
end
--- a/src/HOL/Lifting.thy Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Lifting.thy Thu Mar 06 15:40:33 2014 +0100
@@ -52,7 +52,7 @@
assumes [transfer_rule]: "right_total B"
assumes [transfer_rule]: "bi_unique A"
shows "((A ===> B ===> op=) ===> implies) left_unique left_unique"
-using assms unfolding left_unique_def[abs_def] right_total_def bi_unique_def fun_rel_def
+using assms unfolding left_unique_def[abs_def] right_total_def bi_unique_def rel_fun_def
by metis
lemma bi_unique_iff: "bi_unique A = (right_unique A \<and> left_unique A)"
@@ -69,7 +69,7 @@
lemma left_total_fun:
"\<lbrakk>left_unique A; left_total B\<rbrakk> \<Longrightarrow> left_total (A ===> B)"
- unfolding left_total_def fun_rel_def
+ unfolding left_total_def rel_fun_def
apply (rule allI, rename_tac f)
apply (rule_tac x="\<lambda>y. SOME z. B (f (THE x. A x y)) z" in exI)
apply clarify
@@ -83,7 +83,7 @@
lemma left_unique_fun:
"\<lbrakk>left_total A; left_unique B\<rbrakk> \<Longrightarrow> left_unique (A ===> B)"
- unfolding left_total_def left_unique_def fun_rel_def
+ unfolding left_total_def left_unique_def rel_fun_def
by (clarify, rule ext, fast)
lemma left_total_eq: "left_total op=" unfolding left_total_def by blast
@@ -242,7 +242,7 @@
assumes 2: "Quotient R2 abs2 rep2 T2"
shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2) (T1 ===> T2)"
using assms unfolding Quotient_alt_def2
- unfolding fun_rel_def fun_eq_iff map_fun_apply
+ unfolding rel_fun_def fun_eq_iff map_fun_apply
by (safe, metis+)
lemma apply_rsp:
@@ -250,12 +250,12 @@
assumes q: "Quotient R1 Abs1 Rep1 T1"
and a: "(R1 ===> R2) f g" "R1 x y"
shows "R2 (f x) (g y)"
- using a by (auto elim: fun_relE)
+ using a by (auto elim: rel_funE)
lemma apply_rsp':
assumes a: "(R1 ===> R2) f g" "R1 x y"
shows "R2 (f x) (g y)"
- using a by (auto elim: fun_relE)
+ using a by (auto elim: rel_funE)
lemma apply_rsp'':
assumes "Quotient R Abs Rep T"
@@ -296,12 +296,12 @@
shows "x = y"
using assms by (simp add: invariant_def)
-lemma fun_rel_eq_invariant: "(op= ===> Lifting.invariant P) = Lifting.invariant (\<lambda>f. \<forall>x. P(f x))"
-unfolding invariant_def fun_rel_def by auto
+lemma rel_fun_eq_invariant: "(op= ===> Lifting.invariant P) = Lifting.invariant (\<lambda>f. \<forall>x. P(f x))"
+unfolding invariant_def rel_fun_def by auto
-lemma fun_rel_invariant_rel:
+lemma rel_fun_invariant_rel:
shows "((invariant R) ===> S) = (\<lambda>f g. \<forall>x. R x \<longrightarrow> S (f x) (g x))"
-by (auto simp add: invariant_def fun_rel_def)
+by (auto simp add: invariant_def rel_fun_def)
lemma invariant_same_args:
shows "invariant P x x \<equiv> P x"
@@ -376,7 +376,7 @@
using 1 unfolding Quotient_alt_def right_total_def by metis
lemma Quotient_rel_eq_transfer: "(T ===> T ===> op =) R (op =)"
- using 1 unfolding Quotient_alt_def fun_rel_def by simp
+ using 1 unfolding Quotient_alt_def rel_fun_def by simp
lemma Quotient_abs_induct:
assumes "\<And>y. R y y \<Longrightarrow> P (Abs y)" shows "P x"
@@ -395,7 +395,7 @@
using 1 2 unfolding Quotient_alt_def bi_total_def reflp_def by auto
lemma Quotient_id_abs_transfer: "(op = ===> T) (\<lambda>x. x) Abs"
- using 1 2 unfolding Quotient_alt_def reflp_def fun_rel_def by simp
+ using 1 2 unfolding Quotient_alt_def reflp_def rel_fun_def by simp
lemma Quotient_total_abs_induct: "(\<And>y. P (Abs y)) \<Longrightarrow> P x"
using 1 2 assms unfolding Quotient_alt_def reflp_def by metis
@@ -432,7 +432,7 @@
by blast
lemma typedef_rep_transfer: "(T ===> op =) (\<lambda>x. x) Rep"
- unfolding fun_rel_def T_def by simp
+ unfolding rel_fun_def T_def by simp
end
@@ -557,10 +557,10 @@
assumes "A \<ge> C"
assumes "B \<le> D"
shows "(A ===> B) \<le> (C ===> D)"
-using assms unfolding fun_rel_def by blast
+using assms unfolding rel_fun_def by blast
lemma pos_fun_distr: "((R ===> S) OO (R' ===> S')) \<le> ((R OO R') ===> (S OO S'))"
-unfolding OO_def fun_rel_def by blast
+unfolding OO_def rel_fun_def by blast
lemma functional_relation: "right_unique R \<Longrightarrow> left_total R \<Longrightarrow> \<forall>x. \<exists>!y. R x y"
unfolding right_unique_def left_total_def by blast
@@ -573,7 +573,7 @@
assumes 2: "right_unique R'" "left_total R'"
shows "(R OO R' ===> S OO S') \<le> ((R ===> S) OO (R' ===> S')) "
using functional_relation[OF 2] functional_converse_relation[OF 1]
- unfolding fun_rel_def OO_def
+ unfolding rel_fun_def OO_def
apply clarify
apply (subst all_comm)
apply (subst all_conj_distrib[symmetric])
@@ -585,7 +585,7 @@
assumes 2: "left_unique S'" "right_total S'"
shows "(R OO R' ===> S OO S') \<le> ((R ===> S) OO (R' ===> S'))"
using functional_converse_relation[OF 2] functional_relation[OF 1]
- unfolding fun_rel_def OO_def
+ unfolding rel_fun_def OO_def
apply clarify
apply (subst all_comm)
apply (subst all_conj_distrib[symmetric])
@@ -599,7 +599,7 @@
assumes "(R ===> op=) P P'"
assumes "Domainp R = P''"
shows "(R OO Lifting.invariant P' OO R\<inverse>\<inverse>) = Lifting.invariant (inf P'' P)"
-using assms unfolding OO_def conversep_iff Domainp_iff[abs_def] left_unique_def fun_rel_def invariant_def
+using assms unfolding OO_def conversep_iff Domainp_iff[abs_def] left_unique_def rel_fun_def invariant_def
fun_eq_iff by blast
lemma composed_equiv_rel_eq_invariant:
@@ -615,7 +615,7 @@
assumes "(A ===> op=) P' P"
shows "Domainp (A OO B) = P'"
using assms
-unfolding Domainp_iff[abs_def] OO_def bi_unique_def left_total_def fun_rel_def
+unfolding Domainp_iff[abs_def] OO_def bi_unique_def left_total_def rel_fun_def
by (fast intro: fun_eq_iff)
lemma pcr_Domainp_par:
@@ -623,7 +623,7 @@
assumes "Domainp A = P1"
assumes "(A ===> op=) P2' P2"
shows "Domainp (A OO B) = (inf P1 P2')"
-using assms unfolding fun_rel_def Domainp_iff[abs_def] OO_def
+using assms unfolding rel_fun_def Domainp_iff[abs_def] OO_def
by (fast intro: fun_eq_iff)
definition rel_pred_comp :: "('a => 'b => bool) => ('b => bool) => 'a => bool"
--- a/src/HOL/Lifting_Option.thy Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Lifting_Option.thy Thu Mar 06 15:40:33 2014 +0100
@@ -86,11 +86,11 @@
by (rule option.rel_inject)
lemma Some_transfer [transfer_rule]: "(A ===> rel_option A) Some Some"
- unfolding fun_rel_def by simp
+ unfolding rel_fun_def by simp
lemma case_option_transfer [transfer_rule]:
"(B ===> (A ===> B) ===> rel_option A ===> B) case_option case_option"
- unfolding fun_rel_def split_option_all by simp
+ unfolding rel_fun_def split_option_all by simp
lemma map_option_transfer [transfer_rule]:
"((A ===> B) ===> rel_option A ===> rel_option B) map_option map_option"
@@ -99,7 +99,7 @@
lemma option_bind_transfer [transfer_rule]:
"(rel_option A ===> (A ===> rel_option B) ===> rel_option B)
Option.bind Option.bind"
- unfolding fun_rel_def split_option_all by simp
+ unfolding rel_fun_def split_option_all by simp
end
--- a/src/HOL/Lifting_Product.thy Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Lifting_Product.thy Thu Mar 06 15:40:33 2014 +0100
@@ -80,17 +80,17 @@
interpretation lifting_syntax .
lemma Pair_transfer [transfer_rule]: "(A ===> B ===> rel_prod A B) Pair Pair"
- unfolding fun_rel_def rel_prod_def by simp
+ unfolding rel_fun_def rel_prod_def by simp
lemma fst_transfer [transfer_rule]: "(rel_prod A B ===> A) fst fst"
- unfolding fun_rel_def rel_prod_def by simp
+ unfolding rel_fun_def rel_prod_def by simp
lemma snd_transfer [transfer_rule]: "(rel_prod A B ===> B) snd snd"
- unfolding fun_rel_def rel_prod_def by simp
+ unfolding rel_fun_def rel_prod_def by simp
lemma case_prod_transfer [transfer_rule]:
"((A ===> B ===> C) ===> rel_prod A B ===> C) case_prod case_prod"
- unfolding fun_rel_def rel_prod_def by simp
+ unfolding rel_fun_def rel_prod_def by simp
lemma curry_transfer [transfer_rule]:
"((rel_prod A B ===> C) ===> A ===> B ===> C) curry curry"
@@ -104,7 +104,7 @@
lemma rel_prod_transfer [transfer_rule]:
"((A ===> B ===> op =) ===> (C ===> D ===> op =) ===>
rel_prod A C ===> rel_prod B D ===> op =) rel_prod rel_prod"
- unfolding fun_rel_def by auto
+ unfolding rel_fun_def by auto
end
--- a/src/HOL/Lifting_Set.thy Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Lifting_Set.thy Thu Mar 06 15:40:33 2014 +0100
@@ -109,19 +109,19 @@
lemma insert_transfer [transfer_rule]:
"(A ===> rel_set A ===> rel_set A) insert insert"
- unfolding fun_rel_def rel_set_def by auto
+ unfolding rel_fun_def rel_set_def by auto
lemma union_transfer [transfer_rule]:
"(rel_set A ===> rel_set A ===> rel_set A) union union"
- unfolding fun_rel_def rel_set_def by auto
+ unfolding rel_fun_def rel_set_def by auto
lemma Union_transfer [transfer_rule]:
"(rel_set (rel_set A) ===> rel_set A) Union Union"
- unfolding fun_rel_def rel_set_def by simp fast
+ unfolding rel_fun_def rel_set_def by simp fast
lemma image_transfer [transfer_rule]:
"((A ===> B) ===> rel_set A ===> rel_set B) image image"
- unfolding fun_rel_def rel_set_def by simp fast
+ unfolding rel_fun_def rel_set_def by simp fast
lemma UNION_transfer [transfer_rule]:
"(rel_set A ===> (A ===> rel_set B) ===> rel_set B) UNION UNION"
@@ -129,15 +129,15 @@
lemma Ball_transfer [transfer_rule]:
"(rel_set A ===> (A ===> op =) ===> op =) Ball Ball"
- unfolding rel_set_def fun_rel_def by fast
+ unfolding rel_set_def rel_fun_def by fast
lemma Bex_transfer [transfer_rule]:
"(rel_set A ===> (A ===> op =) ===> op =) Bex Bex"
- unfolding rel_set_def fun_rel_def by fast
+ unfolding rel_set_def rel_fun_def by fast
lemma Pow_transfer [transfer_rule]:
"(rel_set A ===> rel_set (rel_set A)) Pow Pow"
- apply (rule fun_relI, rename_tac X Y, rule rel_setI)
+ apply (rule rel_funI, rename_tac X Y, rule rel_setI)
apply (rename_tac X', rule_tac x="{y\<in>Y. \<exists>x\<in>X'. A x y}" in rev_bexI, clarsimp)
apply (simp add: rel_set_def, fast)
apply (rename_tac Y', rule_tac x="{x\<in>X. \<exists>y\<in>Y'. A x y}" in rev_bexI, clarsimp)
@@ -147,16 +147,16 @@
lemma rel_set_transfer [transfer_rule]:
"((A ===> B ===> op =) ===> rel_set A ===> rel_set B ===> op =)
rel_set rel_set"
- unfolding fun_rel_def rel_set_def by fast
+ unfolding rel_fun_def rel_set_def by fast
lemma SUPR_parametric [transfer_rule]:
"(rel_set R ===> (R ===> op =) ===> op =) SUPR (SUPR :: _ \<Rightarrow> _ \<Rightarrow> _::complete_lattice)"
-proof(rule fun_relI)+
+proof(rule rel_funI)+
fix A B f and g :: "'b \<Rightarrow> 'c"
assume AB: "rel_set R A B"
and fg: "(R ===> op =) f g"
show "SUPR A f = SUPR B g"
- by(rule SUPR_eq)(auto 4 4 dest: rel_setD1[OF AB] rel_setD2[OF AB] fun_relD[OF fg] intro: rev_bexI)
+ by(rule SUPR_eq)(auto 4 4 dest: rel_setD1[OF AB] rel_setD2[OF AB] rel_funD[OF fg] intro: rev_bexI)
qed
lemma bind_transfer [transfer_rule]:
@@ -168,27 +168,27 @@
lemma member_transfer [transfer_rule]:
assumes "bi_unique A"
shows "(A ===> rel_set A ===> op =) (op \<in>) (op \<in>)"
- using assms unfolding fun_rel_def rel_set_def bi_unique_def by fast
+ using assms unfolding rel_fun_def rel_set_def bi_unique_def by fast
lemma right_total_Collect_transfer[transfer_rule]:
assumes "right_total A"
shows "((A ===> op =) ===> rel_set A) (\<lambda>P. Collect (\<lambda>x. P x \<and> Domainp A x)) Collect"
- using assms unfolding right_total_def rel_set_def fun_rel_def Domainp_iff by fast
+ using assms unfolding right_total_def rel_set_def rel_fun_def Domainp_iff by fast
lemma Collect_transfer [transfer_rule]:
assumes "bi_total A"
shows "((A ===> op =) ===> rel_set A) Collect Collect"
- using assms unfolding fun_rel_def rel_set_def bi_total_def by fast
+ using assms unfolding rel_fun_def rel_set_def bi_total_def by fast
lemma inter_transfer [transfer_rule]:
assumes "bi_unique A"
shows "(rel_set A ===> rel_set A ===> rel_set A) inter inter"
- using assms unfolding fun_rel_def rel_set_def bi_unique_def by fast
+ using assms unfolding rel_fun_def rel_set_def bi_unique_def by fast
lemma Diff_transfer [transfer_rule]:
assumes "bi_unique A"
shows "(rel_set A ===> rel_set A ===> rel_set A) (op -) (op -)"
- using assms unfolding fun_rel_def rel_set_def bi_unique_def
+ using assms unfolding rel_fun_def rel_set_def bi_unique_def
unfolding Ball_def Bex_def Diff_eq
by (safe, simp, metis, simp, metis)
@@ -232,7 +232,7 @@
lemma filter_transfer [transfer_rule]:
assumes [transfer_rule]: "bi_unique A"
shows "((A ===> op=) ===> rel_set A ===> rel_set A) Set.filter Set.filter"
- unfolding Set.filter_def[abs_def] fun_rel_def rel_set_def by blast
+ unfolding Set.filter_def[abs_def] rel_fun_def rel_set_def by blast
lemma bi_unique_rel_set_lemma:
assumes "bi_unique R" and "rel_set R X Y"
@@ -270,12 +270,12 @@
lemma finite_transfer [transfer_rule]:
"bi_unique A \<Longrightarrow> (rel_set A ===> op =) finite finite"
- by (rule fun_relI, erule (1) bi_unique_rel_set_lemma,
+ by (rule rel_funI, erule (1) bi_unique_rel_set_lemma,
auto dest: finite_imageD)
lemma card_transfer [transfer_rule]:
"bi_unique A \<Longrightarrow> (rel_set A ===> op =) card card"
- by (rule fun_relI, erule (1) bi_unique_rel_set_lemma, simp add: card_image)
+ by (rule rel_funI, erule (1) bi_unique_rel_set_lemma, simp add: card_image)
lemma vimage_parametric [transfer_rule]:
assumes [transfer_rule]: "bi_total A" "bi_unique B"
@@ -285,7 +285,7 @@
lemma setsum_parametric [transfer_rule]:
assumes "bi_unique A"
shows "((A ===> op =) ===> rel_set A ===> op =) setsum setsum"
-proof(rule fun_relI)+
+proof(rule rel_funI)+
fix f :: "'a \<Rightarrow> 'c" and g S T
assume fg: "(A ===> op =) f g"
and ST: "rel_set A S T"
@@ -313,7 +313,7 @@
assume "t \<in> T"
with ST obtain s where "A s t" "s \<in> S" by(auto dest: rel_setD2)
hence "?f t = s" by(auto dest: bi_uniqueDl[OF assms])
- moreover from fg `A s t` have "f s = g t" by(rule fun_relD)
+ moreover from fg `A s t` have "f s = g t" by(rule rel_funD)
ultimately show "g t = f (?f t)" by simp
qed
qed
--- a/src/HOL/Lifting_Sum.thy Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Lifting_Sum.thy Thu Mar 06 15:40:33 2014 +0100
@@ -70,14 +70,14 @@
interpretation lifting_syntax .
lemma Inl_transfer [transfer_rule]: "(A ===> rel_sum A B) Inl Inl"
- unfolding fun_rel_def by simp
+ unfolding rel_fun_def by simp
lemma Inr_transfer [transfer_rule]: "(B ===> rel_sum A B) Inr Inr"
- unfolding fun_rel_def by simp
+ unfolding rel_fun_def by simp
lemma case_sum_transfer [transfer_rule]:
"((A ===> C) ===> (B ===> C) ===> rel_sum A B ===> C) case_sum case_sum"
- unfolding fun_rel_def rel_sum_def by (simp split: sum.split)
+ unfolding rel_fun_def rel_sum_def by (simp split: sum.split)
end
--- a/src/HOL/List.thy Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/List.thy Thu Mar 06 15:40:33 2014 +0100
@@ -6713,17 +6713,17 @@
lemma Cons_transfer [transfer_rule]:
"(A ===> list_all2 A ===> list_all2 A) Cons Cons"
- unfolding fun_rel_def by simp
+ unfolding rel_fun_def by simp
lemma case_list_transfer [transfer_rule]:
"(B ===> (A ===> list_all2 A ===> B) ===> list_all2 A ===> B)
case_list case_list"
- unfolding fun_rel_def by (simp split: list.split)
+ unfolding rel_fun_def by (simp split: list.split)
lemma rec_list_transfer [transfer_rule]:
"(B ===> (A ===> list_all2 A ===> B ===> B) ===> list_all2 A ===> B)
rec_list rec_list"
- unfolding fun_rel_def by (clarify, erule list_all2_induct, simp_all)
+ unfolding rel_fun_def by (clarify, erule list_all2_induct, simp_all)
lemma tl_transfer [transfer_rule]:
"(list_all2 A ===> list_all2 A) tl tl"
@@ -6731,7 +6731,7 @@
lemma butlast_transfer [transfer_rule]:
"(list_all2 A ===> list_all2 A) butlast butlast"
- by (rule fun_relI, erule list_all2_induct, auto)
+ by (rule rel_funI, erule list_all2_induct, auto)
lemma set_transfer [transfer_rule]:
"(list_all2 A ===> rel_set A) set set"
@@ -6836,7 +6836,7 @@
lemma remdups_adj_transfer [transfer_rule]:
assumes [transfer_rule]: "bi_unique A"
shows "(list_all2 A ===> list_all2 A) remdups_adj remdups_adj"
- proof (rule fun_relI, erule list_all2_induct)
+ proof (rule rel_funI, erule list_all2_induct)
qed (auto simp: remdups_adj_Cons assms[unfolded bi_unique_def] split: list.splits)
lemma replicate_transfer [transfer_rule]:
@@ -6874,7 +6874,7 @@
lemma lists_transfer [transfer_rule]:
"(rel_set A ===> rel_set (list_all2 A)) lists lists"
- apply (rule fun_relI, rule rel_setI)
+ apply (rule rel_funI, rule rel_setI)
apply (erule lists.induct, simp)
apply (simp only: rel_set_def list_all2_Cons1, metis lists.Cons)
apply (erule lists.induct, simp)
@@ -6884,7 +6884,7 @@
lemma set_Cons_transfer [transfer_rule]:
"(rel_set A ===> rel_set (list_all2 A) ===> rel_set (list_all2 A))
set_Cons set_Cons"
- unfolding fun_rel_def rel_set_def set_Cons_def
+ unfolding rel_fun_def rel_set_def set_Cons_def
apply safe
apply (simp add: list_all2_Cons1, fast)
apply (simp add: list_all2_Cons2, fast)
@@ -6896,7 +6896,7 @@
lemma null_transfer [transfer_rule]:
"(list_all2 A ===> op =) List.null List.null"
- unfolding fun_rel_def List.null_def by auto
+ unfolding rel_fun_def List.null_def by auto
lemma list_all_transfer [transfer_rule]:
"((A ===> op =) ===> list_all2 A ===> op =) list_all list_all"
@@ -6908,9 +6908,9 @@
lemma splice_transfer [transfer_rule]:
"(list_all2 A ===> list_all2 A ===> list_all2 A) splice splice"
- apply (rule fun_relI, erule list_all2_induct, simp add: fun_rel_def, simp)
- apply (rule fun_relI)
- apply (erule_tac xs=x in list_all2_induct, simp, simp add: fun_rel_def)
+ apply (rule rel_funI, erule list_all2_induct, simp add: rel_fun_def, simp)
+ apply (rule rel_funI)
+ apply (erule_tac xs=x in list_all2_induct, simp, simp add: rel_fun_def)
done
lemma listsum_transfer[transfer_rule]:
--- a/src/HOL/Quotient.thy Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Quotient.thy Thu Mar 06 15:40:33 2014 +0100
@@ -146,7 +146,7 @@
using q1 q2 by (simp add: Quotient3_def fun_eq_iff)
moreover
have "\<And>a.(R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)"
- by (rule fun_relI)
+ by (rule rel_funI)
(insert q1 q2 Quotient3_rel_abs [of R1 abs1 rep1] Quotient3_rel_rep [of R2 abs2 rep2],
simp (no_asm) add: Quotient3_def, simp)
@@ -157,17 +157,17 @@
(rep1 ---> abs2) r = (rep1 ---> abs2) s)"
proof -
- have "(R1 ===> R2) r s \<Longrightarrow> (R1 ===> R2) r r" unfolding fun_rel_def
+ have "(R1 ===> R2) r s \<Longrightarrow> (R1 ===> R2) r r" unfolding rel_fun_def
using Quotient3_part_equivp[OF q1] Quotient3_part_equivp[OF q2]
by (metis (full_types) part_equivp_def)
- moreover have "(R1 ===> R2) r s \<Longrightarrow> (R1 ===> R2) s s" unfolding fun_rel_def
+ moreover have "(R1 ===> R2) r s \<Longrightarrow> (R1 ===> R2) s s" unfolding rel_fun_def
using Quotient3_part_equivp[OF q1] Quotient3_part_equivp[OF q2]
by (metis (full_types) part_equivp_def)
moreover have "(R1 ===> R2) r s \<Longrightarrow> (rep1 ---> abs2) r = (rep1 ---> abs2) s"
- apply(auto simp add: fun_rel_def fun_eq_iff) using q1 q2 unfolding Quotient3_def by metis
+ apply(auto simp add: rel_fun_def fun_eq_iff) using q1 q2 unfolding Quotient3_def by metis
moreover have "((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and>
(rep1 ---> abs2) r = (rep1 ---> abs2) s) \<Longrightarrow> (R1 ===> R2) r s"
- apply(auto simp add: fun_rel_def fun_eq_iff) using q1 q2 unfolding Quotient3_def
+ apply(auto simp add: rel_fun_def fun_eq_iff) using q1 q2 unfolding Quotient3_def
by (metis map_fun_apply)
ultimately show ?thesis by blast
@@ -204,7 +204,7 @@
assumes q: "Quotient3 R1 Abs1 Rep1"
and a: "(R1 ===> R2) f g" "R1 x y"
shows "R2 (f x) (g y)"
- using a by (auto elim: fun_relE)
+ using a by (auto elim: rel_funE)
lemma apply_rspQ3'':
assumes "Quotient3 R Abs Rep"
@@ -261,7 +261,7 @@
apply(rule iffI)
apply(rule allI)
apply(drule_tac x="\<lambda>y. f x" in bspec)
- apply(simp add: in_respects fun_rel_def)
+ apply(simp add: in_respects rel_fun_def)
apply(rule impI)
using a equivp_reflp_symp_transp[of "R2"]
apply (auto elim: equivpE reflpE)
@@ -273,7 +273,7 @@
apply(auto)
apply(rule_tac x="\<lambda>y. f x" in bexI)
apply(simp)
- apply(simp add: Respects_def in_respects fun_rel_def)
+ apply(simp add: Respects_def in_respects rel_fun_def)
apply(rule impI)
using a equivp_reflp_symp_transp[of "R2"]
apply (auto elim: equivpE reflpE)
@@ -326,10 +326,10 @@
assumes q: "Quotient3 R1 Abs1 Rep1"
and a: "(R1 ===> R2) f g"
shows "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)"
- apply (auto simp add: Babs_def in_respects fun_rel_def)
+ apply (auto simp add: Babs_def in_respects rel_fun_def)
apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1")
- using a apply (simp add: Babs_def fun_rel_def)
- apply (simp add: in_respects fun_rel_def)
+ using a apply (simp add: Babs_def rel_fun_def)
+ apply (simp add: in_respects rel_fun_def)
using Quotient3_rel[OF q]
by metis
@@ -349,7 +349,7 @@
shows "((R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)) = ((R1 ===> R2) f g)"
apply(rule iffI)
apply(simp_all only: babs_rsp[OF q])
- apply(auto simp add: Babs_def fun_rel_def)
+ apply(auto simp add: Babs_def rel_fun_def)
apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1")
apply(metis Babs_def)
apply (simp add: in_respects)
@@ -367,17 +367,17 @@
lemma ball_rsp:
assumes a: "(R ===> (op =)) f g"
shows "Ball (Respects R) f = Ball (Respects R) g"
- using a by (auto simp add: Ball_def in_respects elim: fun_relE)
+ using a by (auto simp add: Ball_def in_respects elim: rel_funE)
lemma bex_rsp:
assumes a: "(R ===> (op =)) f g"
shows "(Bex (Respects R) f = Bex (Respects R) g)"
- using a by (auto simp add: Bex_def in_respects elim: fun_relE)
+ using a by (auto simp add: Bex_def in_respects elim: rel_funE)
lemma bex1_rsp:
assumes a: "(R ===> (op =)) f g"
shows "Ex1 (\<lambda>x. x \<in> Respects R \<and> f x) = Ex1 (\<lambda>x. x \<in> Respects R \<and> g x)"
- using a by (auto elim: fun_relE simp add: Ex1_def in_respects)
+ using a by (auto elim: rel_funE simp add: Ex1_def in_respects)
(* 2 lemmas needed for cleaning of quantifiers *)
lemma all_prs:
@@ -440,7 +440,7 @@
lemma bex1_rel_rsp:
assumes a: "Quotient3 R absf repf"
shows "((R ===> op =) ===> op =) (Bex1_rel R) (Bex1_rel R)"
- apply (simp add: fun_rel_def)
+ apply (simp add: rel_fun_def)
apply clarify
apply rule
apply (simp_all add: bex1_rel_aux bex1_rel_aux2)
@@ -519,7 +519,7 @@
lemma quot_rel_rsp:
assumes a: "Quotient3 R Abs Rep"
shows "(R ===> R ===> op =) R R"
- apply(rule fun_relI)+
+ apply(rule rel_funI)+
apply(rule equals_rsp[OF a])
apply(assumption)+
done
@@ -536,7 +536,7 @@
lemma o_rsp:
"((R2 ===> R3) ===> (R1 ===> R2) ===> (R1 ===> R3)) op \<circ> op \<circ>"
"(op = ===> (R1 ===> op =) ===> R1 ===> op =) op \<circ> op \<circ>"
- by (force elim: fun_relE)+
+ by (force elim: rel_funE)+
lemma cond_prs:
assumes a: "Quotient3 R absf repf"
@@ -563,7 +563,7 @@
lemma let_rsp:
shows "(R1 ===> (R1 ===> R2) ===> R2) Let Let"
- by (force elim: fun_relE)
+ by (force elim: rel_funE)
lemma id_rsp:
shows "(R ===> R) id id"
@@ -759,7 +759,7 @@
ML_file "Tools/Quotient/quotient_info.ML"
setup Quotient_Info.setup
-declare [[mapQ3 "fun" = (fun_rel, fun_quotient3)]]
+declare [[mapQ3 "fun" = (rel_fun, fun_quotient3)]]
lemmas [quot_thm] = fun_quotient3
lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp id_rsp
--- a/src/HOL/Quotient_Examples/FSet.thy Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Quotient_Examples/FSet.thy Thu Mar 06 15:40:33 2014 +0100
@@ -403,7 +403,7 @@
lemma Cons_rsp2 [quot_respect]:
shows "(op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) Cons Cons"
- apply (auto intro!: fun_relI)
+ apply (auto intro!: rel_funI)
apply (rule_tac b="x # b" in relcomppI)
apply auto
apply (rule_tac b="x # ba" in relcomppI)
@@ -459,24 +459,24 @@
lemma compositional_rsp3:
assumes "(R1 ===> R2 ===> R3) C C" and "(R4 ===> R5 ===> R6) C C"
shows "(R1 OOO R4 ===> R2 OOO R5 ===> R3 OOO R6) C C"
- by (auto intro!: fun_relI)
- (metis (full_types) assms fun_relE relcomppI)
+ by (auto intro!: rel_funI)
+ (metis (full_types) assms rel_funE relcomppI)
lemma append_rsp2 [quot_respect]:
"(list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) append append"
by (intro compositional_rsp3)
- (auto intro!: fun_relI simp add: append_rsp2_pre)
+ (auto intro!: rel_funI simp add: append_rsp2_pre)
lemma map_rsp2 [quot_respect]:
"((op \<approx> ===> op \<approx>) ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) map map"
-proof (auto intro!: fun_relI)
+proof (auto intro!: rel_funI)
fix f f' :: "'a list \<Rightarrow> 'b list"
fix xa ya x y :: "'a list list"
assume fs: "(op \<approx> ===> op \<approx>) f f'" and x: "list_all2 op \<approx> xa x" and xy: "set x = set y" and y: "list_all2 op \<approx> y ya"
have a: "(list_all2 op \<approx>) (map f xa) (map f x)"
using x
by (induct xa x rule: list_induct2')
- (simp_all, metis fs fun_relE list_eq_def)
+ (simp_all, metis fs rel_funE list_eq_def)
have b: "set (map f x) = set (map f y)"
using xy fs
by (induct x y rule: list_induct2')
--- a/src/HOL/Real.thy Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Real.thy Thu Mar 06 15:40:33 2014 +0100
@@ -389,7 +389,7 @@
lemma eq_Real:
"cauchy X \<Longrightarrow> cauchy Y \<Longrightarrow> Real X = Real Y \<longleftrightarrow> vanishes (\<lambda>n. X n - Y n)"
using real.rel_eq_transfer
- unfolding real.pcr_cr_eq cr_real_def fun_rel_def realrel_def by simp
+ unfolding real.pcr_cr_eq cr_real_def rel_fun_def realrel_def by simp
lemma Domainp_pcr_real [transfer_domain_rule]: "Domainp pcr_real = cauchy"
by (simp add: real.domain_eq realrel_def)
@@ -445,13 +445,13 @@
assumes X: "cauchy X" and Y: "cauchy Y"
shows "Real X + Real Y = Real (\<lambda>n. X n + Y n)"
using assms plus_real.transfer
- unfolding cr_real_eq fun_rel_def by simp
+ unfolding cr_real_eq rel_fun_def by simp
lemma minus_Real:
assumes X: "cauchy X"
shows "- Real X = Real (\<lambda>n. - X n)"
using assms uminus_real.transfer
- unfolding cr_real_eq fun_rel_def by simp
+ unfolding cr_real_eq rel_fun_def by simp
lemma diff_Real:
assumes X: "cauchy X" and Y: "cauchy Y"
@@ -463,14 +463,14 @@
assumes X: "cauchy X" and Y: "cauchy Y"
shows "Real X * Real Y = Real (\<lambda>n. X n * Y n)"
using assms times_real.transfer
- unfolding cr_real_eq fun_rel_def by simp
+ unfolding cr_real_eq rel_fun_def by simp
lemma inverse_Real:
assumes X: "cauchy X"
shows "inverse (Real X) =
(if vanishes X then 0 else Real (\<lambda>n. inverse (X n)))"
using assms inverse_real.transfer zero_real.transfer
- unfolding cr_real_eq fun_rel_def by (simp split: split_if_asm, metis)
+ unfolding cr_real_eq rel_fun_def by (simp split: split_if_asm, metis)
instance proof
fix a b c :: real
@@ -546,7 +546,7 @@
assumes X: "cauchy X"
shows "positive (Real X) \<longleftrightarrow> (\<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < X n)"
using assms positive.transfer
- unfolding cr_real_eq fun_rel_def by simp
+ unfolding cr_real_eq rel_fun_def by simp
lemma positive_zero: "\<not> positive 0"
by transfer auto
--- a/src/HOL/Tools/BNF/bnf_def.ML Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_def.ML Thu Mar 06 15:40:33 2014 +0100
@@ -1260,12 +1260,12 @@
fun mk_map_transfer () =
let
- val rels = map2 mk_fun_rel transfer_domRs transfer_ranRs;
- val rel = mk_fun_rel
+ val rels = map2 mk_rel_fun transfer_domRs transfer_ranRs;
+ val rel = mk_rel_fun
(Term.list_comb (mk_bnf_rel transfer_domRTs CA' CB1, transfer_domRs))
(Term.list_comb (mk_bnf_rel transfer_ranRTs CB' CB2, transfer_ranRs));
val concl = HOLogic.mk_Trueprop
- (fold_rev mk_fun_rel rels rel $ bnf_map_AsBs $ mk_bnf_map B1Ts B2Ts);
+ (fold_rev mk_rel_fun rels rel $ bnf_map_AsBs $ mk_bnf_map B1Ts B2Ts);
in
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (transfer_domRs @ transfer_ranRs) concl)
--- a/src/HOL/Tools/BNF/bnf_def_tactics.ML Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML Thu Mar 06 15:40:33 2014 +0100
@@ -195,8 +195,8 @@
@{thm ord_eq_le_trans[OF _ subset_trans[OF image_mono convol_image_vimage2p]]}))
set_maps;
in
- REPEAT_DETERM_N n (HEADGOAL (rtac @{thm fun_relI})) THEN
- unfold_thms_tac ctxt @{thms fun_rel_iff_leq_vimage2p} THEN
+ REPEAT_DETERM_N n (HEADGOAL (rtac @{thm rel_funI})) THEN
+ unfold_thms_tac ctxt @{thms rel_fun_iff_leq_vimage2p} THEN
HEADGOAL (EVERY' [rtac @{thm order_trans}, rtac rel_mono, REPEAT_DETERM_N n o atac,
rtac @{thm predicate2I}, dtac (in_rel RS iffD1),
REPEAT_DETERM o eresolve_tac [exE, CollectE, conjE], hyp_subst_tac ctxt,
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Thu Mar 06 15:40:33 2014 +0100
@@ -502,9 +502,9 @@
val relphis = map (fn rel => Term.list_comb (rel, phis)) rels;
fun flip f x y = if fp = Greatest_FP then f y x else f x y;
- val arg_rels = map2 (flip mk_fun_rel) pre_relphis pre_phis;
+ val arg_rels = map2 (flip mk_rel_fun) pre_relphis pre_phis;
fun mk_transfer relphi pre_phi un_fold un_fold' =
- fold_rev mk_fun_rel arg_rels (flip mk_fun_rel relphi pre_phi) $ un_fold $ un_fold';
+ fold_rev mk_rel_fun arg_rels (flip mk_rel_fun relphi pre_phi) $ un_fold $ un_fold';
val transfers = map4 mk_transfer relphis pre_phis un_folds un_folds';
val goal = fold_rev Logic.all (phis @ pre_phis)
--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Thu Mar 06 15:40:33 2014 +0100
@@ -1088,16 +1088,16 @@
val n = length map_transfers;
in
unfold_thms_tac ctxt
- @{thms fun_rel_def_butlast all_conj_distrib[symmetric] imp_conjR[symmetric]} THEN
- unfold_thms_tac ctxt @{thms fun_rel_iff_geq_image2p} THEN
+ @{thms rel_fun_def_butlast all_conj_distrib[symmetric] imp_conjR[symmetric]} THEN
+ unfold_thms_tac ctxt @{thms rel_fun_iff_geq_image2p} THEN
HEADGOAL (EVERY'
[REPEAT_DETERM o resolve_tac [allI, impI], rtac ctor_rel_coinduct,
EVERY' (map (fn map_transfer => EVERY'
[REPEAT_DETERM o resolve_tac [allI, impI], etac @{thm image2pE}, hyp_subst_tac ctxt,
SELECT_GOAL (unfold_thms_tac ctxt unfolds),
- rtac (funpow (m + n + 1) (fn thm => thm RS @{thm fun_relD}) map_transfer),
+ rtac (funpow (m + n + 1) (fn thm => thm RS @{thm rel_funD}) map_transfer),
REPEAT_DETERM_N m o rtac @{thm id_transfer},
- REPEAT_DETERM_N n o rtac @{thm fun_rel_image2p},
+ REPEAT_DETERM_N n o rtac @{thm rel_fun_image2p},
etac @{thm predicate2D}, etac @{thm image2pI}])
map_transfers)])
end;
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Thu Mar 06 15:40:33 2014 +0100
@@ -788,17 +788,17 @@
val n = length map_transfers;
in
unfold_thms_tac ctxt
- @{thms fun_rel_def_butlast all_conj_distrib[symmetric] imp_conjR[symmetric]} THEN
- unfold_thms_tac ctxt @{thms fun_rel_iff_leq_vimage2p} THEN
+ @{thms rel_fun_def_butlast all_conj_distrib[symmetric] imp_conjR[symmetric]} THEN
+ unfold_thms_tac ctxt @{thms rel_fun_iff_leq_vimage2p} THEN
HEADGOAL (EVERY'
[REPEAT_DETERM o resolve_tac [allI, impI], rtac ctor_rel_induct,
EVERY' (map (fn map_transfer => EVERY'
[REPEAT_DETERM o resolve_tac [allI, impI, @{thm vimage2pI}],
SELECT_GOAL (unfold_thms_tac ctxt folds),
etac @{thm predicate2D_vimage2p},
- rtac (funpow (m + n + 1) (fn thm => thm RS @{thm fun_relD}) map_transfer),
+ rtac (funpow (m + n + 1) (fn thm => thm RS @{thm rel_funD}) map_transfer),
REPEAT_DETERM_N m o rtac @{thm id_transfer},
- REPEAT_DETERM_N n o rtac @{thm vimage2p_fun_rel},
+ REPEAT_DETERM_N n o rtac @{thm vimage2p_rel_fun},
atac])
map_transfers)])
end;
--- a/src/HOL/Tools/BNF/bnf_util.ML Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_util.ML Thu Mar 06 15:40:33 2014 +0100
@@ -94,7 +94,7 @@
val mk_cprod: term -> term -> term
val mk_csum: term -> term -> term
val mk_dir_image: term -> term -> term
- val mk_fun_rel: term -> term -> term
+ val mk_rel_fun: term -> term -> term
val mk_image: term -> term
val mk_in: term list -> term list -> typ -> term
val mk_leq: term -> term -> term
@@ -438,11 +438,11 @@
let val (T, U) = dest_funT (fastype_of f);
in Const (@{const_name dir_image}, mk_relT (T, T) --> (T --> U) --> mk_relT (U, U)) $ r $ f end;
-fun mk_fun_rel R S =
+fun mk_rel_fun R S =
let
val ((RA, RB), RT) = `dest_pred2T (fastype_of R);
val ((SA, SB), ST) = `dest_pred2T (fastype_of S);
- in Const (@{const_name fun_rel}, RT --> ST --> mk_pred2T (RA --> SA) (RB --> SB)) $ R $ S end;
+ in Const (@{const_name rel_fun}, RT --> ST --> mk_pred2T (RA --> SA) (RB --> SB)) $ R $ S end;
(*FIXME: "x"?*)
(*(nth sets i) must be of type "T --> 'ai set"*)
--- a/src/HOL/Tools/Lifting/lifting_def.ML Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Thu Mar 06 15:40:33 2014 +0100
@@ -166,11 +166,11 @@
fun get_binder_types (Type ("fun", [T, U]), Type ("fun", [V, W])) = (T, V) :: get_binder_types (U, W)
| get_binder_types _ = []
-fun get_binder_types_by_rel (Const (@{const_name "fun_rel"}, _) $ _ $ S) (Type ("fun", [T, U]), Type ("fun", [V, W])) =
+fun get_binder_types_by_rel (Const (@{const_name "rel_fun"}, _) $ _ $ S) (Type ("fun", [T, U]), Type ("fun", [V, W])) =
(T, V) :: get_binder_types_by_rel S (U, W)
| get_binder_types_by_rel _ _ = []
-fun get_body_type_by_rel (Const (@{const_name "fun_rel"}, _) $ _ $ S) (Type ("fun", [_, U]), Type ("fun", [_, V])) =
+fun get_body_type_by_rel (Const (@{const_name "rel_fun"}, _) $ _ $ S) (Type ("fun", [_, U]), Type ("fun", [_, V])) =
get_body_type_by_rel S (U, V)
| get_body_type_by_rel _ (U, V) = (U, V)
@@ -270,8 +270,8 @@
let
val thy = Proof_Context.theory_of ctxt
val quot_thm = Lifting_Term.prove_quot_thm ctxt (get_body_types (rty, qty))
- val fun_rel = prove_rel ctxt rsp_thm (rty, qty)
- val rep_abs_thm = [quot_thm, fun_rel] MRSL @{thm Quotient_rep_abs_eq}
+ val rel_fun = prove_rel ctxt rsp_thm (rty, qty)
+ val rep_abs_thm = [quot_thm, rel_fun] MRSL @{thm Quotient_rep_abs_eq}
in
case mono_eq_prover ctxt (hd(prems_of rep_abs_thm)) of
SOME mono_eq_thm =>
@@ -311,7 +311,7 @@
end
in
rep_abs_folded_unmapped_thm
- |> fold (fn _ => fn thm => thm RS @{thm fun_relD2}) ty_args
+ |> fold (fn _ => fn thm => thm RS @{thm rel_funD2}) ty_args
|> (fn x => x RS (@{thm Quotient_rel_abs2} OF [quot_ret_thm]))
end
@@ -505,11 +505,11 @@
fun simp_arrows_conv ctm =
let
val unfold_conv = Conv.rewrs_conv
- [@{thm fun_rel_eq_invariant[THEN eq_reflection]},
- @{thm fun_rel_invariant_rel[THEN eq_reflection]},
- @{thm fun_rel_eq[THEN eq_reflection]},
- @{thm fun_rel_eq_rel[THEN eq_reflection]},
- @{thm fun_rel_def[THEN eq_reflection]}]
+ [@{thm rel_fun_eq_invariant[THEN eq_reflection]},
+ @{thm rel_fun_invariant_rel[THEN eq_reflection]},
+ @{thm rel_fun_eq[THEN eq_reflection]},
+ @{thm rel_fun_eq_rel[THEN eq_reflection]},
+ @{thm rel_fun_def[THEN eq_reflection]}]
fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
val invariant_assms_tac_rules = @{thm left_unique_composition} ::
invariant_assms_tac_fixed_rules @ (Transfer.get_transfer_raw lthy)
@@ -522,7 +522,7 @@
(K (Conv.try_conv (Conv.rewrs_conv (Transfer.get_relator_eq lthy)))) lthy
in
case (Thm.term_of ctm) of
- Const (@{const_name "fun_rel"}, _) $ _ $ _ =>
+ Const (@{const_name "rel_fun"}, _) $ _ $ _ =>
(binop_conv2 simp_arrows_conv simp_arrows_conv then_conv unfold_conv) ctm
| _ => (invariant_commute_conv then_conv relator_eq_conv) ctm
end
--- a/src/HOL/Tools/Lifting/lifting_util.ML Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_util.ML Thu Mar 06 15:40:33 2014 +0100
@@ -27,7 +27,7 @@
val same_type_constrs: typ * typ -> bool
val Targs: typ -> typ list
val Tname: typ -> string
- val is_fun_rel: term -> bool
+ val is_rel_fun: term -> bool
val relation_types: typ -> typ * typ
val mk_HOL_eq: thm -> thm
val safe_HOL_meta_eq: thm -> thm
@@ -110,8 +110,8 @@
fun Tname (Type (name, _)) = name
| Tname _ = ""
-fun is_fun_rel (Const (@{const_name "fun_rel"}, _) $ _ $ _) = true
- | is_fun_rel _ = false
+fun is_rel_fun (Const (@{const_name "rel_fun"}, _) $ _ $ _) = true
+ | is_rel_fun _ = false
fun relation_types typ =
case strip_type typ of
--- a/src/HOL/Tools/Quotient/quotient_def.ML Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Thu Mar 06 15:40:33 2014 +0100
@@ -109,13 +109,13 @@
fun simp_arrows_conv ctm =
let
val unfold_conv = Conv.rewrs_conv
- [@{thm fun_rel_eq_invariant[THEN eq_reflection]}, @{thm fun_rel_eq_rel[THEN eq_reflection]},
- @{thm fun_rel_def[THEN eq_reflection]}]
+ [@{thm rel_fun_eq_invariant[THEN eq_reflection]}, @{thm rel_fun_eq_rel[THEN eq_reflection]},
+ @{thm rel_fun_def[THEN eq_reflection]}]
val left_conv = simp_arrows_conv then_conv Conv.try_conv norm_fun_eq
fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
in
case (Thm.term_of ctm) of
- Const (@{const_name fun_rel}, _) $ _ $ _ =>
+ Const (@{const_name rel_fun}, _) $ _ $ _ =>
(binop_conv2 left_conv simp_arrows_conv then_conv unfold_conv) ctm
| _ => Conv.all_conv ctm
end
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Thu Mar 06 15:40:33 2014 +0100
@@ -114,11 +114,11 @@
fun ball_bex_range_simproc ctxt redex =
case redex of
(Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $
- (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
+ (Const (@{const_name "rel_fun"}, _) $ R1 $ R2)) $ _) =>
calculate_inst ctxt @{thm ball_reg_eqv_range[THEN eq_reflection]} redex R1 R2
| (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $
- (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
+ (Const (@{const_name "rel_fun"}, _) $ R1 $ R2)) $ _) =>
calculate_inst ctxt @{thm bex_reg_eqv_range[THEN eq_reflection]} redex R1 R2
| _ => NONE
@@ -306,7 +306,7 @@
The deterministic part:
- remove lambdas from both sides
- prove Ball/Bex/Babs equalities using ball_rsp, bex_rsp, babs_rsp
- - prove Ball/Bex relations using fun_relI
+ - prove Ball/Bex relations using rel_funI
- reflexivity of equality
- prove equality of relations using equals_rsp
- use user-supplied RSP theorems
@@ -324,8 +324,8 @@
fun injection_match_tac ctxt = SUBGOAL (fn (goal, i) =>
(case bare_concl goal of
(* (R1 ===> R2) (%x...) (%x...) ----> [|R1 x y|] ==> R2 (...x) (...y) *)
- (Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _)
- => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
+ (Const (@{const_name rel_fun}, _) $ _ $ _) $ (Abs _) $ (Abs _)
+ => rtac @{thm rel_funI} THEN' quot_true_tac ctxt unlam
(* (op =) (Ball...) (Ball...) ----> (op =) (...) (...) *)
| (Const (@{const_name HOL.eq},_) $
@@ -334,10 +334,10 @@
=> rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}
(* (R1 ===> op =) (Ball...) (Ball...) ----> [|R1 x y|] ==> (Ball...x) = (Ball...y) *)
- | (Const (@{const_name fun_rel}, _) $ _ $ _) $
+ | (Const (@{const_name rel_fun}, _) $ _ $ _) $
(Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
(Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
- => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
+ => rtac @{thm rel_funI} THEN' quot_true_tac ctxt unlam
(* (op =) (Bex...) (Bex...) ----> (op =) (...) (...) *)
| Const (@{const_name HOL.eq},_) $
@@ -346,12 +346,12 @@
=> rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}
(* (R1 ===> op =) (Bex...) (Bex...) ----> [|R1 x y|] ==> (Bex...x) = (Bex...y) *)
- | (Const (@{const_name fun_rel}, _) $ _ $ _) $
+ | (Const (@{const_name rel_fun}, _) $ _ $ _) $
(Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
(Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
- => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
+ => rtac @{thm rel_funI} THEN' quot_true_tac ctxt unlam
- | (Const (@{const_name fun_rel}, _) $ _ $ _) $
+ | (Const (@{const_name rel_fun}, _) $ _ $ _) $
(Const(@{const_name Bex1_rel},_) $ _) $ (Const(@{const_name Bex1_rel},_) $ _)
=> rtac @{thm bex1_rel_rsp} THEN' quotient_tac ctxt
@@ -369,7 +369,7 @@
| Const (@{const_name HOL.eq},_) $ _ $ _ => rtac @{thm refl}
(* respectfulness of constants; in particular of a simple relation *)
- | _ $ (Const _) $ (Const _) (* fun_rel, list_rel, etc but not equality *)
+ | _ $ (Const _) $ (Const _) (* rel_fun, list_rel, etc but not equality *)
=> resolve_tac (Quotient_Info.rsp_rules ctxt) THEN_ALL_NEW quotient_tac ctxt
(* R (...) (Rep (Abs ...)) ----> R (...) (...) *)
--- a/src/HOL/Tools/transfer.ML Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Tools/transfer.ML Thu Mar 06 15:40:33 2014 +0100
@@ -389,7 +389,7 @@
val r2 = rel T2 U2
val rT = fastype_of r1 --> fastype_of r2 --> mk_relT (T, U)
in
- Const (@{const_name fun_rel}, rT) $ r1 $ r2
+ Const (@{const_name rel_fun}, rT) $ r1 $ r2
end
| rel T U =
let
@@ -617,7 +617,7 @@
val rule1 = transfer_rule_of_term ctxt false rhs
val rules = get_transfer_raw ctxt
val eq_rules = get_relator_eq_raw ctxt
- val expand_eq_in_rel = transfer_rel_conv (top_rewr_conv [@{thm fun_rel_eq[symmetric,THEN eq_reflection]}])
+ val expand_eq_in_rel = transfer_rel_conv (top_rewr_conv [@{thm rel_fun_eq[symmetric,THEN eq_reflection]}])
in
EVERY
[CONVERSION prep_conv i,
--- a/src/HOL/Topological_Spaces.thy Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Topological_Spaces.thy Thu Mar 06 15:40:33 2014 +0100
@@ -2363,23 +2363,23 @@
fix F G
assume "rel_filter T F G"
thus "filtermap Abs F = G" unfolding filter_eq_iff
- by(auto simp add: eventually_filtermap rel_filter_eventually * fun_relI del: iffI elim!: fun_relD)
+ by(auto simp add: eventually_filtermap rel_filter_eventually * rel_funI del: iffI elim!: rel_funD)
next
from Q have *: "\<And>x. T (Rep x) x" unfolding Quotient_alt_def by blast
fix F
show "rel_filter T (filtermap Rep F) F"
- by(auto elim: fun_relD intro: * intro!: ext arg_cong[where f="\<lambda>P. eventually P F"] fun_relI
+ by(auto elim: rel_funD intro: * intro!: ext arg_cong[where f="\<lambda>P. eventually P F"] rel_funI
del: iffI simp add: eventually_filtermap rel_filter_eventually)
qed(auto simp add: map_fun_def o_def eventually_filtermap filter_eq_iff fun_eq_iff rel_filter_eventually
fun_quotient[OF fun_quotient[OF Q identity_quotient] identity_quotient, unfolded Quotient_alt_def])
lemma eventually_parametric [transfer_rule]:
"((A ===> op =) ===> rel_filter A ===> op =) eventually eventually"
-by(simp add: fun_rel_def rel_filter_eventually)
+by(simp add: rel_fun_def rel_filter_eventually)
lemma rel_filter_eq [relator_eq]: "rel_filter op = = op ="
-by(auto simp add: rel_filter_eventually fun_rel_eq fun_eq_iff filter_eq_iff)
+by(auto simp add: rel_filter_eventually rel_fun_eq fun_eq_iff filter_eq_iff)
lemma rel_filter_mono [relator_mono]:
"A \<le> B \<Longrightarrow> rel_filter A \<le> rel_filter B"
@@ -2387,7 +2387,7 @@
by(rule le_funI)+(intro fun_mono fun_mono[THEN le_funD, THEN le_funD] order.refl)
lemma rel_filter_conversep [simp]: "rel_filter A\<inverse>\<inverse> = (rel_filter A)\<inverse>\<inverse>"
-by(auto simp add: rel_filter_eventually fun_eq_iff fun_rel_def)
+by(auto simp add: rel_filter_eventually fun_eq_iff rel_fun_def)
lemma is_filter_parametric_aux:
assumes "is_filter F"
@@ -2427,11 +2427,11 @@
lemma is_filter_parametric [transfer_rule]:
"\<lbrakk> bi_total A; bi_unique A \<rbrakk>
\<Longrightarrow> (((A ===> op =) ===> op =) ===> op =) is_filter is_filter"
-apply(rule fun_relI)
+apply(rule rel_funI)
apply(rule iffI)
apply(erule (3) is_filter_parametric_aux)
apply(erule is_filter_parametric_aux[where A="conversep A"])
-apply(auto simp add: fun_rel_def)
+apply(auto simp add: rel_fun_def)
done
lemma left_total_rel_filter [reflexivity_rule]:
@@ -2490,15 +2490,15 @@
by(simp add: rel_filter_eventually All_transfer)
lemma bot_filter_parametric [transfer_rule]: "(rel_filter A) bot bot"
-by(simp add: rel_filter_eventually fun_rel_def)
+by(simp add: rel_filter_eventually rel_fun_def)
lemma sup_filter_parametric [transfer_rule]:
"(rel_filter A ===> rel_filter A ===> rel_filter A) sup sup"
-by(fastforce simp add: rel_filter_eventually[abs_def] eventually_sup dest: fun_relD)
+by(fastforce simp add: rel_filter_eventually[abs_def] eventually_sup dest: rel_funD)
lemma Sup_filter_parametric [transfer_rule]:
"(rel_set (rel_filter A) ===> rel_filter A) Sup Sup"
-proof(rule fun_relI)
+proof(rule rel_funI)
fix S T
assume [transfer_rule]: "rel_set (rel_filter A) S T"
show "rel_filter A (Sup S) (Sup T)"
@@ -2507,7 +2507,7 @@
lemma principal_parametric [transfer_rule]:
"(rel_set A ===> rel_filter A) principal principal"
-proof(rule fun_relI)
+proof(rule rel_funI)
fix S S'
assume [transfer_rule]: "rel_set A S S'"
show "rel_filter A (principal S) (principal S')"
@@ -2537,7 +2537,7 @@
lemma inf_filter_parametric [transfer_rule]:
"(rel_filter A ===> rel_filter A ===> rel_filter A) inf inf"
-proof(intro fun_relI)+
+proof(intro rel_funI)+
fix F F' G G'
assume [transfer_rule]: "rel_filter A F F'" "rel_filter A G G'"
have "rel_filter A (Inf {F, G}) (Inf {F', G'})" by transfer_prover
--- a/src/HOL/Transfer.thy Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Transfer.thy Thu Mar 06 15:40:33 2014 +0100
@@ -13,7 +13,7 @@
locale lifting_syntax
begin
- notation fun_rel (infixr "===>" 55)
+ notation rel_fun (infixr "===>" 55)
notation map_fun (infixr "--->" 55)
end
@@ -21,21 +21,21 @@
begin
interpretation lifting_syntax .
-lemma fun_relD2:
- assumes "fun_rel A B f g" and "A x x"
+lemma rel_funD2:
+ assumes "rel_fun A B f g" and "A x x"
shows "B (f x) (g x)"
- using assms by (rule fun_relD)
+ using assms by (rule rel_funD)
-lemma fun_relE:
- assumes "fun_rel A B f g" and "A x y"
+lemma rel_funE:
+ assumes "rel_fun A B f g" and "A x y"
obtains "B (f x) (g y)"
- using assms by (simp add: fun_rel_def)
+ using assms by (simp add: rel_fun_def)
-lemmas fun_rel_eq = fun.rel_eq
+lemmas rel_fun_eq = fun.rel_eq
-lemma fun_rel_eq_rel:
-shows "fun_rel (op =) R = (\<lambda>f g. \<forall>x. R (f x) (g x))"
- by (simp add: fun_rel_def)
+lemma rel_fun_eq_rel:
+shows "rel_fun (op =) R = (\<lambda>f g. \<forall>x. R (f x) (g x))"
+ by (simp add: rel_fun_def)
subsection {* Transfer method *}
@@ -98,12 +98,12 @@
lemma Rel_app:
assumes "Rel (A ===> B) f g" and "Rel A x y"
shows "Rel B (f x) (g y)"
- using assms unfolding Rel_def fun_rel_def by fast
+ using assms unfolding Rel_def rel_fun_def by fast
lemma Rel_abs:
assumes "\<And>x y. Rel A x y \<Longrightarrow> Rel B (f x) (g y)"
shows "Rel (A ===> B) (\<lambda>x. f x) (\<lambda>y. g y)"
- using assms unfolding Rel_def fun_rel_def by fast
+ using assms unfolding Rel_def rel_fun_def by fast
end
@@ -112,7 +112,7 @@
declare refl [transfer_rule]
-declare fun_rel_eq [relator_eq]
+declare rel_fun_eq [relator_eq]
hide_const (open) Rel
@@ -131,7 +131,7 @@
lemma Domainp_prod_fun_eq[transfer_domain_rule]:
assumes "Domainp T = P"
shows "Domainp (op= ===> T) = (\<lambda>f. \<forall>x. P (f x))"
-by (auto intro: choice simp: assms[symmetric] Domainp_iff fun_rel_def fun_eq_iff)
+by (auto intro: choice simp: assms[symmetric] Domainp_iff rel_fun_def fun_eq_iff)
subsection {* Predicates on relations, i.e. ``class constraints'' *}
@@ -163,7 +163,7 @@
lemma right_total_alt_def:
"right_total R \<longleftrightarrow> ((R ===> op \<longrightarrow>) ===> op \<longrightarrow>) All All"
- unfolding right_total_def fun_rel_def
+ unfolding right_total_def rel_fun_def
apply (rule iffI, fast)
apply (rule allI)
apply (drule_tac x="\<lambda>x. True" in spec)
@@ -173,11 +173,11 @@
lemma right_unique_alt_def:
"right_unique R \<longleftrightarrow> (R ===> R ===> op \<longrightarrow>) (op =) (op =)"
- unfolding right_unique_def fun_rel_def by auto
+ unfolding right_unique_def rel_fun_def by auto
lemma bi_total_alt_def:
"bi_total R \<longleftrightarrow> ((R ===> op =) ===> op =) All All"
- unfolding bi_total_def fun_rel_def
+ unfolding bi_total_def rel_fun_def
apply (rule iffI, fast)
apply safe
apply (drule_tac x="\<lambda>x. \<exists>y. R x y" in spec)
@@ -190,7 +190,7 @@
lemma bi_unique_alt_def:
"bi_unique R \<longleftrightarrow> (R ===> R ===> op =) (op =) (op =)"
- unfolding bi_unique_def fun_rel_def by auto
+ unfolding bi_unique_def rel_fun_def by auto
lemma bi_unique_conversep [simp]: "bi_unique R\<inverse>\<inverse> = bi_unique R"
by(auto simp add: bi_unique_def)
@@ -234,7 +234,7 @@
lemma right_total_fun [transfer_rule]:
"\<lbrakk>right_unique A; right_total B\<rbrakk> \<Longrightarrow> right_total (A ===> B)"
- unfolding right_total_def fun_rel_def
+ unfolding right_total_def rel_fun_def
apply (rule allI, rename_tac g)
apply (rule_tac x="\<lambda>x. SOME z. B z (g (THE y. A x y))" in exI)
apply clarify
@@ -248,12 +248,12 @@
lemma right_unique_fun [transfer_rule]:
"\<lbrakk>right_total A; right_unique B\<rbrakk> \<Longrightarrow> right_unique (A ===> B)"
- unfolding right_total_def right_unique_def fun_rel_def
+ unfolding right_total_def right_unique_def rel_fun_def
by (clarify, rule ext, fast)
lemma bi_total_fun [transfer_rule]:
"\<lbrakk>bi_unique A; bi_total B\<rbrakk> \<Longrightarrow> bi_total (A ===> B)"
- unfolding bi_total_def fun_rel_def
+ unfolding bi_total_def rel_fun_def
apply safe
apply (rename_tac f)
apply (rule_tac x="\<lambda>y. SOME z. B (f (THE x. A x y)) z" in exI)
@@ -277,7 +277,7 @@
lemma bi_unique_fun [transfer_rule]:
"\<lbrakk>bi_total A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (A ===> B)"
- unfolding bi_total_def bi_unique_def fun_rel_def fun_eq_iff
+ unfolding bi_total_def bi_unique_def rel_fun_def fun_eq_iff
by (safe, metis, fast)
@@ -288,7 +288,7 @@
shows "((A ===> op =) ===> op =)
(transfer_bforall (Domainp A)) transfer_forall"
using assms unfolding right_total_def
- unfolding transfer_forall_def transfer_bforall_def fun_rel_def Domainp_iff
+ unfolding transfer_forall_def transfer_bforall_def rel_fun_def Domainp_iff
by metis
text {* Transfer rules using implication instead of equality on booleans. *}
@@ -299,7 +299,7 @@
"right_total A \<Longrightarrow> ((A ===> implies) ===> implies) transfer_forall transfer_forall"
"bi_total A \<Longrightarrow> ((A ===> op =) ===> rev_implies) transfer_forall transfer_forall"
"bi_total A \<Longrightarrow> ((A ===> rev_implies) ===> rev_implies) transfer_forall transfer_forall"
- unfolding transfer_forall_def rev_implies_def fun_rel_def right_total_def bi_total_def
+ unfolding transfer_forall_def rev_implies_def rel_fun_def right_total_def bi_total_def
by metis+
lemma transfer_implies_transfer [transfer_rule]:
@@ -312,7 +312,7 @@
"(implies ===> op = ===> rev_implies) transfer_implies transfer_implies"
"(op = ===> rev_implies ===> rev_implies) transfer_implies transfer_implies"
"(op = ===> op = ===> rev_implies) transfer_implies transfer_implies"
- unfolding transfer_implies_def rev_implies_def fun_rel_def by auto
+ unfolding transfer_implies_def rev_implies_def rel_fun_def by auto
lemma eq_imp_transfer [transfer_rule]:
"right_unique A \<Longrightarrow> (A ===> A ===> op \<longrightarrow>) (op =) (op =)"
@@ -321,42 +321,42 @@
lemma eq_transfer [transfer_rule]:
assumes "bi_unique A"
shows "(A ===> A ===> op =) (op =) (op =)"
- using assms unfolding bi_unique_def fun_rel_def by auto
+ using assms unfolding bi_unique_def rel_fun_def by auto
lemma right_total_Ex_transfer[transfer_rule]:
assumes "right_total A"
shows "((A ===> op=) ===> op=) (Bex (Collect (Domainp A))) Ex"
-using assms unfolding right_total_def Bex_def fun_rel_def Domainp_iff[abs_def]
+using assms unfolding right_total_def Bex_def rel_fun_def Domainp_iff[abs_def]
by blast
lemma right_total_All_transfer[transfer_rule]:
assumes "right_total A"
shows "((A ===> op =) ===> op =) (Ball (Collect (Domainp A))) All"
-using assms unfolding right_total_def Ball_def fun_rel_def Domainp_iff[abs_def]
+using assms unfolding right_total_def Ball_def rel_fun_def Domainp_iff[abs_def]
by blast
lemma All_transfer [transfer_rule]:
assumes "bi_total A"
shows "((A ===> op =) ===> op =) All All"
- using assms unfolding bi_total_def fun_rel_def by fast
+ using assms unfolding bi_total_def rel_fun_def by fast
lemma Ex_transfer [transfer_rule]:
assumes "bi_total A"
shows "((A ===> op =) ===> op =) Ex Ex"
- using assms unfolding bi_total_def fun_rel_def by fast
+ using assms unfolding bi_total_def rel_fun_def by fast
lemma If_transfer [transfer_rule]: "(op = ===> A ===> A ===> A) If If"
- unfolding fun_rel_def by simp
+ unfolding rel_fun_def by simp
lemma Let_transfer [transfer_rule]: "(A ===> (A ===> B) ===> B) Let Let"
- unfolding fun_rel_def by simp
+ unfolding rel_fun_def by simp
lemma id_transfer [transfer_rule]: "(A ===> A) id id"
- unfolding fun_rel_def by simp
+ unfolding rel_fun_def by simp
lemma comp_transfer [transfer_rule]:
"((B ===> C) ===> (A ===> B) ===> (A ===> C)) (op \<circ>) (op \<circ>)"
- unfolding fun_rel_def by simp
+ unfolding rel_fun_def by simp
lemma fun_upd_transfer [transfer_rule]:
assumes [transfer_rule]: "bi_unique A"
@@ -365,11 +365,11 @@
lemma case_nat_transfer [transfer_rule]:
"(A ===> (op = ===> A) ===> op = ===> A) case_nat case_nat"
- unfolding fun_rel_def by (simp split: nat.split)
+ unfolding rel_fun_def by (simp split: nat.split)
lemma rec_nat_transfer [transfer_rule]:
"(A ===> (op = ===> A ===> A) ===> op = ===> A) rec_nat rec_nat"
- unfolding fun_rel_def by (clarsimp, rename_tac n, induct_tac n, simp_all)
+ unfolding rel_fun_def by (clarsimp, rename_tac n, induct_tac n, simp_all)
lemma funpow_transfer [transfer_rule]:
"(op = ===> (A ===> A) ===> (A ===> A)) compow compow"
@@ -409,7 +409,7 @@
"right_total A \<Longrightarrow> ((A ===> A ===> op=) ===> implies) reflp reflp"
"bi_total A \<Longrightarrow> ((A ===> A ===> rev_implies) ===> rev_implies) reflp reflp"
"bi_total A \<Longrightarrow> ((A ===> A ===> op=) ===> rev_implies) reflp reflp"
-using assms unfolding reflp_def[abs_def] rev_implies_def bi_total_def right_total_def fun_rel_def
+using assms unfolding reflp_def[abs_def] rev_implies_def bi_total_def right_total_def rel_fun_def
by fast+
lemma right_unique_transfer [transfer_rule]:
@@ -417,7 +417,7 @@
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 fun_rel_def
+using assms unfolding right_unique_def[abs_def] right_total_def bi_unique_def rel_fun_def
by metis
end
--- a/src/HOL/Word/Word.thy Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Word/Word.thy Thu Mar 06 15:40:33 2014 +0100
@@ -193,9 +193,9 @@
text {* TODO: The next lemma could be generated automatically. *}
lemma uint_transfer [transfer_rule]:
- "(fun_rel pcr_word op =) (bintrunc (len_of TYPE('a)))
+ "(rel_fun pcr_word op =) (bintrunc (len_of TYPE('a)))
(uint :: 'a::len0 word \<Rightarrow> int)"
- unfolding fun_rel_def word.pcr_cr_eq cr_word_def
+ unfolding rel_fun_def word.pcr_cr_eq cr_word_def
by (simp add: no_bintr_alt1 uint_word_of_int)
@@ -651,9 +651,9 @@
declare word_neg_numeral_alt [symmetric, code_abbrev]
lemma word_numeral_transfer [transfer_rule]:
- "(fun_rel op = pcr_word) numeral numeral"
- "(fun_rel op = pcr_word) (- numeral) (- numeral)"
- apply (simp_all add: fun_rel_def word.pcr_cr_eq cr_word_def)
+ "(rel_fun op = pcr_word) numeral numeral"
+ "(rel_fun op = pcr_word) (- numeral) (- numeral)"
+ apply (simp_all add: rel_fun_def word.pcr_cr_eq cr_word_def)
using word_numeral_alt [symmetric] word_neg_numeral_alt [symmetric] by blast+
lemma uint_bintrunc [simp]:
@@ -2295,9 +2295,9 @@
by (simp add: word_ubin.eq_norm nth_bintr)
lemma word_test_bit_transfer [transfer_rule]:
- "(fun_rel pcr_word (fun_rel op = op =))
+ "(rel_fun pcr_word (rel_fun op = op =))
(\<lambda>x n. n < len_of TYPE('a) \<and> bin_nth x n) (test_bit :: 'a::len0 word \<Rightarrow> _)"
- unfolding fun_rel_def word.pcr_cr_eq cr_word_def by simp
+ unfolding rel_fun_def word.pcr_cr_eq cr_word_def by simp
lemma word_ops_nth_size:
"n < size (x::'a::len0 word) \<Longrightarrow>
--- a/src/HOL/ex/Transfer_Int_Nat.thy Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/ex/Transfer_Int_Nat.thy Thu Mar 06 15:40:33 2014 +0100
@@ -37,79 +37,79 @@
unfolding ZN_def by simp
lemma ZN_add [transfer_rule]: "(ZN ===> ZN ===> ZN) (op +) (op +)"
- unfolding fun_rel_def ZN_def by simp
+ unfolding rel_fun_def ZN_def by simp
lemma ZN_mult [transfer_rule]: "(ZN ===> ZN ===> ZN) (op *) (op *)"
- unfolding fun_rel_def ZN_def by (simp add: int_mult)
+ unfolding rel_fun_def ZN_def by (simp add: int_mult)
lemma ZN_diff [transfer_rule]: "(ZN ===> ZN ===> ZN) tsub (op -)"
- unfolding fun_rel_def ZN_def tsub_def by (simp add: zdiff_int)
+ unfolding rel_fun_def ZN_def tsub_def by (simp add: zdiff_int)
lemma ZN_power [transfer_rule]: "(ZN ===> op = ===> ZN) (op ^) (op ^)"
- unfolding fun_rel_def ZN_def by (simp add: int_power)
+ unfolding rel_fun_def ZN_def by (simp add: int_power)
lemma ZN_nat_id [transfer_rule]: "(ZN ===> op =) nat id"
- unfolding fun_rel_def ZN_def by simp
+ unfolding rel_fun_def ZN_def by simp
lemma ZN_id_int [transfer_rule]: "(ZN ===> op =) id int"
- unfolding fun_rel_def ZN_def by simp
+ unfolding rel_fun_def ZN_def by simp
lemma ZN_All [transfer_rule]:
"((ZN ===> op =) ===> op =) (Ball {0..}) All"
- unfolding fun_rel_def ZN_def by (auto dest: zero_le_imp_eq_int)
+ unfolding rel_fun_def ZN_def by (auto dest: zero_le_imp_eq_int)
lemma ZN_transfer_forall [transfer_rule]:
"((ZN ===> op =) ===> op =) (transfer_bforall (\<lambda>x. 0 \<le> x)) transfer_forall"
unfolding transfer_forall_def transfer_bforall_def
- unfolding fun_rel_def ZN_def by (auto dest: zero_le_imp_eq_int)
+ unfolding rel_fun_def ZN_def by (auto dest: zero_le_imp_eq_int)
lemma ZN_Ex [transfer_rule]: "((ZN ===> op =) ===> op =) (Bex {0..}) Ex"
- unfolding fun_rel_def ZN_def Bex_def atLeast_iff
+ unfolding rel_fun_def ZN_def Bex_def atLeast_iff
by (metis zero_le_imp_eq_int zero_zle_int)
lemma ZN_le [transfer_rule]: "(ZN ===> ZN ===> op =) (op \<le>) (op \<le>)"
- unfolding fun_rel_def ZN_def by simp
+ unfolding rel_fun_def ZN_def by simp
lemma ZN_less [transfer_rule]: "(ZN ===> ZN ===> op =) (op <) (op <)"
- unfolding fun_rel_def ZN_def by simp
+ unfolding rel_fun_def ZN_def by simp
lemma ZN_eq [transfer_rule]: "(ZN ===> ZN ===> op =) (op =) (op =)"
- unfolding fun_rel_def ZN_def by simp
+ unfolding rel_fun_def ZN_def by simp
lemma ZN_Suc [transfer_rule]: "(ZN ===> ZN) (\<lambda>x. x + 1) Suc"
- unfolding fun_rel_def ZN_def by simp
+ unfolding rel_fun_def ZN_def by simp
lemma ZN_numeral [transfer_rule]:
"(op = ===> ZN) numeral numeral"
- unfolding fun_rel_def ZN_def by simp
+ unfolding rel_fun_def ZN_def by simp
lemma ZN_dvd [transfer_rule]: "(ZN ===> ZN ===> op =) (op dvd) (op dvd)"
- unfolding fun_rel_def ZN_def by (simp add: zdvd_int)
+ unfolding rel_fun_def ZN_def by (simp add: zdvd_int)
lemma ZN_div [transfer_rule]: "(ZN ===> ZN ===> ZN) (op div) (op div)"
- unfolding fun_rel_def ZN_def by (simp add: zdiv_int)
+ unfolding rel_fun_def ZN_def by (simp add: zdiv_int)
lemma ZN_mod [transfer_rule]: "(ZN ===> ZN ===> ZN) (op mod) (op mod)"
- unfolding fun_rel_def ZN_def by (simp add: zmod_int)
+ unfolding rel_fun_def ZN_def by (simp add: zmod_int)
lemma ZN_gcd [transfer_rule]: "(ZN ===> ZN ===> ZN) gcd gcd"
- unfolding fun_rel_def ZN_def by (simp add: transfer_int_nat_gcd)
+ unfolding rel_fun_def ZN_def by (simp add: transfer_int_nat_gcd)
lemma ZN_atMost [transfer_rule]:
"(ZN ===> rel_set ZN) (atLeastAtMost 0) atMost"
- unfolding fun_rel_def ZN_def rel_set_def
+ unfolding rel_fun_def ZN_def rel_set_def
by (clarsimp simp add: Bex_def, arith)
lemma ZN_atLeastAtMost [transfer_rule]:
"(ZN ===> ZN ===> rel_set ZN) atLeastAtMost atLeastAtMost"
- unfolding fun_rel_def ZN_def rel_set_def
+ unfolding rel_fun_def ZN_def rel_set_def
by (clarsimp simp add: Bex_def, arith)
lemma ZN_setsum [transfer_rule]:
"bi_unique A \<Longrightarrow> ((A ===> ZN) ===> rel_set A ===> ZN) setsum setsum"
- apply (intro fun_relI)
+ apply (intro rel_funI)
apply (erule (1) bi_unique_rel_set_lemma)
- apply (simp add: setsum.reindex int_setsum ZN_def fun_rel_def)
+ apply (simp add: setsum.reindex int_setsum ZN_def rel_fun_def)
apply (rule setsum_cong2, simp)
done