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