patch Isabelle ditribution to conform to changes regarding the parametricity
authorkuncar
Fri Mar 08 13:21:06 2013 +0100 (2013-03-08)
changeset 51375d9e62d9c98de
parent 51374 84d01fd733cf
child 51376 8e38ff09864a
patch Isabelle ditribution to conform to changes regarding the parametricity
src/HOL/Code_Numeral.thy
src/HOL/Library/Float.thy
src/HOL/Library/Mapping.thy
src/HOL/Library/RBT.thy
src/HOL/RealDef.thy
src/HOL/Word/Word.thy
     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]:
     2.1 --- a/src/HOL/Library/Float.thy	Fri Mar 08 13:14:23 2013 +0100
     2.2 +++ b/src/HOL/Library/Float.thy	Fri Mar 08 13:21:06 2013 +0100
     2.3 @@ -223,15 +223,15 @@
     2.4    done
     2.5  
     2.6  lemma transfer_numeral [transfer_rule]: 
     2.7 -  "fun_rel (op =) cr_float (numeral :: _ \<Rightarrow> real) (numeral :: _ \<Rightarrow> float)"
     2.8 -  unfolding fun_rel_def cr_float_def by simp
     2.9 +  "fun_rel (op =) pcr_float (numeral :: _ \<Rightarrow> real) (numeral :: _ \<Rightarrow> float)"
    2.10 +  unfolding fun_rel_def float.pcr_cr_eq  cr_float_def by simp
    2.11  
    2.12  lemma float_neg_numeral[simp]: "real (neg_numeral x :: float) = neg_numeral x"
    2.13    by (simp add: minus_numeral[symmetric] del: minus_numeral)
    2.14  
    2.15  lemma transfer_neg_numeral [transfer_rule]: 
    2.16 -  "fun_rel (op =) cr_float (neg_numeral :: _ \<Rightarrow> real) (neg_numeral :: _ \<Rightarrow> float)"
    2.17 -  unfolding fun_rel_def cr_float_def by simp
    2.18 +  "fun_rel (op =) pcr_float (neg_numeral :: _ \<Rightarrow> real) (neg_numeral :: _ \<Rightarrow> float)"
    2.19 +  unfolding fun_rel_def float.pcr_cr_eq cr_float_def by simp
    2.20  
    2.21  lemma
    2.22    shows float_of_numeral[simp]: "numeral k = float_of (numeral k)"
     3.1 --- a/src/HOL/Library/Mapping.thy	Fri Mar 08 13:14:23 2013 +0100
     3.2 +++ b/src/HOL/Library/Mapping.thy	Fri Mar 08 13:21:06 2013 +0100
     3.3 @@ -5,7 +5,7 @@
     3.4  header {* An abstract view on maps for code generation. *}
     3.5  
     3.6  theory Mapping
     3.7 -imports Main Quotient_Option
     3.8 +imports Main Quotient_Option Quotient_List
     3.9  begin
    3.10  
    3.11  subsection {* Type definition and primitive operations *}
    3.12 @@ -81,7 +81,7 @@
    3.13  end
    3.14  
    3.15  lemma [transfer_rule]:
    3.16 -  "fun_rel cr_mapping (fun_rel cr_mapping HOL.iff) HOL.eq HOL.equal"
    3.17 +  "fun_rel (pcr_mapping op= op=) (fun_rel (pcr_mapping op= op=) HOL.iff) HOL.eq HOL.equal"
    3.18    by (unfold equal) transfer_prover
    3.19  
    3.20  
     4.1 --- a/src/HOL/Library/RBT.thy	Fri Mar 08 13:14:23 2013 +0100
     4.2 +++ b/src/HOL/Library/RBT.thy	Fri Mar 08 13:21:06 2013 +0100
     4.3 @@ -5,7 +5,7 @@
     4.4  header {* Abstract type of RBT trees *}
     4.5  
     4.6  theory RBT 
     4.7 -imports Main RBT_Impl
     4.8 +imports Main RBT_Impl Quotient_List
     4.9  begin
    4.10  
    4.11  subsection {* Type definition *}
    4.12 @@ -36,6 +36,7 @@
    4.13  subsection {* Primitive operations *}
    4.14  
    4.15  setup_lifting type_definition_rbt
    4.16 +print_theorems
    4.17  
    4.18  lift_definition lookup :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" is "rbt_lookup" 
    4.19  by simp
    4.20 @@ -61,7 +62,7 @@
    4.21  lift_definition map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is rbt_map_entry 
    4.22  by simp
    4.23  
    4.24 -lift_definition map :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is RBT_Impl.map
    4.25 +lift_definition map :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'c) rbt" is RBT_Impl.map
    4.26  by simp
    4.27  
    4.28  lift_definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c"  is RBT_Impl.fold 
     5.1 --- a/src/HOL/RealDef.thy	Fri Mar 08 13:14:23 2013 +0100
     5.2 +++ b/src/HOL/RealDef.thy	Fri Mar 08 13:21:06 2013 +0100
     5.3 @@ -373,8 +373,8 @@
     5.4    morphisms rep_real Real
     5.5    by (rule part_equivp_realrel)
     5.6  
     5.7 -lemma cr_real_eq: "cr_real = (\<lambda>x y. cauchy x \<and> Real x = y)"
     5.8 -  unfolding cr_real_def realrel_def by simp
     5.9 +lemma cr_real_eq: "pcr_real = (\<lambda>x y. cauchy x \<and> Real x = y)"
    5.10 +  unfolding real.pcr_cr_eq cr_real_def realrel_def by auto
    5.11  
    5.12  lemma Real_induct [induct type: real]: (* TODO: generate automatically *)
    5.13    assumes "\<And>X. cauchy X \<Longrightarrow> P (Real X)" shows "P x"
    5.14 @@ -387,14 +387,14 @@
    5.15  lemma eq_Real:
    5.16    "cauchy X \<Longrightarrow> cauchy Y \<Longrightarrow> Real X = Real Y \<longleftrightarrow> vanishes (\<lambda>n. X n - Y n)"
    5.17    using real.rel_eq_transfer
    5.18 -  unfolding cr_real_def fun_rel_def realrel_def by simp
    5.19 +  unfolding real.pcr_cr_eq cr_real_def fun_rel_def realrel_def by simp
    5.20  
    5.21  declare real.forall_transfer [transfer_rule del]
    5.22  
    5.23  lemma forall_real_transfer [transfer_rule]: (* TODO: generate automatically *)
    5.24 -  "(fun_rel (fun_rel cr_real op =) op =)
    5.25 +  "(fun_rel (fun_rel pcr_real op =) op =)
    5.26      (transfer_bforall cauchy) transfer_forall"
    5.27 -  using Quotient_forall_transfer [OF Quotient_real]
    5.28 +  using real.forall_transfer
    5.29    by (simp add: realrel_def)
    5.30  
    5.31  instantiation real :: field_inverse_zero
     6.1 --- a/src/HOL/Word/Word.thy	Fri Mar 08 13:14:23 2013 +0100
     6.2 +++ b/src/HOL/Word/Word.thy	Fri Mar 08 13:21:06 2013 +0100
     6.3 @@ -247,9 +247,9 @@
     6.4  text {* TODO: The next lemma could be generated automatically. *}
     6.5  
     6.6  lemma uint_transfer [transfer_rule]:
     6.7 -  "(fun_rel cr_word op =) (bintrunc (len_of TYPE('a)))
     6.8 +  "(fun_rel pcr_word op =) (bintrunc (len_of TYPE('a)))
     6.9      (uint :: 'a::len0 word \<Rightarrow> int)"
    6.10 -  unfolding fun_rel_def cr_word_def by (simp add: word_ubin.eq_norm)
    6.11 +  unfolding fun_rel_def word.pcr_cr_eq cr_word_def by (simp add: word_ubin.eq_norm)
    6.12  
    6.13  subsection  "Arithmetic operations"
    6.14  
    6.15 @@ -599,9 +599,9 @@
    6.16  declare word_neg_numeral_alt [symmetric, code_abbrev]
    6.17  
    6.18  lemma word_numeral_transfer [transfer_rule]:
    6.19 -  "(fun_rel op = cr_word) numeral numeral"
    6.20 -  "(fun_rel op = cr_word) neg_numeral neg_numeral"
    6.21 -  unfolding fun_rel_def cr_word_def word_numeral_alt word_neg_numeral_alt
    6.22 +  "(fun_rel op = pcr_word) numeral numeral"
    6.23 +  "(fun_rel op = pcr_word) neg_numeral neg_numeral"
    6.24 +  unfolding fun_rel_def word.pcr_cr_eq cr_word_def word_numeral_alt word_neg_numeral_alt
    6.25    by simp_all
    6.26  
    6.27  lemma uint_bintrunc [simp]:
    6.28 @@ -2194,9 +2194,9 @@
    6.29    by (simp add: word_ubin.eq_norm nth_bintr)
    6.30  
    6.31  lemma word_test_bit_transfer [transfer_rule]:
    6.32 -  "(fun_rel cr_word (fun_rel op = op =))
    6.33 +  "(fun_rel pcr_word (fun_rel op = op =))
    6.34      (\<lambda>x n. n < len_of TYPE('a) \<and> bin_nth x n) (test_bit :: 'a::len0 word \<Rightarrow> _)"
    6.35 -  unfolding fun_rel_def cr_word_def by simp
    6.36 +  unfolding fun_rel_def word.pcr_cr_eq cr_word_def by simp
    6.37  
    6.38  lemma word_ops_nth_size:
    6.39    "n < size (x::'a::len0 word) \<Longrightarrow>