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