src/HOL/Code_Numeral.thy
changeset 55945 e96383acecf9
parent 55736 f1ed1e9cd080
child 56846 9df717fef2bb
     1.1 --- a/src/HOL/Code_Numeral.thy	Thu Mar 06 15:29:18 2014 +0100
     1.2 +++ b/src/HOL/Code_Numeral.thy	Thu Mar 06 15:40:33 2014 +0100
     1.3 @@ -76,27 +76,27 @@
     1.4  end
     1.5  
     1.6  lemma [transfer_rule]:
     1.7 -  "fun_rel HOL.eq pcr_integer (of_nat :: nat \<Rightarrow> int) (of_nat :: nat \<Rightarrow> integer)"
     1.8 +  "rel_fun HOL.eq pcr_integer (of_nat :: nat \<Rightarrow> int) (of_nat :: nat \<Rightarrow> integer)"
     1.9    by (unfold of_nat_def [abs_def]) transfer_prover
    1.10  
    1.11  lemma [transfer_rule]:
    1.12 -  "fun_rel HOL.eq pcr_integer (\<lambda>k :: int. k :: int) (of_int :: int \<Rightarrow> integer)"
    1.13 +  "rel_fun HOL.eq pcr_integer (\<lambda>k :: int. k :: int) (of_int :: int \<Rightarrow> integer)"
    1.14  proof -
    1.15 -  have "fun_rel HOL.eq pcr_integer (of_int :: int \<Rightarrow> int) (of_int :: int \<Rightarrow> integer)"
    1.16 +  have "rel_fun HOL.eq pcr_integer (of_int :: int \<Rightarrow> int) (of_int :: int \<Rightarrow> integer)"
    1.17      by (unfold of_int_of_nat [abs_def]) transfer_prover
    1.18    then show ?thesis by (simp add: id_def)
    1.19  qed
    1.20  
    1.21  lemma [transfer_rule]:
    1.22 -  "fun_rel HOL.eq pcr_integer (numeral :: num \<Rightarrow> int) (numeral :: num \<Rightarrow> integer)"
    1.23 +  "rel_fun HOL.eq pcr_integer (numeral :: num \<Rightarrow> int) (numeral :: num \<Rightarrow> integer)"
    1.24  proof -
    1.25 -  have "fun_rel HOL.eq pcr_integer (numeral :: num \<Rightarrow> int) (\<lambda>n. of_int (numeral n))"
    1.26 +  have "rel_fun HOL.eq pcr_integer (numeral :: num \<Rightarrow> int) (\<lambda>n. of_int (numeral n))"
    1.27      by transfer_prover
    1.28    then show ?thesis by simp
    1.29  qed
    1.30  
    1.31  lemma [transfer_rule]:
    1.32 -  "fun_rel HOL.eq (fun_rel HOL.eq pcr_integer) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> int) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> integer)"
    1.33 +  "rel_fun HOL.eq (rel_fun HOL.eq pcr_integer) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> int) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> integer)"
    1.34    by (unfold Num.sub_def [abs_def]) transfer_prover
    1.35  
    1.36  lemma int_of_integer_of_nat [simp]:
    1.37 @@ -192,11 +192,11 @@
    1.38  end
    1.39  
    1.40  lemma [transfer_rule]:
    1.41 -  "fun_rel pcr_integer (fun_rel pcr_integer pcr_integer) (min :: _ \<Rightarrow> _ \<Rightarrow> int) (min :: _ \<Rightarrow> _ \<Rightarrow> integer)"
    1.42 +  "rel_fun pcr_integer (rel_fun pcr_integer pcr_integer) (min :: _ \<Rightarrow> _ \<Rightarrow> int) (min :: _ \<Rightarrow> _ \<Rightarrow> integer)"
    1.43    by (unfold min_def [abs_def]) transfer_prover
    1.44  
    1.45  lemma [transfer_rule]:
    1.46 -  "fun_rel pcr_integer (fun_rel pcr_integer pcr_integer) (max :: _ \<Rightarrow> _ \<Rightarrow> int) (max :: _ \<Rightarrow> _ \<Rightarrow> integer)"
    1.47 +  "rel_fun pcr_integer (rel_fun pcr_integer pcr_integer) (max :: _ \<Rightarrow> _ \<Rightarrow> int) (max :: _ \<Rightarrow> _ \<Rightarrow> integer)"
    1.48    by (unfold max_def [abs_def]) transfer_prover
    1.49  
    1.50  lemma int_of_integer_min [simp]:
    1.51 @@ -249,7 +249,7 @@
    1.52    [simp, code_abbrev]: "Pos = numeral"
    1.53  
    1.54  lemma [transfer_rule]:
    1.55 -  "fun_rel HOL.eq pcr_integer numeral Pos"
    1.56 +  "rel_fun HOL.eq pcr_integer numeral Pos"
    1.57    by simp transfer_prover
    1.58  
    1.59  definition Neg :: "num \<Rightarrow> integer"
    1.60 @@ -257,7 +257,7 @@
    1.61    [simp, code_abbrev]: "Neg n = - Pos n"
    1.62  
    1.63  lemma [transfer_rule]:
    1.64 -  "fun_rel HOL.eq pcr_integer (\<lambda>n. - numeral n) Neg"
    1.65 +  "rel_fun HOL.eq pcr_integer (\<lambda>n. - numeral n) Neg"
    1.66    by (simp add: Neg_def [abs_def]) transfer_prover
    1.67  
    1.68  code_datatype "0::integer" Pos Neg
    1.69 @@ -680,17 +680,17 @@
    1.70  end
    1.71  
    1.72  lemma [transfer_rule]:
    1.73 -  "fun_rel HOL.eq pcr_natural (\<lambda>n::nat. n) (of_nat :: nat \<Rightarrow> natural)"
    1.74 +  "rel_fun HOL.eq pcr_natural (\<lambda>n::nat. n) (of_nat :: nat \<Rightarrow> natural)"
    1.75  proof -
    1.76 -  have "fun_rel HOL.eq pcr_natural (of_nat :: nat \<Rightarrow> nat) (of_nat :: nat \<Rightarrow> natural)"
    1.77 +  have "rel_fun HOL.eq pcr_natural (of_nat :: nat \<Rightarrow> nat) (of_nat :: nat \<Rightarrow> natural)"
    1.78      by (unfold of_nat_def [abs_def]) transfer_prover
    1.79    then show ?thesis by (simp add: id_def)
    1.80  qed
    1.81  
    1.82  lemma [transfer_rule]:
    1.83 -  "fun_rel HOL.eq pcr_natural (numeral :: num \<Rightarrow> nat) (numeral :: num \<Rightarrow> natural)"
    1.84 +  "rel_fun HOL.eq pcr_natural (numeral :: num \<Rightarrow> nat) (numeral :: num \<Rightarrow> natural)"
    1.85  proof -
    1.86 -  have "fun_rel HOL.eq pcr_natural (numeral :: num \<Rightarrow> nat) (\<lambda>n. of_nat (numeral n))"
    1.87 +  have "rel_fun HOL.eq pcr_natural (numeral :: num \<Rightarrow> nat) (\<lambda>n. of_nat (numeral n))"
    1.88      by transfer_prover
    1.89    then show ?thesis by simp
    1.90  qed
    1.91 @@ -748,11 +748,11 @@
    1.92  end
    1.93  
    1.94  lemma [transfer_rule]:
    1.95 -  "fun_rel pcr_natural (fun_rel pcr_natural pcr_natural) (min :: _ \<Rightarrow> _ \<Rightarrow> nat) (min :: _ \<Rightarrow> _ \<Rightarrow> natural)"
    1.96 +  "rel_fun pcr_natural (rel_fun pcr_natural pcr_natural) (min :: _ \<Rightarrow> _ \<Rightarrow> nat) (min :: _ \<Rightarrow> _ \<Rightarrow> natural)"
    1.97    by (unfold min_def [abs_def]) transfer_prover
    1.98  
    1.99  lemma [transfer_rule]:
   1.100 -  "fun_rel pcr_natural (fun_rel pcr_natural pcr_natural) (max :: _ \<Rightarrow> _ \<Rightarrow> nat) (max :: _ \<Rightarrow> _ \<Rightarrow> natural)"
   1.101 +  "rel_fun pcr_natural (rel_fun pcr_natural pcr_natural) (max :: _ \<Rightarrow> _ \<Rightarrow> nat) (max :: _ \<Rightarrow> _ \<Rightarrow> natural)"
   1.102    by (unfold max_def [abs_def]) transfer_prover
   1.103  
   1.104  lemma nat_of_natural_min [simp]: