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]: