Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/Transfer.thy
    Author:     Brian Huffman, TU Muenchen
    Author:     Ondrej Kuncar, TU Muenchen
*)

section \<open>Generic theorem transfer using relations\<close>

theory Transfer
imports Basic_BNF_LFPs Hilbert_Choice Metis
begin

subsection \<open>Relator for function space\<close>

bundle lifting_syntax
begin
  notation rel_fun  (infixr "===>" 55)
  notation map_fun  (infixr "--->" 55)
end

context includes lifting_syntax
begin

lemma rel_funD2:
  assumes "rel_fun A B f g" and "A x x"
  shows "B (f x) (g x)"
  using assms by (rule rel_funD)

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: rel_fun_def)

lemmas rel_fun_eq = fun.rel_eq

lemma rel_fun_eq_rel:
shows "rel_fun (=) R = (\f g. \x. R (f x) (g x))"
  by (simp add: rel_fun_def)

subsection \<open>Transfer method\<close>

text \<open>Explicit tag for relation membership allows for
  backward proof methods.\<close>

definition Rel :: "('a \ 'b \ bool) \ 'a \ 'b \ bool"
  where "Rel r \ r"

text \<open>Handling of equality relations\<close>

definition is_equality :: "('a \ 'a \ bool) \ bool"
  where "is_equality R \ R = (=)"

lemma is_equality_eq: "is_equality (=)"
  unfolding is_equality_def by simp

text \<open>Reverse implication for monotonicity rules\<close>

definition rev_implies where
  "rev_implies x y \ (y \ x)"

text \<open>Handling of meta-logic connectives\<close>

definition transfer_forall where
  "transfer_forall \ All"

definition transfer_implies where
  "transfer_implies \ (\)"

definition transfer_bforall :: "('a \ bool) \ ('a \ bool) \ bool"
  where "transfer_bforall \ (\P Q. \x. P x \ Q x)"

lemma transfer_forall_eq: "(\x. P x) \ Trueprop (transfer_forall (\x. P x))"
  unfolding atomize_all transfer_forall_def ..

lemma transfer_implies_eq: "(A \ B) \ Trueprop (transfer_implies A B)"
  unfolding atomize_imp transfer_implies_def ..

lemma transfer_bforall_unfold:
  "Trueprop (transfer_bforall P (\x. Q x)) \ (\x. P x \ Q x)"
  unfolding transfer_bforall_def atomize_imp atomize_all ..

lemma transfer_start: "\P; Rel (=) P Q\ \ Q"
  unfolding Rel_def by simp

lemma transfer_start': "\P; Rel (\) P Q\ \ Q"
  unfolding Rel_def by simp

lemma transfer_prover_start: "\x = x'; Rel R x' y\ \ Rel R x y"
  by simp

lemma untransfer_start: "\Q; Rel (=) P Q\ \ P"
  unfolding Rel_def by simp

lemma Rel_eq_refl: "Rel (=) x x"
  unfolding Rel_def ..

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 rel_fun_def by fast

lemma Rel_abs:
  assumes "\x y. Rel A x y \ Rel B (f x) (g y)"
  shows "Rel (A ===> B) (\x. f x) (\y. g y)"
  using assms unfolding Rel_def rel_fun_def by fast

subsection \<open>Predicates on relations, i.e. ``class constraints''\<close>

definition left_total :: "('a \ 'b \ bool) \ bool"
  where "left_total R \ (\x. \y. R x y)"

definition left_unique :: "('a \ 'b \ bool) \ bool"
  where "left_unique R \ (\x y z. R x z \ R y z \ x = y)"

definition right_total :: "('a \ 'b \ bool) \ bool"
  where "right_total R \ (\y. \x. R x y)"

definition right_unique :: "('a \ 'b \ bool) \ bool"
  where "right_unique R \ (\x y z. R x y \ R x z \ y = z)"

definition bi_total :: "('a \ 'b \ bool) \ bool"
  where "bi_total R \ (\x. \y. R x y) \ (\y. \x. R x y)"

definition bi_unique :: "('a \ 'b \ bool) \ bool"
  where "bi_unique R \
    (\<forall>x y z. R x y \<longrightarrow> R x z \<longrightarrow> y = z) \<and>
    (\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"

lemma left_unique_iff: "left_unique R \ (\z. \\<^sub>\\<^sub>1x. R x z)"
  unfolding Uniq_def left_unique_def by force

lemma left_uniqueI: "(\x y z. \ A x z; A y z \ \ x = y) \ left_unique A"
unfolding left_unique_def by blast

lemma left_uniqueD: "\ left_unique A; A x z; A y z \ \ x = y"
unfolding left_unique_def by blast

lemma left_totalI:
  "(\x. \y. R x y) \ left_total R"
unfolding left_total_def by blast

lemma left_totalE:
  assumes "left_total R"
  obtains "(\x. \y. R x y)"
using assms unfolding left_total_def by blast

lemma bi_uniqueDr: "\ bi_unique A; A x y; A x z \ \ y = z"
  by(simp add: bi_unique_def)

lemma bi_uniqueDl: "\ bi_unique A; A x y; A z y \ \ x = z"
  by(simp add: bi_unique_def)

lemma bi_unique_iff: "bi_unique R \ (\z. \\<^sub>\\<^sub>1x. R x z) \ (\z. \\<^sub>\\<^sub>1x. R z x)"
  unfolding Uniq_def bi_unique_def by force

lemma right_unique_iff: "right_unique R \ (\z. \\<^sub>\\<^sub>1x. R z x)"
  unfolding Uniq_def right_unique_def by force

lemma right_uniqueI: "(\x y z. \ A x y; A x z \ \ y = z) \ right_unique A"
unfolding right_unique_def by fast

lemma right_uniqueD: "\ right_unique A; A x y; A x z \ \ y = z"
unfolding right_unique_def by fast

lemma right_totalI: "(\y. \x. A x y) \ right_total A"
by(simp add: right_total_def)

lemma right_totalE:
  assumes "right_total A"
  obtains x where "A x y"
using assms by(auto simp add: right_total_def)

lemma right_total_alt_def2:
  "right_total R \ ((R ===> (\)) ===> (\)) All All" (is "?lhs = ?rhs")
proof
  assume ?lhs then show ?rhs
    unfolding right_total_def rel_fun_def by blast
next
  assume \<section>: ?rhs
  show ?lhs
    using \<section> [unfolded rel_fun_def, rule_format, of "\<lambda>x. True" "\<lambda>y. \<exists>x. R x y"]
    unfolding right_total_def by blast
qed

lemma right_unique_alt_def2:
  "right_unique R \ (R ===> R ===> (\)) (=) (=)"
  unfolding right_unique_def rel_fun_def by auto

lemma bi_total_alt_def2:
  "bi_total R \ ((R ===> (=)) ===> (=)) All All" (is "?lhs = ?rhs")
proof
  assume ?lhs then show ?rhs
    unfolding bi_total_def rel_fun_def by blast
next
  assume \<section>: ?rhs
  show ?lhs
    using \<section> [unfolded rel_fun_def, rule_format, of "\<lambda>x. \<exists>y. R x y" "\<lambda>y. True"]
    using \<section> [unfolded rel_fun_def, rule_format, of "\<lambda>x. True" "\<lambda>y. \<exists>x. R x y"]
    by (auto simp: bi_total_def)
qed

lemma bi_unique_alt_def2:
  "bi_unique R \ (R ===> R ===> (=)) (=) (=)"
  unfolding bi_unique_def rel_fun_def by auto

lemma [simp]:
  shows left_unique_conversep: "left_unique A\\ \ right_unique A"
    and right_unique_conversep: "right_unique A\\ \ left_unique A"
  by(auto simp add: left_unique_def right_unique_def)

lemma [simp]:
  shows left_total_conversep: "left_total A\\ \ right_total A"
    and right_total_conversep: "right_total A\\ \ left_total A"
  by(simp_all add: left_total_def right_total_def)

lemma bi_unique_conversep [simp]: "bi_unique R\\ = bi_unique R"
  by(auto simp add: bi_unique_def)

lemma bi_total_conversep [simp]: "bi_total R\\ = bi_total R"
  by(auto simp add: bi_total_def)

lemma right_unique_alt_def: "right_unique R = (conversep R OO R \ (=))" unfolding right_unique_def by blast
lemma left_unique_alt_def: "left_unique R = (R OO (conversep R) \ (=))" unfolding left_unique_def by blast

lemma right_total_alt_def: "right_total R = (conversep R OO R \ (=))" unfolding right_total_def by blast
lemma left_total_alt_def: "left_total R = (R OO conversep R \ (=))" unfolding left_total_def by blast

lemma bi_total_alt_def: "bi_total A = (left_total A \ right_total A)"
unfolding left_total_def right_total_def bi_total_def by blast

lemma bi_unique_alt_def: "bi_unique A = (left_unique A \ right_unique A)"
unfolding left_unique_def right_unique_def bi_unique_def by blast

lemma bi_totalI: "left_total R \ right_total R \ bi_total R"
unfolding bi_total_alt_def ..

lemma bi_uniqueI: "left_unique R \ right_unique R \ bi_unique R"
unfolding bi_unique_alt_def ..

end

lemma is_equality_lemma: "(\R. is_equality R \ PROP (P R)) \ PROP (P (=))"
  unfolding is_equality_def
proof (rule equal_intr_rule)
  show "(\R. R = (=) \ PROP P R) \ PROP P (=)"
    apply (drule meta_spec)
    apply (erule meta_mp [OF _ refl])
    done
qed simp

lemma Domainp_lemma: "(\R. Domainp T = R \ PROP (P R)) \ PROP (P (Domainp T))"
proof (rule equal_intr_rule)
  show "(\R. Domainp T = R \ PROP P R) \ PROP P (Domainp T)"
    apply (drule meta_spec)
    apply (erule meta_mp [OF _ refl])
    done
qed simp

ML_file \<open>Tools/Transfer/transfer.ML\<close>
declare refl [transfer_rule]

hide_const (open) Rel

context includes lifting_syntax
begin

text \<open>Handling of domains\<close>

lemma Domainp_iff: "Domainp T x \ (\y. T x y)"
  by auto

lemma Domainp_refl[transfer_domain_rule]:
  "Domainp T = Domainp T" ..

lemma Domain_eq_top[transfer_domain_rule]: "Domainp (=) = top" by auto

lemma Domainp_pred_fun_eq[relator_domain]:
  assumes "left_unique T"
  shows "Domainp (T ===> S) = pred_fun (Domainp T) (Domainp S)"   (is "?lhs = ?rhs")
proof (intro ext iffI)
  fix x
  assume "?lhs x"
  then show "?rhs x"
    using assms unfolding rel_fun_def pred_fun_def by blast
next
  fix x
  assume "?rhs x"
  then have "\g. \y xa. T xa y \ S (x xa) (g y)"
    using assms unfolding Domainp_iff left_unique_def  pred_fun_def
    by (intro choice) blast
  then show "?lhs x"
    by blast
qed

text \<open>Properties are preserved by relation composition.\<close>

lemma OO_def: "R OO S = (\x z. \y. R x y \ S y z)"
  by auto

lemma bi_total_OO: "\bi_total A; bi_total B\ \ bi_total (A OO B)"
  unfolding bi_total_def OO_def by fast

lemma bi_unique_OO: "\bi_unique A; bi_unique B\ \ bi_unique (A OO B)"
  unfolding bi_unique_def OO_def by blast

lemma right_total_OO:
  "\right_total A; right_total B\ \ right_total (A OO B)"
  unfolding right_total_def OO_def by fast

lemma right_unique_OO:
  "\right_unique A; right_unique B\ \ right_unique (A OO B)"
  unfolding right_unique_def OO_def by fast

lemma left_total_OO: "left_total R \ left_total S \ left_total (R OO S)"
  unfolding left_total_def OO_def by fast

lemma left_unique_OO: "left_unique R \ left_unique S \ left_unique (R OO S)"
  unfolding left_unique_def OO_def by blast

subsection \<open>Properties of relators\<close>

lemma left_total_eq[transfer_rule]: "left_total (=)"
  unfolding left_total_def by blast

lemma left_unique_eq[transfer_rule]: "left_unique (=)"
  unfolding left_unique_def by blast

lemma right_total_eq [transfer_rule]: "right_total (=)"
  unfolding right_total_def by simp

lemma right_unique_eq [transfer_rule]: "right_unique (=)"
  unfolding right_unique_def by simp

lemma bi_total_eq[transfer_rule]: "bi_total (=)"
  unfolding bi_total_def by simp

lemma bi_unique_eq[transfer_rule]: "bi_unique (=)"
  unfolding bi_unique_def by simp

lemma left_total_fun[transfer_rule]:
  assumes "left_unique A" "left_total B"
  shows "left_total (A ===> B)"
  unfolding left_total_def
proof
  fix f
  show "Ex ((A ===> B) f)"
    unfolding rel_fun_def
  proof (intro exI strip)
    fix x y
    assume A: "A x y"
    have "(THE x. A x y) = x"
      using A assms by (simp add: left_unique_def the_equality)
    then show "B (f x) (SOME z. B (f (THE x. A x y)) z)"
      using assms by (force simp: left_total_def intro: someI_ex)
  qed
qed

lemma left_unique_fun[transfer_rule]:
  "\left_total A; left_unique B\ \ left_unique (A ===> B)"
  unfolding left_total_def left_unique_def rel_fun_def
  by (clarify, rule ext, fast)

lemma right_total_fun [transfer_rule]:
  assumes "right_unique A" "right_total B"
  shows "right_total (A ===> B)"
  unfolding right_total_def
proof
  fix g
  show "\x. (A ===> B) x g"
    unfolding rel_fun_def
  proof (intro exI strip)
    fix x y
    assume A: "A x y"
    have "(THE y. A x y) = y"
      using A assms by (simp add: right_unique_def the_equality)
    then show "B (SOME z. B z (g (THE y. A x y))) (g y)"
      using assms by (force simp: right_total_def intro: someI_ex)
  qed
qed

lemma right_unique_fun [transfer_rule]:
  "\right_total A; right_unique B\ \ right_unique (A ===> B)"
  unfolding right_total_def right_unique_def rel_fun_def
  by (clarify, rule ext, fast)

lemma bi_total_fun[transfer_rule]:
  "\bi_unique A; bi_total B\ \ bi_total (A ===> B)"
  unfolding bi_unique_alt_def bi_total_alt_def
  by (blast intro: right_total_fun left_total_fun)

lemma bi_unique_fun[transfer_rule]:
  "\bi_total A; bi_unique B\ \ bi_unique (A ===> B)"
  unfolding bi_unique_alt_def bi_total_alt_def
  by (blast intro: right_unique_fun left_unique_fun)

end

lemma if_conn:
  "(if P \ Q then t else e) = (if P then if Q then t else e else e)"
  "(if P \ Q then t else e) = (if P then t else if Q then t else e)"
  "(if P \ Q then t else e) = (if P then if Q then t else e else t)"
  "(if \ P then t else e) = (if P then e else t)"
by auto

ML_file \<open>Tools/Transfer/transfer_bnf.ML\<close>
ML_file \<open>Tools/BNF/bnf_fp_rec_sugar_transfer.ML\<close>

declare pred_fun_def [simp]
declare rel_fun_eq [relator_eq]

(* Delete the automated generated rule from the bnf command;
  we have a more general rule (Domainp_pred_fun_eq) that subsumes it. *)
declare fun.Domainp_rel[relator_domain del]

subsection \<open>Transfer rules\<close>

context includes lifting_syntax
begin

lemma Domainp_forall_transfer [transfer_rule]:
  assumes "right_total A"
  shows "((A ===> (=)) ===> (=))
    (transfer_bforall (Domainp A)) transfer_forall"
  using assms unfolding right_total_def
  unfolding transfer_forall_def transfer_bforall_def rel_fun_def Domainp_iff
  by fast

text \<open>Transfer rules using implication instead of equality on booleans.\<close>

lemma transfer_forall_transfer [transfer_rule]:
  "bi_total A \ ((A ===> (=)) ===> (=)) transfer_forall transfer_forall"
  "right_total A \ ((A ===> (=)) ===> implies) transfer_forall transfer_forall"
  "right_total A \ ((A ===> implies) ===> implies) transfer_forall transfer_forall"
  "bi_total A \ ((A ===> (=)) ===> rev_implies) transfer_forall transfer_forall"
  "bi_total A \ ((A ===> rev_implies) ===> rev_implies) transfer_forall transfer_forall"
  unfolding transfer_forall_def rev_implies_def rel_fun_def right_total_def bi_total_def
  by fast+

lemma transfer_implies_transfer [transfer_rule]:
  "((=) ===> (=) ===> (=) ) transfer_implies transfer_implies"
  "(rev_implies ===> implies ===> implies ) transfer_implies transfer_implies"
  "(rev_implies ===> (=) ===> implies ) transfer_implies transfer_implies"
  "((=) ===> implies ===> implies ) transfer_implies transfer_implies"
  "((=) ===> (=) ===> implies ) transfer_implies transfer_implies"
  "(implies ===> rev_implies ===> rev_implies) transfer_implies transfer_implies"
  "(implies ===> (=) ===> rev_implies) transfer_implies transfer_implies"
  "((=) ===> rev_implies ===> rev_implies) transfer_implies transfer_implies"
  "((=) ===> (=) ===> rev_implies) transfer_implies transfer_implies"
  unfolding transfer_implies_def rev_implies_def rel_fun_def by auto

lemma eq_imp_transfer [transfer_rule]:
  "right_unique A \ (A ===> A ===> (\)) (=) (=)"
  unfolding right_unique_alt_def2 .

text \<open>Transfer rules using equality.\<close>

lemma left_unique_transfer [transfer_rule]:
  assumes "right_total A"
  assumes "right_total B"
  assumes "bi_unique A"
  shows "((A ===> B ===> (=)) ===> implies) left_unique left_unique"
  using assms unfolding left_unique_def right_total_def bi_unique_def rel_fun_def
  by metis

lemma eq_transfer [transfer_rule]:
  assumes "bi_unique A"
  shows "(A ===> A ===> (=)) (=) (=)"
  using assms unfolding bi_unique_def rel_fun_def by auto

lemma right_total_Ex_transfer[transfer_rule]:
  assumes "right_total A"
  shows "((A ===> (=)) ===> (=)) (Bex (Collect (Domainp A))) Ex"
  using assms unfolding right_total_def Bex_def rel_fun_def Domainp_iff
  by fast

lemma right_total_All_transfer[transfer_rule]:
  assumes "right_total A"
  shows "((A ===> (=)) ===> (=)) (Ball (Collect (Domainp A))) All"
  using assms unfolding right_total_def Ball_def rel_fun_def Domainp_iff
  by fast

context
  includes lifting_syntax
begin

lemma right_total_fun_eq_transfer:
  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"
  using assms unfolding bi_total_def rel_fun_def by fast

lemma Ex_transfer [transfer_rule]:
  assumes "bi_total A"
  shows "((A ===> (=)) ===> (=)) Ex Ex"
  using assms unfolding bi_total_def rel_fun_def by fast

lemma Ex1_parametric [transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "bi_total A"
  shows "((A ===> (=)) ===> (=)) Ex1 Ex1"
unfolding Ex1_def by transfer_prover

declare If_transfer [transfer_rule]

lemma Let_transfer [transfer_rule]: "(A ===> (A ===> B) ===> B) Let Let"
  unfolding rel_fun_def by simp

declare id_transfer [transfer_rule]

declare comp_transfer [transfer_rule]

lemma curry_transfer [transfer_rule]:
  "((rel_prod A B ===> C) ===> A ===> B ===> C) curry curry"
  unfolding curry_def by transfer_prover

lemma fun_upd_transfer [transfer_rule]:
  assumes [transfer_rule]: "bi_unique A"
  shows "((A ===> B) ===> A ===> B ===> A ===> B) fun_upd fun_upd"
  unfolding fun_upd_def  by transfer_prover

lemma case_nat_transfer [transfer_rule]:
  "(A ===> ((=) ===> A) ===> (=) ===> A) case_nat case_nat"
  unfolding rel_fun_def by (simp split: nat.split)

lemma rec_nat_transfer [transfer_rule]:
  "(A ===> ((=) ===> A ===> A) ===> (=) ===> A) rec_nat rec_nat"
  unfolding rel_fun_def by (clarsimp, rename_tac n, induct_tac n, simp_all)

lemma funpow_transfer [transfer_rule]:
  "((=) ===> (A ===> A) ===> (A ===> A)) compow compow"
  unfolding funpow_def by transfer_prover

lemma mono_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_total A"
  assumes [transfer_rule]: "(A ===> A ===> (=)) (\) (\)"
  assumes [transfer_rule]: "(B ===> B ===> (=)) (\) (\)"
  shows "((A ===> B) ===> (=)) mono mono"
unfolding mono_def by transfer_prover

lemma right_total_relcompp_transfer[transfer_rule]:
  assumes [transfer_rule]: "right_total B"
  shows "((A ===> B ===> (=)) ===> (B ===> C ===> (=)) ===> A ===> C ===> (=))
    (\<lambda>R S x z. \<exists>y\<in>Collect (Domainp B). R x y \<and> S y z) (OO)"
unfolding OO_def by transfer_prover

lemma relcompp_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_total B"
  shows "((A ===> B ===> (=)) ===> (B ===> C ===> (=)) ===> A ===> C ===> (=)) (OO) (OO)"
unfolding OO_def by transfer_prover

lemma right_total_Domainp_transfer[transfer_rule]:
  assumes [transfer_rule]: "right_total B"
  shows "((A ===> B ===> (=)) ===> A ===> (=)) (\T x. \y\Collect(Domainp B). T x y) Domainp"
apply(subst(2) Domainp_iff[abs_def]) by transfer_prover

lemma Domainp_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_total B"
  shows "((A ===> B ===> (=)) ===> A ===> (=)) Domainp Domainp"
unfolding Domainp_iff by transfer_prover

lemma reflp_transfer[transfer_rule]:
  "bi_total A \ ((A ===> A ===> (=)) ===> (=)) reflp reflp"
  "right_total A \ ((A ===> A ===> implies) ===> implies) reflp reflp"
  "right_total A \ ((A ===> A ===> (=)) ===> implies) reflp reflp"
  "bi_total A \ ((A ===> A ===> rev_implies) ===> rev_implies) reflp reflp"
  "bi_total A \ ((A ===> A ===> (=)) ===> rev_implies) reflp reflp"
unfolding reflp_def rev_implies_def bi_total_def right_total_def rel_fun_def
by fast+

lemma right_unique_transfer [transfer_rule]:
  "\ right_total A; right_total B; bi_unique B \
  \<Longrightarrow> ((A ===> B ===> (=)) ===> implies) right_unique right_unique"
unfolding right_unique_def right_total_def bi_unique_def rel_fun_def
by metis

lemma left_total_parametric [transfer_rule]:
  assumes [transfer_rule]: "bi_total A" "bi_total B"
  shows "((A ===> B ===> (=)) ===> (=)) left_total left_total"
unfolding left_total_def by transfer_prover

lemma right_total_parametric [transfer_rule]:
  assumes [transfer_rule]: "bi_total A" "bi_total B"
  shows "((A ===> B ===> (=)) ===> (=)) right_total right_total"
unfolding right_total_def by transfer_prover

lemma left_unique_parametric [transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "bi_total A" "bi_total B"
  shows "((A ===> B ===> (=)) ===> (=)) left_unique left_unique"
unfolding left_unique_def by transfer_prover

lemma prod_pred_parametric [transfer_rule]:
  "((A ===> (=)) ===> (B ===> (=)) ===> rel_prod A B ===> (=)) pred_prod pred_prod"
unfolding prod.pred_set Basic_BNFs.fsts_def Basic_BNFs.snds_def fstsp.simps sndsp.simps
by simp transfer_prover

lemma apfst_parametric [transfer_rule]:
  "((A ===> B) ===> rel_prod A C ===> rel_prod B C) apfst apfst"
unfolding apfst_def by transfer_prover

lemma rel_fun_eq_eq_onp: "((=) ===> eq_onp P) = eq_onp (\f. \x. P(f x))"
unfolding eq_onp_def rel_fun_def by auto

lemma rel_fun_eq_onp_rel:
  shows "((eq_onp R) ===> S) = (\f g. \x. R x \ S (f x) (g x))"
by (auto simp add: eq_onp_def rel_fun_def)

lemma eq_onp_transfer [transfer_rule]:
  assumes [transfer_rule]: "bi_unique A"
  shows "((A ===> (=)) ===> A ===> A ===> (=)) eq_onp eq_onp"
unfolding eq_onp_def by transfer_prover

lemma rtranclp_parametric [transfer_rule]:
  assumes "bi_unique A" "bi_total A"
  shows "((A ===> A ===> (=)) ===> A ===> A ===> (=)) rtranclp rtranclp"
proof(rule rel_funI iffI)+
  fix R :: "'a \ 'a \ bool" and R' x y x' y'
  assume R: "(A ===> A ===> (=)) R R'" and "A x x'"
  {
    assume "R\<^sup>*\<^sup>* x y" "A y y'"
    thus "R'\<^sup>*\<^sup>* x' y'"
    proof(induction arbitrary: y')
      case base
      with \<open>bi_unique A\<close> \<open>A x x'\<close> have "x' = y'" by(rule bi_uniqueDr)
      thus ?case by simp
    next
      case (step y z z')
      from \<open>bi_total A\<close> obtain y' where "A y y'" unfolding bi_total_def by blast
      hence "R'\<^sup>*\<^sup>* x' y'" by(rule step.IH)
      moreover from R \<open>A y y'\<close> \<open>A z z'\<close> \<open>R y z\<close>
      have "R' y' z'" by(auto dest: rel_funD)
      ultimately show ?case ..
    qed
  next
    assume "R'\<^sup>*\<^sup>* x' y'" "A y y'"
    thus "R\<^sup>*\<^sup>* x y"
    proof(induction arbitrary: y)
      case base
      with \<open>bi_unique A\<close> \<open>A x x'\<close> have "x = y" by(rule bi_uniqueDl)
      thus ?case by simp
    next
      case (step y' z' z)
      from \<open>bi_total A\<close> obtain y where "A y y'" unfolding bi_total_def by blast
      hence "R\<^sup>*\<^sup>* x y" by(rule step.IH)
      moreover from R \<open>A y y'\<close> \<open>A z z'\<close> \<open>R' y' z'\<close>
      have "R y z" by(auto dest: rel_funD)
      ultimately show ?case ..
    qed
  }
qed

lemma right_unique_parametric [transfer_rule]:
  assumes [transfer_rule]: "bi_total A" "bi_unique B" "bi_total B"
  shows "((A ===> B ===> (=)) ===> (=)) right_unique right_unique"
  unfolding right_unique_def by transfer_prover

lemma map_fun_parametric [transfer_rule]:
  "((A ===> B) ===> (C ===> D) ===> (B ===> C) ===> A ===> D) map_fun map_fun"
  unfolding map_fun_def by transfer_prover

end

subsection \<open>\<^const>\<open>of_bool\<close> and \<^const>\<open>of_nat\<close>\<close>

context
  includes lifting_syntax
begin

lemma transfer_rule_of_bool:
  \<open>((\<longleftrightarrow>) ===> (\<cong>)) of_bool of_bool\<close>
    if [transfer_rule]: \<open>0 \<cong> 0\<close> \<open>1 \<cong> 1\<close>
    for R :: \<open>'a::zero_neq_one \<Rightarrow> 'b::zero_neq_one \<Rightarrow> bool\<close>  (infix \<open>\<cong>\<close> 50)
  unfolding of_bool_def by transfer_prover

lemma transfer_rule_of_nat:
  "((=) ===> (\)) of_nat of_nat"
    if [transfer_rule]: \<open>0 \<cong> 0\<close> \<open>1 \<cong> 1\<close>
    \<open>((\<cong>) ===> (\<cong>) ===> (\<cong>)) (+) (+)\<close>
  for R :: \<open>'a::semiring_1 \<Rightarrow> 'b::semiring_1 \<Rightarrow> bool\<close>  (infix \<open>\<cong>\<close> 50)
  unfolding of_nat_def by transfer_prover

end

end

¤ Dauer der Verarbeitung: 0.29 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht 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.