1.1 --- a/NEWS Fri Aug 27 15:36:02 2010 +0200
1.2 +++ b/NEWS Fri Aug 27 19:34:23 2010 +0200
1.3 @@ -56,6 +56,10 @@
1.4
1.5 *** HOL ***
1.6
1.7 +* Renamed class eq and constant eq (for code generation) to class equal
1.8 +and constant equal, plus renaming of related facts and various tuning.
1.9 +INCOMPATIBILITY.
1.10 +
1.11 * Scala (2.8 or higher) has been added to the target languages of
1.12 the code generator.
1.13
2.1 --- a/doc-src/Codegen/Thy/Foundations.thy Fri Aug 27 15:36:02 2010 +0200
2.2 +++ b/doc-src/Codegen/Thy/Foundations.thy Fri Aug 27 19:34:23 2010 +0200
2.3 @@ -220,12 +220,12 @@
2.4 text {*
2.5 \noindent Obviously, polymorphic equality is implemented the Haskell
2.6 way using a type class. How is this achieved? HOL introduces an
2.7 - explicit class @{class eq} with a corresponding operation @{const
2.8 - eq_class.eq} such that @{thm eq [no_vars]}. The preprocessing
2.9 - framework does the rest by propagating the @{class eq} constraints
2.10 + explicit class @{class equal} with a corresponding operation @{const
2.11 + HOL.equal} such that @{thm equal [no_vars]}. The preprocessing
2.12 + framework does the rest by propagating the @{class equal} constraints
2.13 through all dependent code equations. For datatypes, instances of
2.14 - @{class eq} are implicitly derived when possible. For other types,
2.15 - you may instantiate @{text eq} manually like any other type class.
2.16 + @{class equal} are implicitly derived when possible. For other types,
2.17 + you may instantiate @{text equal} manually like any other type class.
2.18 *}
2.19
2.20
3.1 --- a/src/HOL/Code_Evaluation.thy Fri Aug 27 15:36:02 2010 +0200
3.2 +++ b/src/HOL/Code_Evaluation.thy Fri Aug 27 19:34:23 2010 +0200
3.3 @@ -162,7 +162,7 @@
3.4 subsubsection {* Code generator setup *}
3.5
3.6 lemmas [code del] = term.recs term.cases term.size
3.7 -lemma [code, code del]: "eq_class.eq (t1\<Colon>term) t2 \<longleftrightarrow> eq_class.eq t1 t2" ..
3.8 +lemma [code, code del]: "HOL.equal (t1\<Colon>term) t2 \<longleftrightarrow> HOL.equal t1 t2" ..
3.9
3.10 lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
3.11 lemma [code, code del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
4.1 --- a/src/HOL/Code_Numeral.thy Fri Aug 27 15:36:02 2010 +0200
4.2 +++ b/src/HOL/Code_Numeral.thy Fri Aug 27 19:34:23 2010 +0200
4.3 @@ -115,12 +115,12 @@
4.4 lemmas [code del] = code_numeral.recs code_numeral.cases
4.5
4.6 lemma [code]:
4.7 - "eq_class.eq k l \<longleftrightarrow> eq_class.eq (nat_of k) (nat_of l)"
4.8 - by (cases k, cases l) (simp add: eq)
4.9 + "HOL.equal k l \<longleftrightarrow> HOL.equal (nat_of k) (nat_of l)"
4.10 + by (cases k, cases l) (simp add: equal)
4.11
4.12 lemma [code nbe]:
4.13 - "eq_class.eq (k::code_numeral) k \<longleftrightarrow> True"
4.14 - by (rule HOL.eq_refl)
4.15 + "HOL.equal (k::code_numeral) k \<longleftrightarrow> True"
4.16 + by (rule equal_refl)
4.17
4.18
4.19 subsection {* Code numerals as datatype of ints *}
4.20 @@ -301,7 +301,7 @@
4.21 (Haskell "Integer")
4.22 (Scala "BigInt")
4.23
4.24 -code_instance code_numeral :: eq
4.25 +code_instance code_numeral :: equal
4.26 (Haskell -)
4.27
4.28 setup {*
4.29 @@ -342,7 +342,7 @@
4.30 (Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))")
4.31 (Eval "!(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
4.32
4.33 -code_const "eq_class.eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
4.34 +code_const "HOL.equal \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
4.35 (SML "!((_ : Int.int) = _)")
4.36 (OCaml "Big'_int.eq'_big'_int")
4.37 (Haskell infixl 4 "==")
5.1 --- a/src/HOL/HOL.thy Fri Aug 27 15:36:02 2010 +0200
5.2 +++ b/src/HOL/HOL.thy Fri Aug 27 19:34:23 2010 +0200
5.3 @@ -1775,31 +1775,30 @@
5.4
5.5 subsubsection {* Equality *}
5.6
5.7 -class eq =
5.8 - fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
5.9 - assumes eq_equals: "eq x y \<longleftrightarrow> x = y"
5.10 +class equal =
5.11 + fixes equal :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
5.12 + assumes equal_eq: "equal x y \<longleftrightarrow> x = y"
5.13 begin
5.14
5.15 -lemma eq [code_unfold, code_inline del]: "eq = (op =)"
5.16 - by (rule ext eq_equals)+
5.17 +lemma equal [code_unfold, code_inline del]: "equal = (op =)"
5.18 + by (rule ext equal_eq)+
5.19
5.20 -lemma eq_refl: "eq x x \<longleftrightarrow> True"
5.21 - unfolding eq by rule+
5.22 +lemma equal_refl: "equal x x \<longleftrightarrow> True"
5.23 + unfolding equal by rule+
5.24
5.25 -lemma equals_eq: "(op =) \<equiv> eq"
5.26 - by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals)
5.27 -
5.28 -declare equals_eq [symmetric, code_post]
5.29 +lemma eq_equal: "(op =) \<equiv> equal"
5.30 + by (rule eq_reflection) (rule ext, rule ext, rule sym, rule equal_eq)
5.31
5.32 end
5.33
5.34 -declare equals_eq [code]
5.35 +declare eq_equal [symmetric, code_post]
5.36 +declare eq_equal [code]
5.37
5.38 setup {*
5.39 Code_Preproc.map_pre (fn simpset =>
5.40 - simpset addsimprocs [Simplifier.simproc_global_i @{theory} "eq" [@{term "op ="}]
5.41 + simpset addsimprocs [Simplifier.simproc_global_i @{theory} "equal" [@{term "op ="}]
5.42 (fn thy => fn _ => fn Const (_, T) => case strip_type T
5.43 - of (Type _ :: _, _) => SOME @{thm equals_eq}
5.44 + of (Type _ :: _, _) => SOME @{thm eq_equal}
5.45 | _ => NONE)])
5.46 *}
5.47
5.48 @@ -1839,50 +1838,50 @@
5.49 and "(P \<longrightarrow> False) \<longleftrightarrow> \<not> P"
5.50 and "(P \<longrightarrow> True) \<longleftrightarrow> True" by simp_all
5.51
5.52 -instantiation itself :: (type) eq
5.53 +instantiation itself :: (type) equal
5.54 begin
5.55
5.56 -definition eq_itself :: "'a itself \<Rightarrow> 'a itself \<Rightarrow> bool" where
5.57 - "eq_itself x y \<longleftrightarrow> x = y"
5.58 +definition equal_itself :: "'a itself \<Rightarrow> 'a itself \<Rightarrow> bool" where
5.59 + "equal_itself x y \<longleftrightarrow> x = y"
5.60
5.61 instance proof
5.62 -qed (fact eq_itself_def)
5.63 +qed (fact equal_itself_def)
5.64
5.65 end
5.66
5.67 -lemma eq_itself_code [code]:
5.68 - "eq_class.eq TYPE('a) TYPE('a) \<longleftrightarrow> True"
5.69 - by (simp add: eq)
5.70 +lemma equal_itself_code [code]:
5.71 + "equal TYPE('a) TYPE('a) \<longleftrightarrow> True"
5.72 + by (simp add: equal)
5.73
5.74 text {* Equality *}
5.75
5.76 declare simp_thms(6) [code nbe]
5.77
5.78 setup {*
5.79 - Sign.add_const_constraint (@{const_name eq}, SOME @{typ "'a\<Colon>type \<Rightarrow> 'a \<Rightarrow> bool"})
5.80 + Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a\<Colon>type \<Rightarrow> 'a \<Rightarrow> bool"})
5.81 *}
5.82
5.83 -lemma equals_alias_cert: "OFCLASS('a, eq_class) \<equiv> ((op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool) \<equiv> eq)" (is "?ofclass \<equiv> ?eq")
5.84 +lemma equal_alias_cert: "OFCLASS('a, equal_class) \<equiv> ((op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool) \<equiv> equal)" (is "?ofclass \<equiv> ?equal")
5.85 proof
5.86 assume "PROP ?ofclass"
5.87 - show "PROP ?eq"
5.88 - by (tactic {* ALLGOALS (rtac (Thm.unconstrainT @{thm equals_eq})) *})
5.89 + show "PROP ?equal"
5.90 + by (tactic {* ALLGOALS (rtac (Thm.unconstrainT @{thm eq_equal})) *})
5.91 (fact `PROP ?ofclass`)
5.92 next
5.93 - assume "PROP ?eq"
5.94 + assume "PROP ?equal"
5.95 show "PROP ?ofclass" proof
5.96 - qed (simp add: `PROP ?eq`)
5.97 + qed (simp add: `PROP ?equal`)
5.98 qed
5.99
5.100 setup {*
5.101 - Sign.add_const_constraint (@{const_name eq}, SOME @{typ "'a\<Colon>eq \<Rightarrow> 'a \<Rightarrow> bool"})
5.102 + Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a\<Colon>equal \<Rightarrow> 'a \<Rightarrow> bool"})
5.103 *}
5.104
5.105 setup {*
5.106 - Nbe.add_const_alias @{thm equals_alias_cert}
5.107 + Nbe.add_const_alias @{thm equal_alias_cert}
5.108 *}
5.109
5.110 -hide_const (open) eq
5.111 +hide_const (open) equal
5.112
5.113 text {* Cases *}
5.114
5.115 @@ -1939,10 +1938,10 @@
5.116
5.117 text {* using built-in Haskell equality *}
5.118
5.119 -code_class eq
5.120 +code_class equal
5.121 (Haskell "Eq")
5.122
5.123 -code_const "eq_class.eq"
5.124 +code_const "HOL.equal"
5.125 (Haskell infixl 4 "==")
5.126
5.127 code_const "op ="
6.1 --- a/src/HOL/Int.thy Fri Aug 27 15:36:02 2010 +0200
6.2 +++ b/src/HOL/Int.thy Fri Aug 27 19:34:23 2010 +0200
6.3 @@ -2222,42 +2222,42 @@
6.4 mult_bin_simps
6.5 arith_extra_simps(4) [where 'a = int]
6.6
6.7 -instantiation int :: eq
6.8 +instantiation int :: equal
6.9 begin
6.10
6.11 definition
6.12 - "eq_class.eq k l \<longleftrightarrow> k - l = (0\<Colon>int)"
6.13 -
6.14 -instance by default (simp add: eq_int_def)
6.15 + "HOL.equal k l \<longleftrightarrow> k - l = (0\<Colon>int)"
6.16 +
6.17 +instance by default (simp add: equal_int_def)
6.18
6.19 end
6.20
6.21 lemma eq_number_of_int_code [code]:
6.22 - "eq_class.eq (number_of k \<Colon> int) (number_of l) \<longleftrightarrow> eq_class.eq k l"
6.23 - unfolding eq_int_def number_of_is_id ..
6.24 + "HOL.equal (number_of k \<Colon> int) (number_of l) \<longleftrightarrow> HOL.equal k l"
6.25 + unfolding equal_int_def number_of_is_id ..
6.26
6.27 lemma eq_int_code [code]:
6.28 - "eq_class.eq Int.Pls Int.Pls \<longleftrightarrow> True"
6.29 - "eq_class.eq Int.Pls Int.Min \<longleftrightarrow> False"
6.30 - "eq_class.eq Int.Pls (Int.Bit0 k2) \<longleftrightarrow> eq_class.eq Int.Pls k2"
6.31 - "eq_class.eq Int.Pls (Int.Bit1 k2) \<longleftrightarrow> False"
6.32 - "eq_class.eq Int.Min Int.Pls \<longleftrightarrow> False"
6.33 - "eq_class.eq Int.Min Int.Min \<longleftrightarrow> True"
6.34 - "eq_class.eq Int.Min (Int.Bit0 k2) \<longleftrightarrow> False"
6.35 - "eq_class.eq Int.Min (Int.Bit1 k2) \<longleftrightarrow> eq_class.eq Int.Min k2"
6.36 - "eq_class.eq (Int.Bit0 k1) Int.Pls \<longleftrightarrow> eq_class.eq k1 Int.Pls"
6.37 - "eq_class.eq (Int.Bit1 k1) Int.Pls \<longleftrightarrow> False"
6.38 - "eq_class.eq (Int.Bit0 k1) Int.Min \<longleftrightarrow> False"
6.39 - "eq_class.eq (Int.Bit1 k1) Int.Min \<longleftrightarrow> eq_class.eq k1 Int.Min"
6.40 - "eq_class.eq (Int.Bit0 k1) (Int.Bit0 k2) \<longleftrightarrow> eq_class.eq k1 k2"
6.41 - "eq_class.eq (Int.Bit0 k1) (Int.Bit1 k2) \<longleftrightarrow> False"
6.42 - "eq_class.eq (Int.Bit1 k1) (Int.Bit0 k2) \<longleftrightarrow> False"
6.43 - "eq_class.eq (Int.Bit1 k1) (Int.Bit1 k2) \<longleftrightarrow> eq_class.eq k1 k2"
6.44 - unfolding eq_equals by simp_all
6.45 + "HOL.equal Int.Pls Int.Pls \<longleftrightarrow> True"
6.46 + "HOL.equal Int.Pls Int.Min \<longleftrightarrow> False"
6.47 + "HOL.equal Int.Pls (Int.Bit0 k2) \<longleftrightarrow> HOL.equal Int.Pls k2"
6.48 + "HOL.equal Int.Pls (Int.Bit1 k2) \<longleftrightarrow> False"
6.49 + "HOL.equal Int.Min Int.Pls \<longleftrightarrow> False"
6.50 + "HOL.equal Int.Min Int.Min \<longleftrightarrow> True"
6.51 + "HOL.equal Int.Min (Int.Bit0 k2) \<longleftrightarrow> False"
6.52 + "HOL.equal Int.Min (Int.Bit1 k2) \<longleftrightarrow> HOL.equal Int.Min k2"
6.53 + "HOL.equal (Int.Bit0 k1) Int.Pls \<longleftrightarrow> HOL.equal k1 Int.Pls"
6.54 + "HOL.equal (Int.Bit1 k1) Int.Pls \<longleftrightarrow> False"
6.55 + "HOL.equal (Int.Bit0 k1) Int.Min \<longleftrightarrow> False"
6.56 + "HOL.equal (Int.Bit1 k1) Int.Min \<longleftrightarrow> HOL.equal k1 Int.Min"
6.57 + "HOL.equal (Int.Bit0 k1) (Int.Bit0 k2) \<longleftrightarrow> HOL.equal k1 k2"
6.58 + "HOL.equal (Int.Bit0 k1) (Int.Bit1 k2) \<longleftrightarrow> False"
6.59 + "HOL.equal (Int.Bit1 k1) (Int.Bit0 k2) \<longleftrightarrow> False"
6.60 + "HOL.equal (Int.Bit1 k1) (Int.Bit1 k2) \<longleftrightarrow> HOL.equal k1 k2"
6.61 + unfolding equal_eq by simp_all
6.62
6.63 lemma eq_int_refl [code nbe]:
6.64 - "eq_class.eq (k::int) k \<longleftrightarrow> True"
6.65 - by (rule HOL.eq_refl)
6.66 + "HOL.equal (k::int) k \<longleftrightarrow> True"
6.67 + by (rule equal_refl)
6.68
6.69 lemma less_eq_number_of_int_code [code]:
6.70 "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
7.1 --- a/src/HOL/Lazy_Sequence.thy Fri Aug 27 15:36:02 2010 +0200
7.2 +++ b/src/HOL/Lazy_Sequence.thy Fri Aug 27 19:34:23 2010 +0200
7.3 @@ -39,10 +39,14 @@
7.4 "size xq = (case yield xq of None => 0 | Some (x, xq') => size xq' + 1)"
7.5 by (cases xq) auto
7.6
7.7 -lemma [code]: "eq_class.eq xq yq = (case (yield xq, yield yq) of
7.8 - (None, None) => True | (Some (x, xq'), Some (y, yq')) => (HOL.eq x y) \<and> (eq_class.eq xq yq) | _ => False)"
7.9 -apply (cases xq) apply (cases yq) apply (auto simp add: eq_class.eq_equals)
7.10 -apply (cases yq) apply (auto simp add: eq_class.eq_equals) done
7.11 +lemma [code]: "HOL.equal xq yq = (case (yield xq, yield yq) of
7.12 + (None, None) => True | (Some (x, xq'), Some (y, yq')) => (HOL.equal x y) \<and> (HOL.equal xq yq) | _ => False)"
7.13 +apply (cases xq) apply (cases yq) apply (auto simp add: equal_eq)
7.14 +apply (cases yq) apply (auto simp add: equal_eq) done
7.15 +
7.16 +lemma [code nbe]:
7.17 + "HOL.equal (x :: 'a lazy_sequence) x \<longleftrightarrow> True"
7.18 + by (fact equal_refl)
7.19
7.20 lemma seq_case [code]:
7.21 "lazy_sequence_case f g xq = (case (yield xq) of None => f | Some (x, xq') => g x xq')"
8.1 --- a/src/HOL/Library/AssocList.thy Fri Aug 27 15:36:02 2010 +0200
8.2 +++ b/src/HOL/Library/AssocList.thy Fri Aug 27 19:34:23 2010 +0200
8.3 @@ -701,7 +701,44 @@
8.4 "Mapping.bulkload vs = Mapping (map (\<lambda>n. (n, vs ! n)) [0..<length vs])"
8.5 by (rule mapping_eqI) (simp add: map_of_map_restrict expand_fun_eq)
8.6
8.7 -lemma [code, code del]:
8.8 - "HOL.eq (x :: (_, _) mapping) y \<longleftrightarrow> x = y" by (fact eq_equals) (*FIXME*)
8.9 +lemma map_of_eqI: (*FIXME move to Map.thy*)
8.10 + assumes set_eq: "set (map fst xs) = set (map fst ys)"
8.11 + assumes map_eq: "\<forall>k\<in>set (map fst xs). map_of xs k = map_of ys k"
8.12 + shows "map_of xs = map_of ys"
8.13 +proof (rule ext)
8.14 + fix k show "map_of xs k = map_of ys k"
8.15 + proof (cases "map_of xs k")
8.16 + case None then have "k \<notin> set (map fst xs)" by (simp add: map_of_eq_None_iff)
8.17 + with set_eq have "k \<notin> set (map fst ys)" by simp
8.18 + then have "map_of ys k = None" by (simp add: map_of_eq_None_iff)
8.19 + with None show ?thesis by simp
8.20 + next
8.21 + case (Some v) then have "k \<in> set (map fst xs)" by (auto simp add: dom_map_of_conv_image_fst [symmetric])
8.22 + with map_eq show ?thesis by auto
8.23 + qed
8.24 +qed
8.25 +
8.26 +lemma map_of_eq_dom: (*FIXME move to Map.thy*)
8.27 + assumes "map_of xs = map_of ys"
8.28 + shows "fst ` set xs = fst ` set ys"
8.29 +proof -
8.30 + from assms have "dom (map_of xs) = dom (map_of ys)" by simp
8.31 + then show ?thesis by (simp add: dom_map_of_conv_image_fst)
8.32 +qed
8.33 +
8.34 +lemma equal_Mapping [code]:
8.35 + "HOL.equal (Mapping xs) (Mapping ys) \<longleftrightarrow>
8.36 + (let ks = map fst xs; ls = map fst ys
8.37 + in (\<forall>l\<in>set ls. l \<in> set ks) \<and> (\<forall>k\<in>set ks. k \<in> set ls \<and> map_of xs k = map_of ys k))"
8.38 +proof -
8.39 + have aux: "\<And>a b xs. (a, b) \<in> set xs \<Longrightarrow> a \<in> fst ` set xs" by (auto simp add: image_def intro!: bexI)
8.40 + show ?thesis
8.41 + by (auto intro!: map_of_eqI simp add: Let_def equal Mapping_def)
8.42 + (auto dest!: map_of_eq_dom intro: aux)
8.43 +qed
8.44 +
8.45 +lemma [code nbe]:
8.46 + "HOL.equal (x :: ('a, 'b) mapping) x \<longleftrightarrow> True"
8.47 + by (fact equal_refl)
8.48
8.49 end
9.1 --- a/src/HOL/Library/Code_Char.thy Fri Aug 27 15:36:02 2010 +0200
9.2 +++ b/src/HOL/Library/Code_Char.thy Fri Aug 27 19:34:23 2010 +0200
9.3 @@ -19,7 +19,7 @@
9.4 #> String_Code.add_literal_list_string "Haskell"
9.5 *}
9.6
9.7 -code_instance char :: eq
9.8 +code_instance char :: equal
9.9 (Haskell -)
9.10
9.11 code_reserved SML
9.12 @@ -31,7 +31,7 @@
9.13 code_reserved Scala
9.14 char
9.15
9.16 -code_const "eq_class.eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
9.17 +code_const "HOL.equal \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
9.18 (SML "!((_ : char) = _)")
9.19 (OCaml "!((_ : char) = _)")
9.20 (Haskell infixl 4 "==")
10.1 --- a/src/HOL/Library/Code_Integer.thy Fri Aug 27 15:36:02 2010 +0200
10.2 +++ b/src/HOL/Library/Code_Integer.thy Fri Aug 27 19:34:23 2010 +0200
10.3 @@ -21,7 +21,7 @@
10.4 (Scala "BigInt")
10.5 (Eval "int")
10.6
10.7 -code_instance int :: eq
10.8 +code_instance int :: equal
10.9 (Haskell -)
10.10
10.11 setup {*
10.12 @@ -96,7 +96,7 @@
10.13 (Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))")
10.14 (Eval "Integer.div'_mod/ (abs _)/ (abs _)")
10.15
10.16 -code_const "eq_class.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
10.17 +code_const "HOL.equal \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
10.18 (SML "!((_ : IntInf.int) = _)")
10.19 (OCaml "Big'_int.eq'_big'_int")
10.20 (Haskell infixl 4 "==")
11.1 --- a/src/HOL/Library/Code_Natural.thy Fri Aug 27 15:36:02 2010 +0200
11.2 +++ b/src/HOL/Library/Code_Natural.thy Fri Aug 27 19:34:23 2010 +0200
11.3 @@ -112,7 +112,7 @@
11.4 false Code_Printer.literal_alternative_numeral) ["Haskell", "Scala"]
11.5 *}
11.6
11.7 -code_instance code_numeral :: eq
11.8 +code_instance code_numeral :: equal
11.9 (Haskell -)
11.10
11.11 code_const "op + \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
11.12 @@ -131,7 +131,7 @@
11.13 (Haskell "divMod")
11.14 (Scala infixl 8 "/%")
11.15
11.16 -code_const "eq_class.eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
11.17 +code_const "HOL.equal \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
11.18 (Haskell infixl 4 "==")
11.19 (Scala infixl 5 "==")
11.20
12.1 --- a/src/HOL/Library/Dlist.thy Fri Aug 27 15:36:02 2010 +0200
12.2 +++ b/src/HOL/Library/Dlist.thy Fri Aug 27 19:34:23 2010 +0200
12.3 @@ -109,16 +109,20 @@
12.4
12.5 text {* Equality *}
12.6
12.7 -instantiation dlist :: (eq) eq
12.8 +instantiation dlist :: (equal) equal
12.9 begin
12.10
12.11 -definition "HOL.eq dxs dys \<longleftrightarrow> HOL.eq (list_of_dlist dxs) (list_of_dlist dys)"
12.12 +definition "HOL.equal dxs dys \<longleftrightarrow> HOL.equal (list_of_dlist dxs) (list_of_dlist dys)"
12.13
12.14 instance proof
12.15 -qed (simp add: eq_dlist_def eq list_of_dlist_inject)
12.16 +qed (simp add: equal_dlist_def equal list_of_dlist_inject)
12.17
12.18 end
12.19
12.20 +lemma [code nbe]:
12.21 + "HOL.equal (dxs :: 'a::equal dlist) dxs \<longleftrightarrow> True"
12.22 + by (fact equal_refl)
12.23 +
12.24
12.25 section {* Induction principle and case distinction *}
12.26
13.1 --- a/src/HOL/Library/Efficient_Nat.thy Fri Aug 27 15:36:02 2010 +0200
13.2 +++ b/src/HOL/Library/Efficient_Nat.thy Fri Aug 27 19:34:23 2010 +0200
13.3 @@ -55,12 +55,12 @@
13.4 by (simp add: prod_fun_def split_def pdivmod_def nat_div_distrib nat_mod_distrib divmod_nat_div_mod)
13.5
13.6 lemma eq_nat_code [code]:
13.7 - "eq_class.eq n m \<longleftrightarrow> eq_class.eq (of_nat n \<Colon> int) (of_nat m)"
13.8 - by (simp add: eq)
13.9 + "HOL.equal n m \<longleftrightarrow> HOL.equal (of_nat n \<Colon> int) (of_nat m)"
13.10 + by (simp add: equal)
13.11
13.12 lemma eq_nat_refl [code nbe]:
13.13 - "eq_class.eq (n::nat) n \<longleftrightarrow> True"
13.14 - by (rule HOL.eq_refl)
13.15 + "HOL.equal (n::nat) n \<longleftrightarrow> True"
13.16 + by (rule equal_refl)
13.17
13.18 lemma less_eq_nat_code [code]:
13.19 "n \<le> m \<longleftrightarrow> (of_nat n \<Colon> int) \<le> of_nat m"
13.20 @@ -332,7 +332,7 @@
13.21 (Haskell "Nat.Nat")
13.22 (Scala "Nat.Nat")
13.23
13.24 -code_instance nat :: eq
13.25 +code_instance nat :: equal
13.26 (Haskell -)
13.27
13.28 text {*
13.29 @@ -442,7 +442,7 @@
13.30 (Scala infixl 8 "/%")
13.31 (Eval "Integer.div'_mod")
13.32
13.33 -code_const "eq_class.eq \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
13.34 +code_const "HOL.equal \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
13.35 (SML "!((_ : IntInf.int) = _)")
13.36 (OCaml "Big'_int.eq'_big'_int")
13.37 (Haskell infixl 4 "==")
14.1 --- a/src/HOL/Library/Enum.thy Fri Aug 27 15:36:02 2010 +0200
14.2 +++ b/src/HOL/Library/Enum.thy Fri Aug 27 19:34:23 2010 +0200
14.3 @@ -35,17 +35,21 @@
14.4
14.5 subsection {* Equality and order on functions *}
14.6
14.7 -instantiation "fun" :: (enum, eq) eq
14.8 +instantiation "fun" :: (enum, equal) equal
14.9 begin
14.10
14.11 definition
14.12 - "eq_class.eq f g \<longleftrightarrow> (\<forall>x \<in> set enum. f x = g x)"
14.13 + "HOL.equal f g \<longleftrightarrow> (\<forall>x \<in> set enum. f x = g x)"
14.14
14.15 instance proof
14.16 -qed (simp_all add: eq_fun_def enum_all expand_fun_eq)
14.17 +qed (simp_all add: equal_fun_def enum_all expand_fun_eq)
14.18
14.19 end
14.20
14.21 +lemma [code nbe]:
14.22 + "HOL.equal (f :: _ \<Rightarrow> _) f \<longleftrightarrow> True"
14.23 + by (fact equal_refl)
14.24 +
14.25 lemma order_fun [code]:
14.26 fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>order"
14.27 shows "f \<le> g \<longleftrightarrow> list_all (\<lambda>x. f x \<le> g x) enum"
14.28 @@ -169,7 +173,7 @@
14.29
14.30 end
14.31
14.32 -lemma enum_fun_code [code]: "enum = (let enum_a = (enum \<Colon> 'a\<Colon>{enum, eq} list)
14.33 +lemma enum_fun_code [code]: "enum = (let enum_a = (enum \<Colon> 'a\<Colon>{enum, equal} list)
14.34 in map (\<lambda>ys. the o map_of (zip enum_a ys)) (n_lists (length enum_a) enum))"
14.35 by (simp add: enum_fun_def Let_def)
14.36
15.1 --- a/src/HOL/Library/Fset.thy Fri Aug 27 15:36:02 2010 +0200
15.2 +++ b/src/HOL/Library/Fset.thy Fri Aug 27 19:34:23 2010 +0200
15.3 @@ -227,17 +227,21 @@
15.4 "A < B \<longleftrightarrow> A \<le> B \<and> \<not> B \<le> (A :: 'a fset)"
15.5 by (fact less_le_not_le)
15.6
15.7 -instantiation fset :: (type) eq
15.8 +instantiation fset :: (type) equal
15.9 begin
15.10
15.11 definition
15.12 - "eq_fset A B \<longleftrightarrow> A \<le> B \<and> B \<le> (A :: 'a fset)"
15.13 + "HOL.equal A B \<longleftrightarrow> A \<le> B \<and> B \<le> (A :: 'a fset)"
15.14
15.15 instance proof
15.16 -qed (simp add: eq_fset_def set_eq [symmetric])
15.17 +qed (simp add: equal_fset_def set_eq [symmetric])
15.18
15.19 end
15.20
15.21 +lemma [code nbe]:
15.22 + "HOL.equal (A :: 'a fset) A \<longleftrightarrow> True"
15.23 + by (fact equal_refl)
15.24 +
15.25
15.26 subsection {* Functorial operations *}
15.27
16.1 --- a/src/HOL/Library/List_Prefix.thy Fri Aug 27 15:36:02 2010 +0200
16.2 +++ b/src/HOL/Library/List_Prefix.thy Fri Aug 27 19:34:23 2010 +0200
16.3 @@ -81,9 +81,9 @@
16.4 by (auto simp add: prefix_def)
16.5
16.6 lemma less_eq_list_code [code]:
16.7 - "([]\<Colon>'a\<Colon>{eq, ord} list) \<le> xs \<longleftrightarrow> True"
16.8 - "(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> [] \<longleftrightarrow> False"
16.9 - "(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> y # ys \<longleftrightarrow> x = y \<and> xs \<le> ys"
16.10 + "([]\<Colon>'a\<Colon>{equal, ord} list) \<le> xs \<longleftrightarrow> True"
16.11 + "(x\<Colon>'a\<Colon>{equal, ord}) # xs \<le> [] \<longleftrightarrow> False"
16.12 + "(x\<Colon>'a\<Colon>{equal, ord}) # xs \<le> y # ys \<longleftrightarrow> x = y \<and> xs \<le> ys"
16.13 by simp_all
16.14
16.15 lemma same_prefix_prefix [simp]: "(xs @ ys \<le> xs @ zs) = (ys \<le> zs)"
17.1 --- a/src/HOL/Library/List_lexord.thy Fri Aug 27 15:36:02 2010 +0200
17.2 +++ b/src/HOL/Library/List_lexord.thy Fri Aug 27 19:34:23 2010 +0200
17.3 @@ -103,15 +103,15 @@
17.4 end
17.5
17.6 lemma less_list_code [code]:
17.7 - "xs < ([]\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> False"
17.8 - "[] < (x\<Colon>'a\<Colon>{eq, order}) # xs \<longleftrightarrow> True"
17.9 - "(x\<Colon>'a\<Colon>{eq, order}) # xs < y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs < ys"
17.10 + "xs < ([]\<Colon>'a\<Colon>{equal, order} list) \<longleftrightarrow> False"
17.11 + "[] < (x\<Colon>'a\<Colon>{equal, order}) # xs \<longleftrightarrow> True"
17.12 + "(x\<Colon>'a\<Colon>{equal, order}) # xs < y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs < ys"
17.13 by simp_all
17.14
17.15 lemma less_eq_list_code [code]:
17.16 - "x # xs \<le> ([]\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> False"
17.17 - "[] \<le> (xs\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> True"
17.18 - "(x\<Colon>'a\<Colon>{eq, order}) # xs \<le> y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs \<le> ys"
17.19 + "x # xs \<le> ([]\<Colon>'a\<Colon>{equal, order} list) \<longleftrightarrow> False"
17.20 + "[] \<le> (xs\<Colon>'a\<Colon>{equal, order} list) \<longleftrightarrow> True"
17.21 + "(x\<Colon>'a\<Colon>{equal, order}) # xs \<le> y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs \<le> ys"
17.22 by simp_all
17.23
17.24 end
18.1 --- a/src/HOL/Library/Mapping.thy Fri Aug 27 15:36:02 2010 +0200
18.2 +++ b/src/HOL/Library/Mapping.thy Fri Aug 27 19:34:23 2010 +0200
18.3 @@ -280,14 +280,14 @@
18.4
18.5 code_datatype empty update
18.6
18.7 -instantiation mapping :: (type, type) eq
18.8 +instantiation mapping :: (type, type) equal
18.9 begin
18.10
18.11 definition [code del]:
18.12 - "HOL.eq m n \<longleftrightarrow> lookup m = lookup n"
18.13 + "HOL.equal m n \<longleftrightarrow> lookup m = lookup n"
18.14
18.15 instance proof
18.16 -qed (simp add: eq_mapping_def)
18.17 +qed (simp add: equal_mapping_def)
18.18
18.19 end
18.20
19.1 --- a/src/HOL/Library/Multiset.thy Fri Aug 27 15:36:02 2010 +0200
19.2 +++ b/src/HOL/Library/Multiset.thy Fri Aug 27 19:34:23 2010 +0200
19.3 @@ -938,17 +938,21 @@
19.4 qed
19.5 qed
19.6
19.7 -instantiation multiset :: (eq) eq
19.8 +instantiation multiset :: (equal) equal
19.9 begin
19.10
19.11 definition
19.12 - "HOL.eq A B \<longleftrightarrow> (A::'a multiset) \<le> B \<and> B \<le> A"
19.13 + "HOL.equal A B \<longleftrightarrow> (A::'a multiset) \<le> B \<and> B \<le> A"
19.14
19.15 instance proof
19.16 -qed (simp add: eq_multiset_def eq_iff)
19.17 +qed (simp add: equal_multiset_def eq_iff)
19.18
19.19 end
19.20
19.21 +lemma [code nbe]:
19.22 + "HOL.equal (A :: 'a::equal multiset) A \<longleftrightarrow> True"
19.23 + by (fact equal_refl)
19.24 +
19.25 definition (in term_syntax)
19.26 bagify :: "('a\<Colon>typerep \<times> nat) list \<times> (unit \<Rightarrow> Code_Evaluation.term)
19.27 \<Rightarrow> 'a multiset \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
20.1 --- a/src/HOL/Library/Nested_Environment.thy Fri Aug 27 15:36:02 2010 +0200
20.2 +++ b/src/HOL/Library/Nested_Environment.thy Fri Aug 27 19:34:23 2010 +0200
20.3 @@ -521,22 +521,21 @@
20.4 text {* Environments and code generation *}
20.5
20.6 lemma [code, code del]:
20.7 - fixes e1 e2 :: "('b\<Colon>eq, 'a\<Colon>eq, 'c\<Colon>eq) env"
20.8 - shows "eq_class.eq e1 e2 \<longleftrightarrow> eq_class.eq e1 e2" ..
20.9 + "(HOL.equal :: (_, _, _) env \<Rightarrow> _) = HOL.equal" ..
20.10
20.11 -lemma eq_env_code [code]:
20.12 - fixes x y :: "'a\<Colon>eq"
20.13 - and f g :: "'c\<Colon>{eq, finite} \<Rightarrow> ('b\<Colon>eq, 'a, 'c) env option"
20.14 - shows "eq_class.eq (Env x f) (Env y g) \<longleftrightarrow>
20.15 - eq_class.eq x y \<and> (\<forall>z\<in>UNIV. case f z
20.16 +lemma equal_env_code [code]:
20.17 + fixes x y :: "'a\<Colon>equal"
20.18 + and f g :: "'c\<Colon>{equal, finite} \<Rightarrow> ('b\<Colon>equal, 'a, 'c) env option"
20.19 + shows "HOL.equal (Env x f) (Env y g) \<longleftrightarrow>
20.20 + HOL.equal x y \<and> (\<forall>z\<in>UNIV. case f z
20.21 of None \<Rightarrow> (case g z
20.22 of None \<Rightarrow> True | Some _ \<Rightarrow> False)
20.23 | Some a \<Rightarrow> (case g z
20.24 - of None \<Rightarrow> False | Some b \<Rightarrow> eq_class.eq a b))" (is ?env)
20.25 - and "eq_class.eq (Val a) (Val b) \<longleftrightarrow> eq_class.eq a b"
20.26 - and "eq_class.eq (Val a) (Env y g) \<longleftrightarrow> False"
20.27 - and "eq_class.eq (Env x f) (Val b) \<longleftrightarrow> False"
20.28 -proof (unfold eq)
20.29 + of None \<Rightarrow> False | Some b \<Rightarrow> HOL.equal a b))" (is ?env)
20.30 + and "HOL.equal (Val a) (Val b) \<longleftrightarrow> HOL.equal a b"
20.31 + and "HOL.equal (Val a) (Env y g) \<longleftrightarrow> False"
20.32 + and "HOL.equal (Env x f) (Val b) \<longleftrightarrow> False"
20.33 +proof (unfold equal)
20.34 have "f = g \<longleftrightarrow> (\<forall>z. case f z
20.35 of None \<Rightarrow> (case g z
20.36 of None \<Rightarrow> True | Some _ \<Rightarrow> False)
20.37 @@ -562,6 +561,10 @@
20.38 of None \<Rightarrow> False | Some b \<Rightarrow> a = b))" by simp
20.39 qed simp_all
20.40
20.41 +lemma [code nbe]:
20.42 + "HOL.equal (x :: (_, _, _) env) x \<longleftrightarrow> True"
20.43 + by (fact equal_refl)
20.44 +
20.45 lemma [code, code del]:
20.46 "(Code_Evaluation.term_of :: ('a::{term_of, type}, 'b::{term_of, type}, 'c::{term_of, type}) env \<Rightarrow> term) = Code_Evaluation.term_of" ..
20.47
21.1 --- a/src/HOL/Library/Polynomial.thy Fri Aug 27 15:36:02 2010 +0200
21.2 +++ b/src/HOL/Library/Polynomial.thy Fri Aug 27 19:34:23 2010 +0200
21.3 @@ -1505,23 +1505,27 @@
21.4
21.5 declare pCons_0_0 [code_post]
21.6
21.7 -instantiation poly :: ("{zero,eq}") eq
21.8 +instantiation poly :: ("{zero, equal}") equal
21.9 begin
21.10
21.11 definition
21.12 - "eq_class.eq (p::'a poly) q \<longleftrightarrow> p = q"
21.13 + "HOL.equal (p::'a poly) q \<longleftrightarrow> p = q"
21.14
21.15 -instance
21.16 - by default (rule eq_poly_def)
21.17 +instance proof
21.18 +qed (rule equal_poly_def)
21.19
21.20 end
21.21
21.22 lemma eq_poly_code [code]:
21.23 - "eq_class.eq (0::_ poly) (0::_ poly) \<longleftrightarrow> True"
21.24 - "eq_class.eq (0::_ poly) (pCons b q) \<longleftrightarrow> eq_class.eq 0 b \<and> eq_class.eq 0 q"
21.25 - "eq_class.eq (pCons a p) (0::_ poly) \<longleftrightarrow> eq_class.eq a 0 \<and> eq_class.eq p 0"
21.26 - "eq_class.eq (pCons a p) (pCons b q) \<longleftrightarrow> eq_class.eq a b \<and> eq_class.eq p q"
21.27 -unfolding eq by simp_all
21.28 + "HOL.equal (0::_ poly) (0::_ poly) \<longleftrightarrow> True"
21.29 + "HOL.equal (0::_ poly) (pCons b q) \<longleftrightarrow> HOL.equal 0 b \<and> HOL.equal 0 q"
21.30 + "HOL.equal (pCons a p) (0::_ poly) \<longleftrightarrow> HOL.equal a 0 \<and> HOL.equal p 0"
21.31 + "HOL.equal (pCons a p) (pCons b q) \<longleftrightarrow> HOL.equal a b \<and> HOL.equal p q"
21.32 + by (simp_all add: equal)
21.33 +
21.34 +lemma [code nbe]:
21.35 + "HOL.equal (p :: _ poly) p \<longleftrightarrow> True"
21.36 + by (fact equal_refl)
21.37
21.38 lemmas coeff_code [code] =
21.39 coeff_0 coeff_pCons_0 coeff_pCons_Suc
22.1 --- a/src/HOL/Library/Product_ord.thy Fri Aug 27 15:36:02 2010 +0200
22.2 +++ b/src/HOL/Library/Product_ord.thy Fri Aug 27 19:34:23 2010 +0200
22.3 @@ -22,8 +22,8 @@
22.4 end
22.5
22.6 lemma [code]:
22.7 - "(x1\<Colon>'a\<Colon>{ord, eq}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 \<le> y2"
22.8 - "(x1\<Colon>'a\<Colon>{ord, eq}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 < y2"
22.9 + "(x1\<Colon>'a\<Colon>{ord, equal}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 \<le> y2"
22.10 + "(x1\<Colon>'a\<Colon>{ord, equal}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 < y2"
22.11 unfolding prod_le_def prod_less_def by simp_all
22.12
22.13 instance prod :: (preorder, preorder) preorder proof
23.1 --- a/src/HOL/Library/RBT.thy Fri Aug 27 15:36:02 2010 +0200
23.2 +++ b/src/HOL/Library/RBT.thy Fri Aug 27 19:34:23 2010 +0200
23.3 @@ -222,12 +222,14 @@
23.4 "Mapping.bulkload vs = Mapping (bulkload (List.map (\<lambda>n. (n, vs ! n)) [0..<length vs]))"
23.5 by (rule mapping_eqI) (simp add: map_of_map_restrict expand_fun_eq)
23.6
23.7 -lemma [code, code del]:
23.8 - "HOL.eq (x :: (_, _) mapping) y \<longleftrightarrow> x = y" by (fact eq_equals) (*FIXME*)
23.9 +lemma equal_Mapping [code]:
23.10 + "HOL.equal (Mapping t1) (Mapping t2) \<longleftrightarrow> entries t1 = entries t2"
23.11 + by (simp add: equal Mapping_def entries_lookup)
23.12
23.13 -lemma eq_Mapping [code]:
23.14 - "HOL.eq (Mapping t1) (Mapping t2) \<longleftrightarrow> entries t1 = entries t2"
23.15 - by (simp add: eq Mapping_def entries_lookup)
23.16 +lemma [code nbe]:
23.17 + "HOL.equal (x :: (_, _) mapping) x \<longleftrightarrow> True"
23.18 + by (fact equal_refl)
23.19 +
23.20
23.21 hide_const (open) impl_of lookup empty insert delete
23.22 entries keys bulkload map_entry map fold
24.1 --- a/src/HOL/List.thy Fri Aug 27 15:36:02 2010 +0200
24.2 +++ b/src/HOL/List.thy Fri Aug 27 19:34:23 2010 +0200
24.3 @@ -4721,8 +4721,8 @@
24.4 by (simp add: null_def)
24.5
24.6 lemma equal_Nil_null [code_unfold]:
24.7 - "eq_class.eq xs [] \<longleftrightarrow> null xs"
24.8 - by (simp add: eq eq_Nil_null)
24.9 + "HOL.equal xs [] \<longleftrightarrow> null xs"
24.10 + by (simp add: equal eq_Nil_null)
24.11
24.12 definition maps :: "('a \<Rightarrow> 'b list) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
24.13 [code_post]: "maps f xs = concat (map f xs)"
24.14 @@ -4821,10 +4821,10 @@
24.15 (Haskell "[]")
24.16 (Scala "!Nil")
24.17
24.18 -code_instance list :: eq
24.19 +code_instance list :: equal
24.20 (Haskell -)
24.21
24.22 -code_const "eq_class.eq \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool"
24.23 +code_const "HOL.equal \<Colon> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
24.24 (Haskell infixl 4 "==")
24.25
24.26 code_reserved SML
25.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML Fri Aug 27 15:36:02 2010 +0200
25.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Fri Aug 27 19:34:23 2010 +0200
25.3 @@ -202,7 +202,7 @@
25.4 (@{const_name "top_fun_inst.top_fun"}, "'a"),
25.5 (@{const_name "Pure.term"}, "'a"),
25.6 (@{const_name "top_class.top"}, "'a"),
25.7 - (@{const_name "eq_class.eq"}, "'a"),
25.8 + (@{const_name "HOL.equal"}, "'a"),
25.9 (@{const_name "Quotient.Quot_True"}, "'a")(*,
25.10 (@{const_name "uminus"}, "'a"),
25.11 (@{const_name "Nat.size"}, "'a"),
25.12 @@ -237,7 +237,7 @@
25.13 @{const_name "top_fun_inst.top_fun"},
25.14 @{const_name "Pure.term"},
25.15 @{const_name "top_class.top"},
25.16 - @{const_name "eq_class.eq"},
25.17 + @{const_name "HOL.equal"},
25.18 @{const_name "Quotient.Quot_True"}]
25.19
25.20 fun is_forbidden_mutant t =
26.1 --- a/src/HOL/Option.thy Fri Aug 27 15:36:02 2010 +0200
26.2 +++ b/src/HOL/Option.thy Fri Aug 27 19:34:23 2010 +0200
26.3 @@ -99,8 +99,8 @@
26.4 by (simp add: is_none_def)
26.5
26.6 lemma [code_unfold]:
26.7 - "eq_class.eq x None \<longleftrightarrow> is_none x"
26.8 - by (simp add: eq is_none_none)
26.9 + "HOL.equal x None \<longleftrightarrow> is_none x"
26.10 + by (simp add: equal is_none_none)
26.11
26.12 hide_const (open) is_none
26.13
26.14 @@ -116,10 +116,10 @@
26.15 (Haskell "Nothing" and "Just")
26.16 (Scala "!None" and "Some")
26.17
26.18 -code_instance option :: eq
26.19 +code_instance option :: equal
26.20 (Haskell -)
26.21
26.22 -code_const "eq_class.eq \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool"
26.23 +code_const "HOL.equal \<Colon> 'a option \<Rightarrow> 'a option \<Rightarrow> bool"
26.24 (Haskell infixl 4 "==")
26.25
26.26 code_reserved SML
27.1 --- a/src/HOL/Predicate.thy Fri Aug 27 15:36:02 2010 +0200
27.2 +++ b/src/HOL/Predicate.thy Fri Aug 27 19:34:23 2010 +0200
27.3 @@ -808,8 +808,12 @@
27.4
27.5 lemma eq_pred_code [code]:
27.6 fixes P Q :: "'a pred"
27.7 - shows "eq_class.eq P Q \<longleftrightarrow> P \<le> Q \<and> Q \<le> P"
27.8 - unfolding eq by auto
27.9 + shows "HOL.equal P Q \<longleftrightarrow> P \<le> Q \<and> Q \<le> P"
27.10 + by (auto simp add: equal)
27.11 +
27.12 +lemma [code nbe]:
27.13 + "HOL.equal (x :: 'a pred) x \<longleftrightarrow> True"
27.14 + by (fact equal_refl)
27.15
27.16 lemma [code]:
27.17 "pred_case f P = f (eval P)"
28.1 --- a/src/HOL/Product_Type.thy Fri Aug 27 15:36:02 2010 +0200
28.2 +++ b/src/HOL/Product_Type.thy Fri Aug 27 19:34:23 2010 +0200
28.3 @@ -21,17 +21,17 @@
28.4 -- "prefer plain propositional version"
28.5
28.6 lemma
28.7 - shows [code]: "eq_class.eq False P \<longleftrightarrow> \<not> P"
28.8 - and [code]: "eq_class.eq True P \<longleftrightarrow> P"
28.9 - and [code]: "eq_class.eq P False \<longleftrightarrow> \<not> P"
28.10 - and [code]: "eq_class.eq P True \<longleftrightarrow> P"
28.11 - and [code nbe]: "eq_class.eq P P \<longleftrightarrow> True"
28.12 - by (simp_all add: eq)
28.13 + shows [code]: "HOL.equal False P \<longleftrightarrow> \<not> P"
28.14 + and [code]: "HOL.equal True P \<longleftrightarrow> P"
28.15 + and [code]: "HOL.equal P False \<longleftrightarrow> \<not> P"
28.16 + and [code]: "HOL.equal P True \<longleftrightarrow> P"
28.17 + and [code nbe]: "HOL.equal P P \<longleftrightarrow> True"
28.18 + by (simp_all add: equal)
28.19
28.20 -code_const "eq_class.eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
28.21 +code_const "HOL.equal \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
28.22 (Haskell infixl 4 "==")
28.23
28.24 -code_instance bool :: eq
28.25 +code_instance bool :: equal
28.26 (Haskell -)
28.27
28.28
28.29 @@ -92,7 +92,7 @@
28.30 end
28.31
28.32 lemma [code]:
28.33 - "eq_class.eq (u\<Colon>unit) v \<longleftrightarrow> True" unfolding eq unit_eq [of u] unit_eq [of v] by rule+
28.34 + "HOL.equal (u\<Colon>unit) v \<longleftrightarrow> True" unfolding equal unit_eq [of u] unit_eq [of v] by rule+
28.35
28.36 code_type unit
28.37 (SML "unit")
28.38 @@ -106,10 +106,10 @@
28.39 (Haskell "()")
28.40 (Scala "()")
28.41
28.42 -code_instance unit :: eq
28.43 +code_instance unit :: equal
28.44 (Haskell -)
28.45
28.46 -code_const "eq_class.eq \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
28.47 +code_const "HOL.equal \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
28.48 (Haskell infixl 4 "==")
28.49
28.50 code_reserved SML
28.51 @@ -277,10 +277,10 @@
28.52 (Haskell "!((_),/ (_))")
28.53 (Scala "!((_),/ (_))")
28.54
28.55 -code_instance prod :: eq
28.56 +code_instance prod :: equal
28.57 (Haskell -)
28.58
28.59 -code_const "eq_class.eq \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
28.60 +code_const "HOL.equal \<Colon> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
28.61 (Haskell infixl 4 "==")
28.62
28.63 types_code
29.1 --- a/src/HOL/Quickcheck.thy Fri Aug 27 15:36:02 2010 +0200
29.2 +++ b/src/HOL/Quickcheck.thy Fri Aug 27 19:34:23 2010 +0200
29.3 @@ -97,7 +97,7 @@
29.4 \<Rightarrow> Random.seed \<Rightarrow> (('a\<Colon>term_of \<Rightarrow> 'b\<Colon>typerep) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
29.5 "random_fun_lift f = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Evaluation.term_of f Random.split_seed"
29.6
29.7 -instantiation "fun" :: ("{eq, term_of}", random) random
29.8 +instantiation "fun" :: ("{equal, term_of}", random) random
29.9 begin
29.10
29.11 definition random_fun :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
30.1 --- a/src/HOL/Rat.thy Fri Aug 27 15:36:02 2010 +0200
30.2 +++ b/src/HOL/Rat.thy Fri Aug 27 19:34:23 2010 +0200
30.3 @@ -1083,18 +1083,18 @@
30.4 by (cases "0::int" a rule: linorder_cases) (simp_all add: quotient_of_Fract)
30.5 qed
30.6
30.7 -instantiation rat :: eq
30.8 +instantiation rat :: equal
30.9 begin
30.10
30.11 definition [code]:
30.12 - "eq_class.eq a b \<longleftrightarrow> quotient_of a = quotient_of b"
30.13 + "HOL.equal a b \<longleftrightarrow> quotient_of a = quotient_of b"
30.14
30.15 instance proof
30.16 -qed (simp add: eq_rat_def quotient_of_inject_eq)
30.17 +qed (simp add: equal_rat_def quotient_of_inject_eq)
30.18
30.19 lemma rat_eq_refl [code nbe]:
30.20 - "eq_class.eq (r::rat) r \<longleftrightarrow> True"
30.21 - by (rule HOL.eq_refl)
30.22 + "HOL.equal (r::rat) r \<longleftrightarrow> True"
30.23 + by (rule equal_refl)
30.24
30.25 end
30.26
31.1 --- a/src/HOL/RealDef.thy Fri Aug 27 15:36:02 2010 +0200
31.2 +++ b/src/HOL/RealDef.thy Fri Aug 27 19:34:23 2010 +0200
31.3 @@ -1697,19 +1697,21 @@
31.4 "Ratreal (number_of r / number_of s) = number_of r / number_of s"
31.5 unfolding Ratreal_number_of_quotient [symmetric] Ratreal_def of_rat_divide ..
31.6
31.7 -instantiation real :: eq
31.8 +instantiation real :: equal
31.9 begin
31.10
31.11 -definition "eq_class.eq (x\<Colon>real) y \<longleftrightarrow> x - y = 0"
31.12 +definition "HOL.equal (x\<Colon>real) y \<longleftrightarrow> x - y = 0"
31.13
31.14 -instance by default (simp add: eq_real_def)
31.15 +instance proof
31.16 +qed (simp add: equal_real_def)
31.17
31.18 -lemma real_eq_code [code]: "eq_class.eq (Ratreal x) (Ratreal y) \<longleftrightarrow> eq_class.eq x y"
31.19 - by (simp add: eq_real_def eq)
31.20 +lemma real_equal_code [code]:
31.21 + "HOL.equal (Ratreal x) (Ratreal y) \<longleftrightarrow> HOL.equal x y"
31.22 + by (simp add: equal_real_def equal)
31.23
31.24 -lemma real_eq_refl [code nbe]:
31.25 - "eq_class.eq (x::real) x \<longleftrightarrow> True"
31.26 - by (rule HOL.eq_refl)
31.27 +lemma [code nbe]:
31.28 + "HOL.equal (x::real) x \<longleftrightarrow> True"
31.29 + by (rule equal_refl)
31.30
31.31 end
31.32
32.1 --- a/src/HOL/String.thy Fri Aug 27 15:36:02 2010 +0200
32.2 +++ b/src/HOL/String.thy Fri Aug 27 19:34:23 2010 +0200
32.3 @@ -183,10 +183,10 @@
32.4 fold String_Code.add_literal_string ["SML", "OCaml", "Haskell", "Scala"]
32.5 *}
32.6
32.7 -code_instance literal :: eq
32.8 +code_instance literal :: equal
32.9 (Haskell -)
32.10
32.11 -code_const "eq_class.eq \<Colon> literal \<Rightarrow> literal \<Rightarrow> bool"
32.12 +code_const "HOL.equal \<Colon> literal \<Rightarrow> literal \<Rightarrow> bool"
32.13 (SML "!((_ : string) = _)")
32.14 (OCaml "!((_ : string) = _)")
32.15 (Haskell infixl 4 "==")
33.1 --- a/src/HOL/Tools/Datatype/datatype_codegen.ML Fri Aug 27 15:36:02 2010 +0200
33.2 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Fri Aug 27 19:34:23 2010 +0200
33.3 @@ -68,7 +68,7 @@
33.4 val { descr, index, inject = inject_thms, distinct = distinct_thms, ... } =
33.5 Datatype_Data.the_info thy tyco;
33.6 val ty = Type (tyco, map TFree vs);
33.7 - fun mk_eq (t1, t2) = Const (@{const_name eq_class.eq}, ty --> ty --> HOLogic.boolT)
33.8 + fun mk_eq (t1, t2) = Const (@{const_name HOL.equal}, ty --> ty --> HOLogic.boolT)
33.9 $ t1 $ t2;
33.10 fun true_eq t12 = HOLogic.mk_eq (mk_eq t12, HOLogic.true_const);
33.11 fun false_eq t12 = HOLogic.mk_eq (mk_eq t12, HOLogic.false_const);
33.12 @@ -83,7 +83,7 @@
33.13 val distincts = maps prep_distinct (snd (nth (Datatype_Prop.make_distincts [descr] vs) index));
33.14 val refl = HOLogic.mk_Trueprop (true_eq (Free ("x", ty), Free ("x", ty)));
33.15 val simpset = Simplifier.global_context thy (HOL_basic_ss addsimps
33.16 - (map Simpdata.mk_eq (@{thm eq} :: @{thm eq_True} :: inject_thms @ distinct_thms)));
33.17 + (map Simpdata.mk_eq (@{thm equal} :: @{thm eq_True} :: inject_thms @ distinct_thms)));
33.18 fun prove prop = Skip_Proof.prove_global thy [] [] prop (K (ALLGOALS (simp_tac simpset)))
33.19 |> Simpdata.mk_eq;
33.20 in (map prove (triv_injects @ injects @ distincts), prove refl) end;
33.21 @@ -96,7 +96,7 @@
33.22 fun mk_side const_name = Const (const_name, ty --> ty --> HOLogic.boolT)
33.23 $ Free ("x", ty) $ Free ("y", ty);
33.24 val def = HOLogic.mk_Trueprop (HOLogic.mk_eq
33.25 - (mk_side @{const_name eq_class.eq}, mk_side @{const_name "op ="}));
33.26 + (mk_side @{const_name HOL.equal}, mk_side @{const_name "op ="}));
33.27 val def' = Syntax.check_term lthy def;
33.28 val ((_, (_, thm)), lthy') = Specification.definition
33.29 (NONE, (Attrib.empty_binding, def')) lthy;
33.30 @@ -115,7 +115,7 @@
33.31 #> snd
33.32 in
33.33 thy
33.34 - |> Class.instantiation (tycos, vs, [HOLogic.class_eq])
33.35 + |> Class.instantiation (tycos, vs, [HOLogic.class_equal])
33.36 |> fold_map add_def tycos
33.37 |-> (fn def_thms => Class.prove_instantiation_exit_result (map o Morphism.thm)
33.38 (fn _ => fn def_thms => tac def_thms) def_thms)
33.39 @@ -135,7 +135,7 @@
33.40 val case_rewrites = maps (#case_rewrites o Datatype_Data.the_info thy) tycos;
33.41 val certs = map (mk_case_cert thy) tycos;
33.42 val tycos_eq = filter_out
33.43 - (fn tyco => can (Sorts.mg_domain (Sign.classes_of thy) tyco) [HOLogic.class_eq]) tycos;
33.44 + (fn tyco => can (Sorts.mg_domain (Sign.classes_of thy) tyco) [HOLogic.class_equal]) tycos;
33.45 in
33.46 if null css then thy
33.47 else thy
34.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML Fri Aug 27 15:36:02 2010 +0200
34.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Fri Aug 27 19:34:23 2010 +0200
34.3 @@ -182,7 +182,7 @@
34.4 fun none_true assigns = forall (not_equal (SOME true) o snd) assigns
34.5
34.6 val syntactic_sorts =
34.7 - @{sort "{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,eq}"} @
34.8 + @{sort "{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,equal}"} @
34.9 @{sort number}
34.10 fun has_tfree_syntactic_sort (TFree (_, S as _ :: _)) =
34.11 subset (op =) (S, syntactic_sorts)
35.1 --- a/src/HOL/Tools/hologic.ML Fri Aug 27 15:36:02 2010 +0200
35.2 +++ b/src/HOL/Tools/hologic.ML Fri Aug 27 19:34:23 2010 +0200
35.3 @@ -49,7 +49,7 @@
35.4 val exists_const: typ -> term
35.5 val mk_exists: string * typ * term -> term
35.6 val choice_const: typ -> term
35.7 - val class_eq: string
35.8 + val class_equal: string
35.9 val mk_binop: string -> term * term -> term
35.10 val mk_binrel: string -> term * term -> term
35.11 val dest_bin: string -> typ -> term -> term * term
35.12 @@ -251,7 +251,7 @@
35.13
35.14 fun choice_const T = Const("Hilbert_Choice.Eps", (T --> boolT) --> T);
35.15
35.16 -val class_eq = "HOL.eq";
35.17 +val class_equal = "HOL.equal";
35.18
35.19
35.20 (* binary operations and relations *)
36.1 --- a/src/HOL/Tools/record.ML Fri Aug 27 15:36:02 2010 +0200
36.2 +++ b/src/HOL/Tools/record.ML Fri Aug 27 19:34:23 2010 +0200
36.3 @@ -1844,7 +1844,7 @@
36.4 let
36.5 val eq =
36.6 (HOLogic.mk_Trueprop o HOLogic.mk_eq)
36.7 - (Const (@{const_name eq_class.eq}, extT --> extT --> HOLogic.boolT),
36.8 + (Const (@{const_name HOL.equal}, extT --> extT --> HOLogic.boolT),
36.9 Const (@{const_name "op ="}, extT --> extT --> HOLogic.boolT));
36.10 fun tac eq_def =
36.11 Class.intro_classes_tac []
36.12 @@ -1853,15 +1853,15 @@
36.13 fun mk_eq thy eq_def = Simplifier.rewrite_rule
36.14 [(AxClass.unoverload thy o Thm.symmetric o Simpdata.mk_eq) eq_def] inject;
36.15 fun mk_eq_refl thy =
36.16 - @{thm HOL.eq_refl}
36.17 + @{thm equal_refl}
36.18 |> Thm.instantiate
36.19 - ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT_global extT)], [])
36.20 + ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort equal}), Logic.varifyT_global extT)], [])
36.21 |> AxClass.unoverload thy;
36.22 in
36.23 thy
36.24 |> Code.add_datatype [ext]
36.25 |> fold Code.add_default_eqn simps
36.26 - |> Class.instantiation ([ext_tyco], vs, [HOLogic.class_eq])
36.27 + |> Class.instantiation ([ext_tyco], vs, [HOLogic.class_equal])
36.28 |> `(fn lthy => Syntax.check_term lthy eq)
36.29 |-> (fn eq => Specification.definition
36.30 (NONE, (Attrib.empty_binding, eq)))
37.1 --- a/src/HOL/Typerep.thy Fri Aug 27 15:36:02 2010 +0200
37.2 +++ b/src/HOL/Typerep.thy Fri Aug 27 19:34:23 2010 +0200
37.3 @@ -78,9 +78,13 @@
37.4 *}
37.5
37.6 lemma [code]:
37.7 - "eq_class.eq (Typerep tyco1 tys1) (Typerep tyco2 tys2) \<longleftrightarrow> eq_class.eq tyco1 tyco2
37.8 - \<and> list_all2 eq_class.eq tys1 tys2"
37.9 - by (auto simp add: equals_eq [symmetric] list_all2_eq [symmetric])
37.10 + "HOL.equal (Typerep tyco1 tys1) (Typerep tyco2 tys2) \<longleftrightarrow> HOL.equal tyco1 tyco2
37.11 + \<and> list_all2 HOL.equal tys1 tys2"
37.12 + by (auto simp add: eq_equal [symmetric] list_all2_eq [symmetric])
37.13 +
37.14 +lemma [code nbe]:
37.15 + "HOL.equal (x :: typerep) x \<longleftrightarrow> True"
37.16 + by (fact equal_refl)
37.17
37.18 code_type typerep
37.19 (Eval "Term.typ")
38.1 --- a/src/HOL/Word/Word.thy Fri Aug 27 15:36:02 2010 +0200
38.2 +++ b/src/HOL/Word/Word.thy Fri Aug 27 19:34:23 2010 +0200
38.3 @@ -953,14 +953,14 @@
38.4
38.5 text {* Executable equality *}
38.6
38.7 -instantiation word :: ("{len0}") eq
38.8 +instantiation word :: (len0) equal
38.9 begin
38.10
38.11 -definition eq_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool" where
38.12 - "eq_word k l \<longleftrightarrow> HOL.eq (uint k) (uint l)"
38.13 +definition equal_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool" where
38.14 + "equal_word k l \<longleftrightarrow> HOL.equal (uint k) (uint l)"
38.15
38.16 instance proof
38.17 -qed (simp add: eq eq_word_def)
38.18 +qed (simp add: equal equal_word_def)
38.19
38.20 end
38.21
39.1 --- a/src/HOL/ex/Numeral.thy Fri Aug 27 15:36:02 2010 +0200
39.2 +++ b/src/HOL/ex/Numeral.thy Fri Aug 27 19:34:23 2010 +0200
39.3 @@ -845,7 +845,7 @@
39.4 "(uminus :: int \<Rightarrow> int) = uminus"
39.5 "(op - :: int \<Rightarrow> int \<Rightarrow> int) = op -"
39.6 "(op * :: int \<Rightarrow> int \<Rightarrow> int) = op *"
39.7 - "(eq_class.eq :: int \<Rightarrow> int \<Rightarrow> bool) = eq_class.eq"
39.8 + "(HOL.equal :: int \<Rightarrow> int \<Rightarrow> bool) = HOL.equal"
39.9 "(op \<le> :: int \<Rightarrow> int \<Rightarrow> bool) = op \<le>"
39.10 "(op < :: int \<Rightarrow> int \<Rightarrow> bool) = op <"
39.11 by rule+
39.12 @@ -928,16 +928,20 @@
39.13 by simp_all
39.14
39.15 lemma eq_int_code [code]:
39.16 - "eq_class.eq 0 (0::int) \<longleftrightarrow> True"
39.17 - "eq_class.eq 0 (Pls l) \<longleftrightarrow> False"
39.18 - "eq_class.eq 0 (Mns l) \<longleftrightarrow> False"
39.19 - "eq_class.eq (Pls k) 0 \<longleftrightarrow> False"
39.20 - "eq_class.eq (Pls k) (Pls l) \<longleftrightarrow> eq_class.eq k l"
39.21 - "eq_class.eq (Pls k) (Mns l) \<longleftrightarrow> False"
39.22 - "eq_class.eq (Mns k) 0 \<longleftrightarrow> False"
39.23 - "eq_class.eq (Mns k) (Pls l) \<longleftrightarrow> False"
39.24 - "eq_class.eq (Mns k) (Mns l) \<longleftrightarrow> eq_class.eq k l"
39.25 - by (auto simp add: eq dest: sym)
39.26 + "HOL.equal 0 (0::int) \<longleftrightarrow> True"
39.27 + "HOL.equal 0 (Pls l) \<longleftrightarrow> False"
39.28 + "HOL.equal 0 (Mns l) \<longleftrightarrow> False"
39.29 + "HOL.equal (Pls k) 0 \<longleftrightarrow> False"
39.30 + "HOL.equal (Pls k) (Pls l) \<longleftrightarrow> HOL.equal k l"
39.31 + "HOL.equal (Pls k) (Mns l) \<longleftrightarrow> False"
39.32 + "HOL.equal (Mns k) 0 \<longleftrightarrow> False"
39.33 + "HOL.equal (Mns k) (Pls l) \<longleftrightarrow> False"
39.34 + "HOL.equal (Mns k) (Mns l) \<longleftrightarrow> HOL.equal k l"
39.35 + by (auto simp add: equal dest: sym)
39.36 +
39.37 +lemma [code nbe]:
39.38 + "HOL.equal (k::int) k \<longleftrightarrow> True"
39.39 + by (fact equal_refl)
39.40
39.41 lemma less_eq_int_code [code]:
39.42 "0 \<le> (0::int) \<longleftrightarrow> True"
39.43 @@ -1078,7 +1082,7 @@
39.44 (Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))")
39.45 (Eval "Integer.div'_mod/ (abs _)/ (abs _)")
39.46
39.47 -code_const "eq_class.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
39.48 +code_const "HOL.equal \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
39.49 (SML "!((_ : IntInf.int) = _)")
39.50 (OCaml "Big'_int.eq'_big'_int")
39.51 (Haskell infixl 4 "==")