Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Transfer_Int_Nat.thy Sprache: Isabelle

Original von: Isabelle^©

(*  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.16 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.