src/HOL/Code_Numeral.thy
 changeset 51375 d9e62d9c98de parent 51143 0a2371e7ced3 child 52435 6646bb548c6b
```     1.1 --- a/src/HOL/Code_Numeral.thy	Fri Mar 08 13:14:23 2013 +0100
1.2 +++ b/src/HOL/Code_Numeral.thy	Fri Mar 08 13:21:06 2013 +0100
1.3 @@ -76,31 +76,31 @@
1.4  end
1.5
1.6  lemma [transfer_rule]:
1.7 -  "fun_rel HOL.eq cr_integer (of_nat :: nat \<Rightarrow> int) (of_nat :: nat \<Rightarrow> integer)"
1.8 -  by (unfold of_nat_def [abs_def])  transfer_prover
1.9 +  "fun_rel HOL.eq pcr_integer (of_nat :: nat \<Rightarrow> int) (of_nat :: nat \<Rightarrow> integer)"
1.10 +  by (unfold of_nat_def [abs_def]) transfer_prover
1.11
1.12  lemma [transfer_rule]:
1.13 -  "fun_rel HOL.eq cr_integer (\<lambda>k :: int. k :: int) (of_int :: int \<Rightarrow> integer)"
1.14 +  "fun_rel HOL.eq pcr_integer (\<lambda>k :: int. k :: int) (of_int :: int \<Rightarrow> integer)"
1.15  proof -
1.16 -  have "fun_rel HOL.eq cr_integer (of_int :: int \<Rightarrow> int) (of_int :: int \<Rightarrow> integer)"
1.17 +  have "fun_rel HOL.eq pcr_integer (of_int :: int \<Rightarrow> int) (of_int :: int \<Rightarrow> integer)"
1.18      by (unfold of_int_of_nat [abs_def]) transfer_prover
1.19    then show ?thesis by (simp add: id_def)
1.20  qed
1.21
1.22  lemma [transfer_rule]:
1.23 -  "fun_rel HOL.eq cr_integer (numeral :: num \<Rightarrow> int) (numeral :: num \<Rightarrow> integer)"
1.24 +  "fun_rel HOL.eq pcr_integer (numeral :: num \<Rightarrow> int) (numeral :: num \<Rightarrow> integer)"
1.25  proof -
1.26 -  have "fun_rel HOL.eq cr_integer (numeral :: num \<Rightarrow> int) (\<lambda>n. of_int (numeral n))"
1.27 +  have "fun_rel HOL.eq pcr_integer (numeral :: num \<Rightarrow> int) (\<lambda>n. of_int (numeral n))"
1.28      by transfer_prover
1.29    then show ?thesis by simp
1.30  qed
1.31
1.32  lemma [transfer_rule]:
1.33 -  "fun_rel HOL.eq cr_integer (neg_numeral :: num \<Rightarrow> int) (neg_numeral :: num \<Rightarrow> integer)"
1.34 +  "fun_rel HOL.eq pcr_integer (neg_numeral :: num \<Rightarrow> int) (neg_numeral :: num \<Rightarrow> integer)"
1.35    by (unfold neg_numeral_def [abs_def]) transfer_prover
1.36
1.37  lemma [transfer_rule]:
1.38 -  "fun_rel HOL.eq (fun_rel HOL.eq cr_integer) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> int) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> integer)"
1.39 +  "fun_rel HOL.eq (fun_rel HOL.eq pcr_integer) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> int) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> integer)"
1.40    by (unfold Num.sub_def [abs_def]) transfer_prover
1.41
1.42  lemma int_of_integer_of_nat [simp]:
1.43 @@ -200,11 +200,11 @@
1.44  end
1.45
1.46  lemma [transfer_rule]:
1.47 -  "fun_rel cr_integer (fun_rel cr_integer cr_integer) (min :: _ \<Rightarrow> _ \<Rightarrow> int) (min :: _ \<Rightarrow> _ \<Rightarrow> integer)"
1.48 +  "fun_rel pcr_integer (fun_rel pcr_integer pcr_integer) (min :: _ \<Rightarrow> _ \<Rightarrow> int) (min :: _ \<Rightarrow> _ \<Rightarrow> integer)"
1.49    by (unfold min_def [abs_def]) transfer_prover
1.50
1.51  lemma [transfer_rule]:
1.52 -  "fun_rel cr_integer (fun_rel cr_integer cr_integer) (max :: _ \<Rightarrow> _ \<Rightarrow> int) (max :: _ \<Rightarrow> _ \<Rightarrow> integer)"
1.53 +  "fun_rel pcr_integer (fun_rel pcr_integer pcr_integer) (max :: _ \<Rightarrow> _ \<Rightarrow> int) (max :: _ \<Rightarrow> _ \<Rightarrow> integer)"
1.54    by (unfold max_def [abs_def]) transfer_prover
1.55
1.56  lemma int_of_integer_min [simp]:
1.57 @@ -233,7 +233,7 @@
1.58    [simp, code_abbrev]: "Pos = numeral"
1.59
1.60  lemma [transfer_rule]:
1.61 -  "fun_rel HOL.eq cr_integer numeral Pos"
1.62 +  "fun_rel HOL.eq pcr_integer numeral Pos"
1.63    by simp transfer_prover
1.64
1.65  definition Neg :: "num \<Rightarrow> integer"
1.66 @@ -241,7 +241,7 @@
1.67    [simp, code_abbrev]: "Neg = neg_numeral"
1.68
1.69  lemma [transfer_rule]:
1.70 -  "fun_rel HOL.eq cr_integer neg_numeral Neg"
1.71 +  "fun_rel HOL.eq pcr_integer neg_numeral Neg"
1.72    by simp transfer_prover
1.73
1.74  code_datatype "0::integer" Pos Neg
1.75 @@ -686,17 +686,17 @@
1.76  end
1.77
1.78  lemma [transfer_rule]:
1.79 -  "fun_rel HOL.eq cr_natural (\<lambda>n::nat. n) (of_nat :: nat \<Rightarrow> natural)"
1.80 +  "fun_rel HOL.eq pcr_natural (\<lambda>n::nat. n) (of_nat :: nat \<Rightarrow> natural)"
1.81  proof -
1.82 -  have "fun_rel HOL.eq cr_natural (of_nat :: nat \<Rightarrow> nat) (of_nat :: nat \<Rightarrow> natural)"
1.83 +  have "fun_rel HOL.eq pcr_natural (of_nat :: nat \<Rightarrow> nat) (of_nat :: nat \<Rightarrow> natural)"
1.84      by (unfold of_nat_def [abs_def]) transfer_prover
1.85    then show ?thesis by (simp add: id_def)
1.86  qed
1.87
1.88  lemma [transfer_rule]:
1.89 -  "fun_rel HOL.eq cr_natural (numeral :: num \<Rightarrow> nat) (numeral :: num \<Rightarrow> natural)"
1.90 +  "fun_rel HOL.eq pcr_natural (numeral :: num \<Rightarrow> nat) (numeral :: num \<Rightarrow> natural)"
1.91  proof -
1.92 -  have "fun_rel HOL.eq cr_natural (numeral :: num \<Rightarrow> nat) (\<lambda>n. of_nat (numeral n))"
1.93 +  have "fun_rel HOL.eq pcr_natural (numeral :: num \<Rightarrow> nat) (\<lambda>n. of_nat (numeral n))"
1.94      by transfer_prover
1.95    then show ?thesis by simp
1.96  qed
1.97 @@ -754,11 +754,11 @@
1.98  end
1.99
1.100  lemma [transfer_rule]:
1.101 -  "fun_rel cr_natural (fun_rel cr_natural cr_natural) (min :: _ \<Rightarrow> _ \<Rightarrow> nat) (min :: _ \<Rightarrow> _ \<Rightarrow> natural)"
1.102 +  "fun_rel pcr_natural (fun_rel pcr_natural pcr_natural) (min :: _ \<Rightarrow> _ \<Rightarrow> nat) (min :: _ \<Rightarrow> _ \<Rightarrow> natural)"
1.103    by (unfold min_def [abs_def]) transfer_prover
1.104
1.105  lemma [transfer_rule]:
1.106 -  "fun_rel cr_natural (fun_rel cr_natural cr_natural) (max :: _ \<Rightarrow> _ \<Rightarrow> nat) (max :: _ \<Rightarrow> _ \<Rightarrow> natural)"
1.107 +  "fun_rel pcr_natural (fun_rel pcr_natural pcr_natural) (max :: _ \<Rightarrow> _ \<Rightarrow> nat) (max :: _ \<Rightarrow> _ \<Rightarrow> natural)"
1.108    by (unfold max_def [abs_def]) transfer_prover
1.109
1.110  lemma nat_of_natural_min [simp]:
```