# HG changeset patch # User haftmann # Date 1571846963 0 # Node ID cc204e10385ce9aa85aec10890f8bf1345de7fc8 # Parent b4564de51fa78c1786f5c067a3b7da4e970f0d56 tuned syntax diff -r b4564de51fa7 -r cc204e10385c src/HOL/Code_Numeral.thy --- 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 \ int) (of_bool :: bool \ integer)" + "(pcr_integer ===> pcr_integer ===> (\)) (dvd) (dvd)" + by (unfold dvd_def) transfer_prover + +lemma [transfer_rule]: + "((\) ===> 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 \ int) (of_nat :: nat \ integer)" + "((=) ===> pcr_integer) int of_nat" by (rule transfer_rule_of_nat) transfer_prover+ lemma [transfer_rule]: - "rel_fun (=) pcr_integer (\k :: int. k :: int) (of_int :: int \ integer)" + "((=) ===> pcr_integer) (\k. k) of_int" proof - - have "rel_fun HOL.eq pcr_integer (of_int :: int \ int) (of_int :: int \ 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 \ int) (numeral :: num \ 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 :: _ \ _ \ int) (Num.sub :: _ \ _ \ 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 :: _ \ _ \ int) (power :: _ \ _ \ 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 diff -r b4564de51fa7 -r cc204e10385c src/HOL/Filter.thy --- 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 \Code generation for filters\ definition abstract_filter :: "(unit \ 'a filter) \ 'a filter" diff -r b4564de51fa7 -r cc204e10385c src/HOL/Groups_List.thy --- 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.. 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 \List product\ diff -r b4564de51fa7 -r cc204e10385c src/HOL/Int.thy --- 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) (\n. (n, 0)) int" +lemma int_transfer [transfer_rule]: + includes lifting_syntax + shows "rel_fun (=) pcr_int (\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 \ 'b::ring_1 \ 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 diff -r b4564de51fa7 -r cc204e10385c src/HOL/Lifting_Set.thy --- 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 ===> (=)) (\) (\)" 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 ===> (=)) (\) (\)" 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) (\f X. f -` X \ 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" diff -r b4564de51fa7 -r cc204e10385c src/HOL/Num.thy --- 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 \ 'b::semiring_1 \ 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 \ 'b::semiring_1 \ bool" +proof - + have "((=) ===> R) (\k. ((+) 1 ^^ numeral k) 0) (\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 diff -r b4564de51fa7 -r cc204e10385c src/HOL/Transfer.thy --- 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) ===> (=)) (\f g. \x\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" diff -r b4564de51fa7 -r cc204e10385c src/HOL/ex/Word_Type.thy --- 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 \Conversions\ -lemma [transfer_rule]: - "rel_fun HOL.eq (pcr_word :: int \ 'a::len word \ 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 \ 'a::len word \ 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 (\k. k) of_int" + "((=) ===> pcr_word) (\k. k) of_int" proof - - note transfer_rule_of_int [transfer_rule] - have "rel_fun HOL.eq pcr_word (of_int :: int \ int) (of_int :: int \ '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 (\) even ((dvd) 2 :: 'a::len word \ bool)" + "(pcr_word ===> (\)) even ((dvd) 2 :: 'a::len word \ bool)" proof - have even_word_unfold: "even k \ (\l. take_bit LENGTH('a) k = take_bit LENGTH('a) (2 * l))" (is "?P \ ?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"