# HG changeset patch
# User kuncar
# Date 1362745266 -3600
# Node ID d9e62d9c98dea221f6f3cdc530372dcf43dc656f
# Parent  84d01fd733cf055204fd313161530a7d15d57e06
patch Isabelle ditribution to conform to changes regarding the parametricity

diff -r 84d01fd733cf -r d9e62d9c98de src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Fri Mar 08 13:14:23 2013 +0100
+++ b/src/HOL/Code_Numeral.thy	Fri Mar 08 13:21:06 2013 +0100
@@ -76,31 +76,31 @@
 end
 
 lemma [transfer_rule]:
-  "fun_rel HOL.eq cr_integer (of_nat :: nat \<Rightarrow> int) (of_nat :: nat \<Rightarrow> integer)"
-  by (unfold of_nat_def [abs_def])  transfer_prover
+  "fun_rel HOL.eq pcr_integer (of_nat :: nat \<Rightarrow> int) (of_nat :: nat \<Rightarrow> integer)"
+  by (unfold of_nat_def [abs_def]) transfer_prover
 
 lemma [transfer_rule]:
-  "fun_rel HOL.eq cr_integer (\<lambda>k :: int. k :: int) (of_int :: int \<Rightarrow> integer)"
+  "fun_rel HOL.eq pcr_integer (\<lambda>k :: int. k :: int) (of_int :: int \<Rightarrow> integer)"
 proof -
-  have "fun_rel HOL.eq cr_integer (of_int :: int \<Rightarrow> int) (of_int :: int \<Rightarrow> integer)"
+  have "fun_rel HOL.eq pcr_integer (of_int :: int \<Rightarrow> int) (of_int :: int \<Rightarrow> integer)"
     by (unfold of_int_of_nat [abs_def]) transfer_prover
   then show ?thesis by (simp add: id_def)
 qed
 
 lemma [transfer_rule]:
-  "fun_rel HOL.eq cr_integer (numeral :: num \<Rightarrow> int) (numeral :: num \<Rightarrow> integer)"
+  "fun_rel HOL.eq pcr_integer (numeral :: num \<Rightarrow> int) (numeral :: num \<Rightarrow> integer)"
 proof -
-  have "fun_rel HOL.eq cr_integer (numeral :: num \<Rightarrow> int) (\<lambda>n. of_int (numeral n))"
+  have "fun_rel HOL.eq pcr_integer (numeral :: num \<Rightarrow> int) (\<lambda>n. of_int (numeral n))"
     by transfer_prover
   then show ?thesis by simp
 qed
 
 lemma [transfer_rule]:
-  "fun_rel HOL.eq cr_integer (neg_numeral :: num \<Rightarrow> int) (neg_numeral :: num \<Rightarrow> integer)"
+  "fun_rel HOL.eq pcr_integer (neg_numeral :: num \<Rightarrow> int) (neg_numeral :: num \<Rightarrow> integer)"
   by (unfold neg_numeral_def [abs_def]) transfer_prover
 
 lemma [transfer_rule]:
-  "fun_rel HOL.eq (fun_rel HOL.eq cr_integer) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> int) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> integer)"
+  "fun_rel HOL.eq (fun_rel HOL.eq pcr_integer) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> int) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> integer)"
   by (unfold Num.sub_def [abs_def]) transfer_prover
 
 lemma int_of_integer_of_nat [simp]:
@@ -200,11 +200,11 @@
 end
 
 lemma [transfer_rule]:
-  "fun_rel cr_integer (fun_rel cr_integer cr_integer) (min :: _ \<Rightarrow> _ \<Rightarrow> int) (min :: _ \<Rightarrow> _ \<Rightarrow> integer)"
+  "fun_rel pcr_integer (fun_rel pcr_integer pcr_integer) (min :: _ \<Rightarrow> _ \<Rightarrow> int) (min :: _ \<Rightarrow> _ \<Rightarrow> integer)"
   by (unfold min_def [abs_def]) transfer_prover
 
 lemma [transfer_rule]:
-  "fun_rel cr_integer (fun_rel cr_integer cr_integer) (max :: _ \<Rightarrow> _ \<Rightarrow> int) (max :: _ \<Rightarrow> _ \<Rightarrow> integer)"
+  "fun_rel pcr_integer (fun_rel pcr_integer pcr_integer) (max :: _ \<Rightarrow> _ \<Rightarrow> int) (max :: _ \<Rightarrow> _ \<Rightarrow> integer)"
   by (unfold max_def [abs_def]) transfer_prover
 
 lemma int_of_integer_min [simp]:
@@ -233,7 +233,7 @@
   [simp, code_abbrev]: "Pos = numeral"
 
 lemma [transfer_rule]:
-  "fun_rel HOL.eq cr_integer numeral Pos"
+  "fun_rel HOL.eq pcr_integer numeral Pos"
   by simp transfer_prover
 
 definition Neg :: "num \<Rightarrow> integer"
@@ -241,7 +241,7 @@
   [simp, code_abbrev]: "Neg = neg_numeral"
 
 lemma [transfer_rule]:
-  "fun_rel HOL.eq cr_integer neg_numeral Neg"
+  "fun_rel HOL.eq pcr_integer neg_numeral Neg"
   by simp transfer_prover
 
 code_datatype "0::integer" Pos Neg
@@ -686,17 +686,17 @@
 end
 
 lemma [transfer_rule]:
-  "fun_rel HOL.eq cr_natural (\<lambda>n::nat. n) (of_nat :: nat \<Rightarrow> natural)"
+  "fun_rel HOL.eq pcr_natural (\<lambda>n::nat. n) (of_nat :: nat \<Rightarrow> natural)"
 proof -
-  have "fun_rel HOL.eq cr_natural (of_nat :: nat \<Rightarrow> nat) (of_nat :: nat \<Rightarrow> natural)"
+  have "fun_rel HOL.eq pcr_natural (of_nat :: nat \<Rightarrow> nat) (of_nat :: nat \<Rightarrow> natural)"
     by (unfold of_nat_def [abs_def]) transfer_prover
   then show ?thesis by (simp add: id_def)
 qed
 
 lemma [transfer_rule]:
-  "fun_rel HOL.eq cr_natural (numeral :: num \<Rightarrow> nat) (numeral :: num \<Rightarrow> natural)"
+  "fun_rel HOL.eq pcr_natural (numeral :: num \<Rightarrow> nat) (numeral :: num \<Rightarrow> natural)"
 proof -
-  have "fun_rel HOL.eq cr_natural (numeral :: num \<Rightarrow> nat) (\<lambda>n. of_nat (numeral n))"
+  have "fun_rel HOL.eq pcr_natural (numeral :: num \<Rightarrow> nat) (\<lambda>n. of_nat (numeral n))"
     by transfer_prover
   then show ?thesis by simp
 qed
@@ -754,11 +754,11 @@
 end
 
 lemma [transfer_rule]:
-  "fun_rel cr_natural (fun_rel cr_natural cr_natural) (min :: _ \<Rightarrow> _ \<Rightarrow> nat) (min :: _ \<Rightarrow> _ \<Rightarrow> natural)"
+  "fun_rel pcr_natural (fun_rel pcr_natural pcr_natural) (min :: _ \<Rightarrow> _ \<Rightarrow> nat) (min :: _ \<Rightarrow> _ \<Rightarrow> natural)"
   by (unfold min_def [abs_def]) transfer_prover
 
 lemma [transfer_rule]:
-  "fun_rel cr_natural (fun_rel cr_natural cr_natural) (max :: _ \<Rightarrow> _ \<Rightarrow> nat) (max :: _ \<Rightarrow> _ \<Rightarrow> natural)"
+  "fun_rel pcr_natural (fun_rel pcr_natural pcr_natural) (max :: _ \<Rightarrow> _ \<Rightarrow> nat) (max :: _ \<Rightarrow> _ \<Rightarrow> natural)"
   by (unfold max_def [abs_def]) transfer_prover
 
 lemma nat_of_natural_min [simp]:
diff -r 84d01fd733cf -r d9e62d9c98de src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Fri Mar 08 13:14:23 2013 +0100
+++ b/src/HOL/Library/Float.thy	Fri Mar 08 13:21:06 2013 +0100
@@ -223,15 +223,15 @@
   done
 
 lemma transfer_numeral [transfer_rule]: 
-  "fun_rel (op =) cr_float (numeral :: _ \<Rightarrow> real) (numeral :: _ \<Rightarrow> float)"
-  unfolding fun_rel_def cr_float_def by simp
+  "fun_rel (op =) pcr_float (numeral :: _ \<Rightarrow> real) (numeral :: _ \<Rightarrow> float)"
+  unfolding fun_rel_def float.pcr_cr_eq  cr_float_def by simp
 
 lemma float_neg_numeral[simp]: "real (neg_numeral x :: float) = neg_numeral x"
   by (simp add: minus_numeral[symmetric] del: minus_numeral)
 
 lemma transfer_neg_numeral [transfer_rule]: 
-  "fun_rel (op =) cr_float (neg_numeral :: _ \<Rightarrow> real) (neg_numeral :: _ \<Rightarrow> float)"
-  unfolding fun_rel_def cr_float_def by simp
+  "fun_rel (op =) pcr_float (neg_numeral :: _ \<Rightarrow> real) (neg_numeral :: _ \<Rightarrow> float)"
+  unfolding fun_rel_def float.pcr_cr_eq cr_float_def by simp
 
 lemma
   shows float_of_numeral[simp]: "numeral k = float_of (numeral k)"
diff -r 84d01fd733cf -r d9e62d9c98de src/HOL/Library/Mapping.thy
--- a/src/HOL/Library/Mapping.thy	Fri Mar 08 13:14:23 2013 +0100
+++ b/src/HOL/Library/Mapping.thy	Fri Mar 08 13:21:06 2013 +0100
@@ -5,7 +5,7 @@
 header {* An abstract view on maps for code generation. *}
 
 theory Mapping
-imports Main Quotient_Option
+imports Main Quotient_Option Quotient_List
 begin
 
 subsection {* Type definition and primitive operations *}
@@ -81,7 +81,7 @@
 end
 
 lemma [transfer_rule]:
-  "fun_rel cr_mapping (fun_rel cr_mapping HOL.iff) HOL.eq HOL.equal"
+  "fun_rel (pcr_mapping op= op=) (fun_rel (pcr_mapping op= op=) HOL.iff) HOL.eq HOL.equal"
   by (unfold equal) transfer_prover
 
 
diff -r 84d01fd733cf -r d9e62d9c98de src/HOL/Library/RBT.thy
--- a/src/HOL/Library/RBT.thy	Fri Mar 08 13:14:23 2013 +0100
+++ b/src/HOL/Library/RBT.thy	Fri Mar 08 13:21:06 2013 +0100
@@ -5,7 +5,7 @@
 header {* Abstract type of RBT trees *}
 
 theory RBT 
-imports Main RBT_Impl
+imports Main RBT_Impl Quotient_List
 begin
 
 subsection {* Type definition *}
@@ -36,6 +36,7 @@
 subsection {* Primitive operations *}
 
 setup_lifting type_definition_rbt
+print_theorems
 
 lift_definition lookup :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" is "rbt_lookup" 
 by simp
@@ -61,7 +62,7 @@
 lift_definition map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is rbt_map_entry 
 by simp
 
-lift_definition map :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is RBT_Impl.map
+lift_definition map :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'c) rbt" is RBT_Impl.map
 by simp
 
 lift_definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c"  is RBT_Impl.fold 
diff -r 84d01fd733cf -r d9e62d9c98de src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Fri Mar 08 13:14:23 2013 +0100
+++ b/src/HOL/RealDef.thy	Fri Mar 08 13:21:06 2013 +0100
@@ -373,8 +373,8 @@
   morphisms rep_real Real
   by (rule part_equivp_realrel)
 
-lemma cr_real_eq: "cr_real = (\<lambda>x y. cauchy x \<and> Real x = y)"
-  unfolding cr_real_def realrel_def by simp
+lemma cr_real_eq: "pcr_real = (\<lambda>x y. cauchy x \<and> Real x = y)"
+  unfolding real.pcr_cr_eq cr_real_def realrel_def by auto
 
 lemma Real_induct [induct type: real]: (* TODO: generate automatically *)
   assumes "\<And>X. cauchy X \<Longrightarrow> P (Real X)" shows "P x"
@@ -387,14 +387,14 @@
 lemma eq_Real:
   "cauchy X \<Longrightarrow> cauchy Y \<Longrightarrow> Real X = Real Y \<longleftrightarrow> vanishes (\<lambda>n. X n - Y n)"
   using real.rel_eq_transfer
-  unfolding cr_real_def fun_rel_def realrel_def by simp
+  unfolding real.pcr_cr_eq cr_real_def fun_rel_def realrel_def by simp
 
 declare real.forall_transfer [transfer_rule del]
 
 lemma forall_real_transfer [transfer_rule]: (* TODO: generate automatically *)
-  "(fun_rel (fun_rel cr_real op =) op =)
+  "(fun_rel (fun_rel pcr_real op =) op =)
     (transfer_bforall cauchy) transfer_forall"
-  using Quotient_forall_transfer [OF Quotient_real]
+  using real.forall_transfer
   by (simp add: realrel_def)
 
 instantiation real :: field_inverse_zero
diff -r 84d01fd733cf -r d9e62d9c98de src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Fri Mar 08 13:14:23 2013 +0100
+++ b/src/HOL/Word/Word.thy	Fri Mar 08 13:21:06 2013 +0100
@@ -247,9 +247,9 @@
 text {* TODO: The next lemma could be generated automatically. *}
 
 lemma uint_transfer [transfer_rule]:
-  "(fun_rel cr_word op =) (bintrunc (len_of TYPE('a)))
+  "(fun_rel pcr_word op =) (bintrunc (len_of TYPE('a)))
     (uint :: 'a::len0 word \<Rightarrow> int)"
-  unfolding fun_rel_def cr_word_def by (simp add: word_ubin.eq_norm)
+  unfolding fun_rel_def word.pcr_cr_eq cr_word_def by (simp add: word_ubin.eq_norm)
 
 subsection  "Arithmetic operations"
 
@@ -599,9 +599,9 @@
 declare word_neg_numeral_alt [symmetric, code_abbrev]
 
 lemma word_numeral_transfer [transfer_rule]:
-  "(fun_rel op = cr_word) numeral numeral"
-  "(fun_rel op = cr_word) neg_numeral neg_numeral"
-  unfolding fun_rel_def cr_word_def word_numeral_alt word_neg_numeral_alt
+  "(fun_rel op = pcr_word) numeral numeral"
+  "(fun_rel op = pcr_word) neg_numeral neg_numeral"
+  unfolding fun_rel_def word.pcr_cr_eq cr_word_def word_numeral_alt word_neg_numeral_alt
   by simp_all
 
 lemma uint_bintrunc [simp]:
@@ -2194,9 +2194,9 @@
   by (simp add: word_ubin.eq_norm nth_bintr)
 
 lemma word_test_bit_transfer [transfer_rule]:
-  "(fun_rel cr_word (fun_rel op = op =))
+  "(fun_rel pcr_word (fun_rel op = op =))
     (\<lambda>x n. n < len_of TYPE('a) \<and> bin_nth x n) (test_bit :: 'a::len0 word \<Rightarrow> _)"
-  unfolding fun_rel_def cr_word_def by simp
+  unfolding fun_rel_def word.pcr_cr_eq cr_word_def by simp
 
 lemma word_ops_nth_size:
   "n < size (x::'a::len0 word) \<Longrightarrow>