equal
deleted
inserted
replaced
72 |
72 |
73 instance proof |
73 instance proof |
74 qed (transfer, simp add: algebra_simps)+ |
74 qed (transfer, simp add: algebra_simps)+ |
75 |
75 |
76 end |
76 end |
|
77 |
|
78 instance integer :: Rings.dvd .. |
|
79 |
|
80 lemma [transfer_rule]: |
|
81 "rel_fun pcr_integer (rel_fun pcr_integer HOL.iff) Rings.dvd Rings.dvd" |
|
82 unfolding dvd_def by transfer_prover |
77 |
83 |
78 lemma [transfer_rule]: |
84 lemma [transfer_rule]: |
79 "rel_fun HOL.eq pcr_integer (of_nat :: nat \<Rightarrow> int) (of_nat :: nat \<Rightarrow> integer)" |
85 "rel_fun HOL.eq pcr_integer (of_nat :: nat \<Rightarrow> int) (of_nat :: nat \<Rightarrow> integer)" |
80 by (rule transfer_rule_of_nat) transfer_prover+ |
86 by (rule transfer_rule_of_nat) transfer_prover+ |
81 |
87 |
714 instance proof |
720 instance proof |
715 qed (transfer, simp add: algebra_simps)+ |
721 qed (transfer, simp add: algebra_simps)+ |
716 |
722 |
717 end |
723 end |
718 |
724 |
|
725 instance natural :: Rings.dvd .. |
|
726 |
|
727 lemma [transfer_rule]: |
|
728 "rel_fun pcr_natural (rel_fun pcr_natural HOL.iff) Rings.dvd Rings.dvd" |
|
729 unfolding dvd_def by transfer_prover |
|
730 |
719 lemma [transfer_rule]: |
731 lemma [transfer_rule]: |
720 "rel_fun HOL.eq pcr_natural (\<lambda>n::nat. n) (of_nat :: nat \<Rightarrow> natural)" |
732 "rel_fun HOL.eq pcr_natural (\<lambda>n::nat. n) (of_nat :: nat \<Rightarrow> natural)" |
721 proof - |
733 proof - |
722 have "rel_fun HOL.eq pcr_natural (of_nat :: nat \<Rightarrow> nat) (of_nat :: nat \<Rightarrow> natural)" |
734 have "rel_fun HOL.eq pcr_natural (of_nat :: nat \<Rightarrow> nat) (of_nat :: nat \<Rightarrow> natural)" |
723 by (unfold of_nat_def [abs_def]) transfer_prover |
735 by (unfold of_nat_def [abs_def]) transfer_prover |