products/sources/formale Sprachen/Java/openjdk-20-36_src/src/hotspot/os_cpu/bsd_x86/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Transfer_Int_Nat.thy   Sprache: Unknown

(*  Title:      HOL/ex/Transfer_Int_Nat.thy
    Author:     Brian Huffman, TU Muenchen
*)

section \<open>Using the transfer method between nat and int\<close>

theory Transfer_Int_Nat
imports Main
begin

subsection \<open>Correspondence relation\<close>

definition ZN :: "int \ nat \ bool"
  where "ZN = (\z n. z = of_nat n)"

subsection \<open>Transfer domain rules\<close>

lemma Domainp_ZN [transfer_domain_rule]: "Domainp ZN = (\x. x \ 0)"
  unfolding ZN_def Domainp_iff[abs_def] by (auto intro: zero_le_imp_eq_int)

subsection \<open>Transfer rules\<close>

context includes lifting_syntax
begin

lemma bi_unique_ZN [transfer_rule]: "bi_unique ZN"
  unfolding ZN_def bi_unique_def by simp

lemma right_total_ZN [transfer_rule]: "right_total ZN"
  unfolding ZN_def right_total_def by simp

lemma ZN_0 [transfer_rule]: "ZN 0 0"
  unfolding ZN_def by simp

lemma ZN_1 [transfer_rule]: "ZN 1 1"
  unfolding ZN_def by simp

lemma ZN_add [transfer_rule]: "(ZN ===> ZN ===> ZN) (+) (+)"
  unfolding rel_fun_def ZN_def by simp

lemma ZN_mult [transfer_rule]: "(ZN ===> ZN ===> ZN) ((*)) ((*))"
  unfolding rel_fun_def ZN_def by simp

definition tsub :: "int \ int \ int"
  where "tsub k l = max 0 (k - l)"

lemma ZN_diff [transfer_rule]: "(ZN ===> ZN ===> ZN) tsub (-)"
  unfolding rel_fun_def ZN_def by (auto simp add: of_nat_diff tsub_def)

lemma ZN_power [transfer_rule]: "(ZN ===> (=) ===> ZN) (^) (^)"
  unfolding rel_fun_def ZN_def by simp

lemma ZN_nat_id [transfer_rule]: "(ZN ===> (=)) nat id"
  unfolding rel_fun_def ZN_def by simp

lemma ZN_id_int [transfer_rule]: "(ZN ===> (=)) id int"
  unfolding rel_fun_def ZN_def by simp

lemma ZN_All [transfer_rule]:
  "((ZN ===> (=)) ===> (=)) (Ball {0..}) All"
  unfolding rel_fun_def ZN_def by (auto dest: zero_le_imp_eq_int)

lemma ZN_transfer_forall [transfer_rule]:
  "((ZN ===> (=)) ===> (=)) (transfer_bforall (\x. 0 \ x)) transfer_forall"
  unfolding transfer_forall_def transfer_bforall_def
  unfolding rel_fun_def ZN_def by (auto dest: zero_le_imp_eq_int)

lemma ZN_Ex [transfer_rule]: "((ZN ===> (=)) ===> (=)) (Bex {0..}) Ex"
  unfolding rel_fun_def ZN_def Bex_def atLeast_iff
  by (metis zero_le_imp_eq_int of_nat_0_le_iff)

lemma ZN_le [transfer_rule]: "(ZN ===> ZN ===> (=)) (\) (\)"
  unfolding rel_fun_def ZN_def by simp

lemma ZN_less [transfer_rule]: "(ZN ===> ZN ===> (=)) (<) (<)"
  unfolding rel_fun_def ZN_def by simp

lemma ZN_eq [transfer_rule]: "(ZN ===> ZN ===> (=)) (=) (=)"
  unfolding rel_fun_def ZN_def by simp

lemma ZN_Suc [transfer_rule]: "(ZN ===> ZN) (\x. x + 1) Suc"
  unfolding rel_fun_def ZN_def by simp

lemma ZN_numeral [transfer_rule]:
  "((=) ===> ZN) numeral numeral"
  unfolding rel_fun_def ZN_def by simp

lemma ZN_dvd [transfer_rule]: "(ZN ===> ZN ===> (=)) (dvd) (dvd)"
  unfolding rel_fun_def ZN_def by simp

lemma ZN_div [transfer_rule]: "(ZN ===> ZN ===> ZN) (div) (div)"
  unfolding rel_fun_def ZN_def by (simp add: zdiv_int)

lemma ZN_mod [transfer_rule]: "(ZN ===> ZN ===> ZN) (mod) (mod)"
  unfolding rel_fun_def ZN_def by (simp add: zmod_int)

lemma ZN_gcd [transfer_rule]: "(ZN ===> ZN ===> ZN) gcd gcd"
  unfolding rel_fun_def ZN_def by (simp add: gcd_int_def)

lemma ZN_atMost [transfer_rule]:
  "(ZN ===> rel_set ZN) (atLeastAtMost 0) atMost"
  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 rel_fun_def ZN_def rel_set_def
  by (clarsimp simp add: Bex_def, arith)

lemma ZN_sum [transfer_rule]:
  "bi_unique A \ ((A ===> ZN) ===> rel_set A ===> ZN) sum sum"
  apply (intro rel_funI)
  apply (erule (1) bi_unique_rel_set_lemma)
  apply (simp add: sum.reindex int_sum ZN_def rel_fun_def)
  apply (rule sum.cong)
  apply simp_all
  done

text \<open>For derived operations, we can use the \<open>transfer_prover\<close>
  method to help generate transfer rules.\<close>

lemma ZN_sum_list [transfer_rule]: "(list_all2 ZN ===> ZN) sum_list sum_list"
  by transfer_prover

end

subsection \<open>Transfer examples\<close>

lemma
  assumes "\i::int. 0 \ i \ i + 0 = i"
  shows "\i::nat. i + 0 = i"
apply transfer
apply fact
done

lemma
  assumes "\i k::int. \0 \ i; 0 \ k; i < k\ \ \j\{0..}. i + j = k"
  shows "\i k::nat. i < k \ \j. i + j = k"
apply transfer
apply fact
done

lemma
  assumes "\x\{0::int..}. \y\{0..}. x * y div y = x"
  shows "\x y :: nat. x * y div y = x"
apply transfer
apply fact
done

lemma
  assumes "\m n::int. \0 \ m; 0 \ n; m * n = 0\ \ m = 0 \ n = 0"
  shows "m * n = (0::nat) \ m = 0 \ n = 0"
apply transfer
apply fact
done

lemma
  assumes "\x\{0::int..}. \y\{0..}. \z\{0..}. x + 3 * y = 5 * z"
  shows "\x::nat. \y z. x + 3 * y = 5 * z"
apply transfer
apply fact
done

text \<open>The \<open>fixing\<close> option prevents generalization over the free
  variable \<open>n\<close>, allowing the local transfer rule to be used.\<close>

lemma
  assumes [transfer_rule]: "ZN x n"
  assumes "\i\{0..}. i < x \ 2 * i < 3 * x"
  shows "\i. i < n \ 2 * i < 3 * n"
apply (transfer fixing: n)
apply fact
done

lemma
  assumes "gcd (2^i) (3^j) = (1::int)"
  shows "gcd (2^i) (3^j) = (1::nat)"
apply (transfer fixing: i j)
apply fact
done

lemma
  assumes "\x y z::int. \0 \ x; 0 \ y; 0 \ z\ \
    sum_list [x, y, z] = 0 \<longleftrightarrow> list_all (\<lambda>x. x = 0) [x, y, z]"
  shows "sum_list [x, y, z] = (0::nat) \ list_all (\x. x = 0) [x, y, z]"
apply transfer
apply fact
done

text \<open>Quantifiers over higher types (e.g. \<open>nat list\<close>) are
  transferred to a readable formula thanks to the transfer domain rule @{thm Domainp_ZN}\<close>

lemma
  assumes "\xs::int list. list_all (\x. x \ 0) xs \
    (sum_list xs = 0) = list_all (\<lambda>x. x = 0) xs"
  shows "sum_list xs = (0::nat) \ list_all (\x. x = 0) xs"
apply transfer
apply fact
done

text \<open>Equality on a higher type can be transferred if the relations
  involved are bi-unique.\<close>

lemma
  assumes "\xs::int list. \list_all (\x. x \ 0) xs; xs \ []\ \
    sum_list xs < sum_list (map (\<lambda>x. x + 1) xs)"
  shows "xs \ [] \ sum_list xs < sum_list (map Suc xs)"
apply transfer
apply fact
done

end

[ Dauer der Verarbeitung: 0.31 Sekunden  (vorverarbeitet)  ]