--- a/src/HOL/Code_Numeral.thy Tue Oct 22 19:07:12 2019 +0000
+++ b/src/HOL/Code_Numeral.thy Wed Oct 23 16:09:23 2019 +0000
@@ -77,38 +77,45 @@
instance integer :: Rings.dvd ..
-lemma [transfer_rule]:
- "rel_fun pcr_integer (rel_fun pcr_integer HOL.iff) Rings.dvd Rings.dvd"
- unfolding dvd_def by transfer_prover
+context
+ includes lifting_syntax
+ notes transfer_rule_numeral [transfer_rule]
+begin
lemma [transfer_rule]:
- "rel_fun (=) pcr_integer (of_bool :: bool \<Rightarrow> int) (of_bool :: bool \<Rightarrow> integer)"
+ "(pcr_integer ===> pcr_integer ===> (\<longleftrightarrow>)) (dvd) (dvd)"
+ by (unfold dvd_def) transfer_prover
+
+lemma [transfer_rule]:
+ "((\<longleftrightarrow>) ===> pcr_integer) of_bool of_bool"
by (unfold of_bool_def [abs_def]) transfer_prover
lemma [transfer_rule]:
- "rel_fun (=) pcr_integer (of_nat :: nat \<Rightarrow> int) (of_nat :: nat \<Rightarrow> integer)"
+ "((=) ===> pcr_integer) int of_nat"
by (rule transfer_rule_of_nat) transfer_prover+
lemma [transfer_rule]:
- "rel_fun (=) pcr_integer (\<lambda>k :: int. k :: int) (of_int :: int \<Rightarrow> integer)"
+ "((=) ===> pcr_integer) (\<lambda>k. k) of_int"
proof -
- have "rel_fun HOL.eq pcr_integer (of_int :: int \<Rightarrow> int) (of_int :: int \<Rightarrow> integer)"
+ have "((=) ===> pcr_integer) of_int of_int"
by (rule transfer_rule_of_int) transfer_prover+
then show ?thesis by (simp add: id_def)
qed
lemma [transfer_rule]:
- "rel_fun HOL.eq pcr_integer (numeral :: num \<Rightarrow> int) (numeral :: num \<Rightarrow> integer)"
- by (rule transfer_rule_numeral) transfer_prover+
+ "((=) ===> pcr_integer) numeral numeral"
+ by transfer_prover
lemma [transfer_rule]:
- "rel_fun HOL.eq (rel_fun HOL.eq pcr_integer) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> int) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> integer)"
+ "((=) ===> (=) ===> pcr_integer) Num.sub Num.sub"
by (unfold Num.sub_def [abs_def]) transfer_prover
lemma [transfer_rule]:
- "rel_fun pcr_integer (rel_fun (=) pcr_integer) (power :: _ \<Rightarrow> _ \<Rightarrow> int) (power :: _ \<Rightarrow> _ \<Rightarrow> integer)"
+ "(pcr_integer ===> (=) ===> pcr_integer) (^) (^)"
by (unfold power_def [abs_def]) transfer_prover
+end
+
lemma int_of_integer_of_nat [simp]:
"int_of_integer (of_nat n) = of_nat n"
by transfer rule
--- a/src/HOL/Filter.thy Tue Oct 22 19:07:12 2019 +0000
+++ b/src/HOL/Filter.thy Wed Oct 23 16:09:23 2019 +0000
@@ -1903,7 +1903,11 @@
end
-lemma prod_filter_parametric [transfer_rule]: includes lifting_syntax shows
+context
+ includes lifting_syntax
+begin
+
+lemma prod_filter_parametric [transfer_rule]:
"(rel_filter R ===> rel_filter S ===> rel_filter (rel_prod R S)) prod_filter prod_filter"
proof(intro rel_funI; elim rel_filter.cases; hypsubst)
fix F G
@@ -1947,6 +1951,9 @@
qed
qed
+end
+
+
text \<open>Code generation for filters\<close>
definition abstract_filter :: "(unit \<Rightarrow> 'a filter) \<Rightarrow> 'a filter"
--- a/src/HOL/Groups_List.thy Tue Oct 22 19:07:12 2019 +0000
+++ b/src/HOL/Groups_List.thy Wed Oct 23 16:09:23 2019 +0000
@@ -367,14 +367,18 @@
"sum f (set [m..<n]) = sum_list (map f [m..<n])"
by (simp add: interv_sum_list_conv_sum_set_nat)
-lemma sum_list_transfer[transfer_rule]:
+context
includes lifting_syntax
- assumes [transfer_rule]: "A 0 0"
- assumes [transfer_rule]: "(A ===> A ===> A) (+) (+)"
- shows "(list_all2 A ===> A) sum_list sum_list"
+begin
+
+lemma sum_list_transfer [transfer_rule]:
+ "(list_all2 A ===> A) sum_list sum_list"
+ if [transfer_rule]: "A 0 0" "(A ===> A ===> A) (+) (+)"
unfolding sum_list.eq_foldr [abs_def]
by transfer_prover
+end
+
subsection \<open>List product\<close>
--- a/src/HOL/Int.thy Tue Oct 22 19:07:12 2019 +0000
+++ b/src/HOL/Int.thy Wed Oct 23 16:09:23 2019 +0000
@@ -74,7 +74,9 @@
lemma int_def: "int n = Abs_Integ (n, 0)"
by (induct n) (simp add: zero_int.abs_eq, simp add: one_int.abs_eq plus_int.abs_eq)
-lemma int_transfer [transfer_rule]: "(rel_fun (=) pcr_int) (\<lambda>n. (n, 0)) int"
+lemma int_transfer [transfer_rule]:
+ includes lifting_syntax
+ shows "rel_fun (=) pcr_int (\<lambda>n. (n, 0)) int"
by (simp add: rel_fun_def int.pcr_cr_eq cr_int_def int_def)
lemma int_diff_cases: obtains (diff) m n where "z = int m - int n"
@@ -1197,14 +1199,16 @@
end
lemma transfer_rule_of_int:
+ includes lifting_syntax
fixes R :: "'a::ring_1 \<Rightarrow> 'b::ring_1 \<Rightarrow> bool"
assumes [transfer_rule]: "R 0 0" "R 1 1"
- "rel_fun R (rel_fun R R) plus plus"
- "rel_fun R R uminus uminus"
- shows "rel_fun HOL.eq R of_int of_int"
+ "(R ===> R ===> R) (+) (+)"
+ "(R ===> R) uminus uminus"
+ shows "((=) ===> R) of_int of_int"
proof -
+ note assms
note transfer_rule_of_nat [transfer_rule]
- have [transfer_rule]: "rel_fun HOL.eq R of_nat of_nat"
+ have [transfer_rule]: "((=) ===> R) of_nat of_nat"
by transfer_prover
show ?thesis
by (unfold of_int_of_nat [abs_def]) transfer_prover
--- a/src/HOL/Lifting_Set.thy Tue Oct 22 19:07:12 2019 +0000
+++ b/src/HOL/Lifting_Set.thy Wed Oct 23 16:09:23 2019 +0000
@@ -215,12 +215,17 @@
shows "(rel_set A ===> rel_set A ===> (=)) (\<subseteq>) (\<subseteq>)"
unfolding subset_eq [abs_def] by transfer_prover
+context
+ includes lifting_syntax
+begin
+
lemma strict_subset_transfer [transfer_rule]:
- includes lifting_syntax
assumes [transfer_rule]: "bi_unique A"
shows "(rel_set A ===> rel_set A ===> (=)) (\<subset>) (\<subset>)"
unfolding subset_not_subset_eq by transfer_prover
+end
+
declare right_total_UNIV_transfer[transfer_rule]
lemma UNIV_transfer [transfer_rule]:
@@ -265,8 +270,11 @@
by (rule rel_funI, erule (1) bi_unique_rel_set_lemma)
(simp add: card_image)
+context
+ includes lifting_syntax
+begin
+
lemma vimage_right_total_transfer[transfer_rule]:
- includes lifting_syntax
assumes [transfer_rule]: "bi_unique B" "right_total A"
shows "((A ===> B) ===> rel_set B ===> rel_set A) (\<lambda>f X. f -` X \<inter> Collect (Domainp A)) vimage"
proof -
@@ -279,6 +287,8 @@
finally show ?thesis .
qed
+end
+
lemma vimage_parametric [transfer_rule]:
assumes [transfer_rule]: "bi_total A" "bi_unique B"
shows "((A ===> B) ===> rel_set B ===> rel_set A) vimage vimage"
--- a/src/HOL/Num.thy Tue Oct 22 19:07:12 2019 +0000
+++ b/src/HOL/Num.thy Wed Oct 23 16:09:23 2019 +0000
@@ -549,15 +549,23 @@
end
+context
+ includes lifting_syntax
+begin
+
lemma transfer_rule_numeral:
- fixes R :: "'a::semiring_1 \<Rightarrow> 'b::semiring_1 \<Rightarrow> bool"
- assumes [transfer_rule]: "R 0 0" "R 1 1"
- "rel_fun R (rel_fun R R) plus plus"
- shows "rel_fun HOL.eq R numeral numeral"
- apply (subst (2) numeral_unfold_funpow [abs_def])
- apply (subst (1) numeral_unfold_funpow [abs_def])
- apply transfer_prover
- done
+ "((=) ===> R) numeral numeral"
+ if [transfer_rule]: "R 0 0" "R 1 1"
+ "(R ===> R ===> R) (+) (+)"
+ for R :: "'a::semiring_1 \<Rightarrow> 'b::semiring_1 \<Rightarrow> bool"
+proof -
+ have "((=) ===> R) (\<lambda>k. ((+) 1 ^^ numeral k) 0) (\<lambda>k. ((+) 1 ^^ numeral k) 0)"
+ by transfer_prover
+ then show ?thesis
+ by (simp flip: numeral_unfold_funpow [abs_def])
+qed
+
+end
lemma nat_of_num_numeral [code_abbrev]: "nat_of_num = numeral"
proof
--- a/src/HOL/Transfer.thy Tue Oct 22 19:07:12 2019 +0000
+++ b/src/HOL/Transfer.thy Wed Oct 23 16:09:23 2019 +0000
@@ -455,13 +455,18 @@
using assms unfolding right_total_def Ball_def rel_fun_def Domainp_iff[abs_def]
by fast
+context
+ includes lifting_syntax
+begin
+
lemma right_total_fun_eq_transfer:
- includes lifting_syntax
assumes [transfer_rule]: "right_total A" "bi_unique B"
shows "((A ===> B) ===> (A ===> B) ===> (=)) (\<lambda>f g. \<forall>x\<in>Collect(Domainp A). f x = g x) (=)"
unfolding fun_eq_iff
by transfer_prover
+end
+
lemma All_transfer [transfer_rule]:
assumes "bi_total A"
shows "((A ===> (=)) ===> (=)) All All"
--- a/src/HOL/ex/Word_Type.thy Tue Oct 22 19:07:12 2019 +0000
+++ b/src/HOL/ex/Word_Type.thy Wed Oct 23 16:09:23 2019 +0000
@@ -144,29 +144,31 @@
subsubsection \<open>Conversions\<close>
-lemma [transfer_rule]:
- "rel_fun HOL.eq (pcr_word :: int \<Rightarrow> 'a::len word \<Rightarrow> bool) numeral numeral"
-proof -
- note transfer_rule_numeral [transfer_rule]
- show ?thesis by transfer_prover
-qed
+context
+ includes lifting_syntax
+ notes transfer_rule_numeral [transfer_rule]
+ transfer_rule_of_nat [transfer_rule]
+ transfer_rule_of_int [transfer_rule]
+begin
lemma [transfer_rule]:
- "rel_fun HOL.eq pcr_word int of_nat"
-proof -
- note transfer_rule_of_nat [transfer_rule]
- show ?thesis by transfer_prover
-qed
+ "((=) ===> (pcr_word :: int \<Rightarrow> 'a::len word \<Rightarrow> bool)) numeral numeral"
+ by transfer_prover
+
+lemma [transfer_rule]:
+ "((=) ===> pcr_word) int of_nat"
+ by transfer_prover
lemma [transfer_rule]:
- "rel_fun HOL.eq pcr_word (\<lambda>k. k) of_int"
+ "((=) ===> pcr_word) (\<lambda>k. k) of_int"
proof -
- note transfer_rule_of_int [transfer_rule]
- have "rel_fun HOL.eq pcr_word (of_int :: int \<Rightarrow> int) (of_int :: int \<Rightarrow> 'a word)"
+ have "((=) ===> pcr_word) of_int of_int"
by transfer_prover
then show ?thesis by (simp add: id_def)
qed
+end
+
context semiring_1
begin
@@ -266,8 +268,12 @@
end
+context
+ includes lifting_syntax
+begin
+
lemma [transfer_rule]:
- "rel_fun pcr_word (\<longleftrightarrow>) even ((dvd) 2 :: 'a::len word \<Rightarrow> bool)"
+ "(pcr_word ===> (\<longleftrightarrow>)) even ((dvd) 2 :: 'a::len word \<Rightarrow> bool)"
proof -
have even_word_unfold: "even k \<longleftrightarrow> (\<exists>l. take_bit LENGTH('a) k = take_bit LENGTH('a) (2 * l))" (is "?P \<longleftrightarrow> ?Q")
for k :: int
@@ -287,6 +293,8 @@
transfer_prover
qed
+end
+
instance word :: (len) semiring_modulo
proof
show "a div b * b + a mod b = a" for a b :: "'a word"