--- a/NEWS Fri Aug 27 22:30:25 2010 +0200
+++ b/NEWS Sat Aug 28 11:42:33 2010 +0200
@@ -62,6 +62,10 @@
*** HOL ***
+* Renamed class eq and constant eq (for code generation) to class equal
+and constant equal, plus renaming of related facts and various tuning.
+INCOMPATIBILITY.
+
* Scala (2.8 or higher) has been added to the target languages of
the code generator.
--- a/doc-src/Codegen/Thy/Foundations.thy Fri Aug 27 22:30:25 2010 +0200
+++ b/doc-src/Codegen/Thy/Foundations.thy Sat Aug 28 11:42:33 2010 +0200
@@ -220,12 +220,12 @@
text {*
\noindent Obviously, polymorphic equality is implemented the Haskell
way using a type class. How is this achieved? HOL introduces an
- explicit class @{class eq} with a corresponding operation @{const
- eq_class.eq} such that @{thm eq [no_vars]}. The preprocessing
- framework does the rest by propagating the @{class eq} constraints
+ explicit class @{class equal} with a corresponding operation @{const
+ HOL.equal} such that @{thm equal [no_vars]}. The preprocessing
+ framework does the rest by propagating the @{class equal} constraints
through all dependent code equations. For datatypes, instances of
- @{class eq} are implicitly derived when possible. For other types,
- you may instantiate @{text eq} manually like any other type class.
+ @{class equal} are implicitly derived when possible. For other types,
+ you may instantiate @{text equal} manually like any other type class.
*}
--- a/src/HOL/Code_Evaluation.thy Fri Aug 27 22:30:25 2010 +0200
+++ b/src/HOL/Code_Evaluation.thy Sat Aug 28 11:42:33 2010 +0200
@@ -162,7 +162,7 @@
subsubsection {* Code generator setup *}
lemmas [code del] = term.recs term.cases term.size
-lemma [code, code del]: "eq_class.eq (t1\<Colon>term) t2 \<longleftrightarrow> eq_class.eq t1 t2" ..
+lemma [code, code del]: "HOL.equal (t1\<Colon>term) t2 \<longleftrightarrow> HOL.equal t1 t2" ..
lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
lemma [code, code del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
--- a/src/HOL/Code_Numeral.thy Fri Aug 27 22:30:25 2010 +0200
+++ b/src/HOL/Code_Numeral.thy Sat Aug 28 11:42:33 2010 +0200
@@ -115,12 +115,12 @@
lemmas [code del] = code_numeral.recs code_numeral.cases
lemma [code]:
- "eq_class.eq k l \<longleftrightarrow> eq_class.eq (nat_of k) (nat_of l)"
- by (cases k, cases l) (simp add: eq)
+ "HOL.equal k l \<longleftrightarrow> HOL.equal (nat_of k) (nat_of l)"
+ by (cases k, cases l) (simp add: equal)
lemma [code nbe]:
- "eq_class.eq (k::code_numeral) k \<longleftrightarrow> True"
- by (rule HOL.eq_refl)
+ "HOL.equal (k::code_numeral) k \<longleftrightarrow> True"
+ by (rule equal_refl)
subsection {* Code numerals as datatype of ints *}
@@ -301,7 +301,7 @@
(Haskell "Integer")
(Scala "BigInt")
-code_instance code_numeral :: eq
+code_instance code_numeral :: equal
(Haskell -)
setup {*
@@ -342,7 +342,7 @@
(Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))")
(Eval "!(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
-code_const "eq_class.eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
+code_const "HOL.equal \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
(SML "!((_ : Int.int) = _)")
(OCaml "Big'_int.eq'_big'_int")
(Haskell infixl 4 "==")
--- a/src/HOL/HOL.thy Fri Aug 27 22:30:25 2010 +0200
+++ b/src/HOL/HOL.thy Sat Aug 28 11:42:33 2010 +0200
@@ -1775,31 +1775,30 @@
subsubsection {* Equality *}
-class eq =
- fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
- assumes eq_equals: "eq x y \<longleftrightarrow> x = y"
+class equal =
+ fixes equal :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+ assumes equal_eq: "equal x y \<longleftrightarrow> x = y"
begin
-lemma eq [code_unfold, code_inline del]: "eq = (op =)"
- by (rule ext eq_equals)+
+lemma equal [code_unfold, code_inline del]: "equal = (op =)"
+ by (rule ext equal_eq)+
-lemma eq_refl: "eq x x \<longleftrightarrow> True"
- unfolding eq by rule+
+lemma equal_refl: "equal x x \<longleftrightarrow> True"
+ unfolding equal by rule+
-lemma equals_eq: "(op =) \<equiv> eq"
- by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals)
-
-declare equals_eq [symmetric, code_post]
+lemma eq_equal: "(op =) \<equiv> equal"
+ by (rule eq_reflection) (rule ext, rule ext, rule sym, rule equal_eq)
end
-declare equals_eq [code]
+declare eq_equal [symmetric, code_post]
+declare eq_equal [code]
setup {*
Code_Preproc.map_pre (fn simpset =>
- simpset addsimprocs [Simplifier.simproc_global_i @{theory} "eq" [@{term "op ="}]
+ simpset addsimprocs [Simplifier.simproc_global_i @{theory} "equal" [@{term "op ="}]
(fn thy => fn _ => fn Const (_, T) => case strip_type T
- of (Type _ :: _, _) => SOME @{thm equals_eq}
+ of (Type _ :: _, _) => SOME @{thm eq_equal}
| _ => NONE)])
*}
@@ -1839,50 +1838,50 @@
and "(P \<longrightarrow> False) \<longleftrightarrow> \<not> P"
and "(P \<longrightarrow> True) \<longleftrightarrow> True" by simp_all
-instantiation itself :: (type) eq
+instantiation itself :: (type) equal
begin
-definition eq_itself :: "'a itself \<Rightarrow> 'a itself \<Rightarrow> bool" where
- "eq_itself x y \<longleftrightarrow> x = y"
+definition equal_itself :: "'a itself \<Rightarrow> 'a itself \<Rightarrow> bool" where
+ "equal_itself x y \<longleftrightarrow> x = y"
instance proof
-qed (fact eq_itself_def)
+qed (fact equal_itself_def)
end
-lemma eq_itself_code [code]:
- "eq_class.eq TYPE('a) TYPE('a) \<longleftrightarrow> True"
- by (simp add: eq)
+lemma equal_itself_code [code]:
+ "equal TYPE('a) TYPE('a) \<longleftrightarrow> True"
+ by (simp add: equal)
text {* Equality *}
declare simp_thms(6) [code nbe]
setup {*
- Sign.add_const_constraint (@{const_name eq}, SOME @{typ "'a\<Colon>type \<Rightarrow> 'a \<Rightarrow> bool"})
+ Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a\<Colon>type \<Rightarrow> 'a \<Rightarrow> bool"})
*}
-lemma equals_alias_cert: "OFCLASS('a, eq_class) \<equiv> ((op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool) \<equiv> eq)" (is "?ofclass \<equiv> ?eq")
+lemma equal_alias_cert: "OFCLASS('a, equal_class) \<equiv> ((op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool) \<equiv> equal)" (is "?ofclass \<equiv> ?equal")
proof
assume "PROP ?ofclass"
- show "PROP ?eq"
- by (tactic {* ALLGOALS (rtac (Thm.unconstrainT @{thm equals_eq})) *})
+ show "PROP ?equal"
+ by (tactic {* ALLGOALS (rtac (Thm.unconstrainT @{thm eq_equal})) *})
(fact `PROP ?ofclass`)
next
- assume "PROP ?eq"
+ assume "PROP ?equal"
show "PROP ?ofclass" proof
- qed (simp add: `PROP ?eq`)
+ qed (simp add: `PROP ?equal`)
qed
setup {*
- Sign.add_const_constraint (@{const_name eq}, SOME @{typ "'a\<Colon>eq \<Rightarrow> 'a \<Rightarrow> bool"})
+ Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a\<Colon>equal \<Rightarrow> 'a \<Rightarrow> bool"})
*}
setup {*
- Nbe.add_const_alias @{thm equals_alias_cert}
+ Nbe.add_const_alias @{thm equal_alias_cert}
*}
-hide_const (open) eq
+hide_const (open) equal
text {* Cases *}
@@ -1939,10 +1938,10 @@
text {* using built-in Haskell equality *}
-code_class eq
+code_class equal
(Haskell "Eq")
-code_const "eq_class.eq"
+code_const "HOL.equal"
(Haskell infixl 4 "==")
code_const "op ="
--- a/src/HOL/Int.thy Fri Aug 27 22:30:25 2010 +0200
+++ b/src/HOL/Int.thy Sat Aug 28 11:42:33 2010 +0200
@@ -2222,42 +2222,42 @@
mult_bin_simps
arith_extra_simps(4) [where 'a = int]
-instantiation int :: eq
+instantiation int :: equal
begin
definition
- "eq_class.eq k l \<longleftrightarrow> k - l = (0\<Colon>int)"
-
-instance by default (simp add: eq_int_def)
+ "HOL.equal k l \<longleftrightarrow> k - l = (0\<Colon>int)"
+
+instance by default (simp add: equal_int_def)
end
lemma eq_number_of_int_code [code]:
- "eq_class.eq (number_of k \<Colon> int) (number_of l) \<longleftrightarrow> eq_class.eq k l"
- unfolding eq_int_def number_of_is_id ..
+ "HOL.equal (number_of k \<Colon> int) (number_of l) \<longleftrightarrow> HOL.equal k l"
+ unfolding equal_int_def number_of_is_id ..
lemma eq_int_code [code]:
- "eq_class.eq Int.Pls Int.Pls \<longleftrightarrow> True"
- "eq_class.eq Int.Pls Int.Min \<longleftrightarrow> False"
- "eq_class.eq Int.Pls (Int.Bit0 k2) \<longleftrightarrow> eq_class.eq Int.Pls k2"
- "eq_class.eq Int.Pls (Int.Bit1 k2) \<longleftrightarrow> False"
- "eq_class.eq Int.Min Int.Pls \<longleftrightarrow> False"
- "eq_class.eq Int.Min Int.Min \<longleftrightarrow> True"
- "eq_class.eq Int.Min (Int.Bit0 k2) \<longleftrightarrow> False"
- "eq_class.eq Int.Min (Int.Bit1 k2) \<longleftrightarrow> eq_class.eq Int.Min k2"
- "eq_class.eq (Int.Bit0 k1) Int.Pls \<longleftrightarrow> eq_class.eq k1 Int.Pls"
- "eq_class.eq (Int.Bit1 k1) Int.Pls \<longleftrightarrow> False"
- "eq_class.eq (Int.Bit0 k1) Int.Min \<longleftrightarrow> False"
- "eq_class.eq (Int.Bit1 k1) Int.Min \<longleftrightarrow> eq_class.eq k1 Int.Min"
- "eq_class.eq (Int.Bit0 k1) (Int.Bit0 k2) \<longleftrightarrow> eq_class.eq k1 k2"
- "eq_class.eq (Int.Bit0 k1) (Int.Bit1 k2) \<longleftrightarrow> False"
- "eq_class.eq (Int.Bit1 k1) (Int.Bit0 k2) \<longleftrightarrow> False"
- "eq_class.eq (Int.Bit1 k1) (Int.Bit1 k2) \<longleftrightarrow> eq_class.eq k1 k2"
- unfolding eq_equals by simp_all
+ "HOL.equal Int.Pls Int.Pls \<longleftrightarrow> True"
+ "HOL.equal Int.Pls Int.Min \<longleftrightarrow> False"
+ "HOL.equal Int.Pls (Int.Bit0 k2) \<longleftrightarrow> HOL.equal Int.Pls k2"
+ "HOL.equal Int.Pls (Int.Bit1 k2) \<longleftrightarrow> False"
+ "HOL.equal Int.Min Int.Pls \<longleftrightarrow> False"
+ "HOL.equal Int.Min Int.Min \<longleftrightarrow> True"
+ "HOL.equal Int.Min (Int.Bit0 k2) \<longleftrightarrow> False"
+ "HOL.equal Int.Min (Int.Bit1 k2) \<longleftrightarrow> HOL.equal Int.Min k2"
+ "HOL.equal (Int.Bit0 k1) Int.Pls \<longleftrightarrow> HOL.equal k1 Int.Pls"
+ "HOL.equal (Int.Bit1 k1) Int.Pls \<longleftrightarrow> False"
+ "HOL.equal (Int.Bit0 k1) Int.Min \<longleftrightarrow> False"
+ "HOL.equal (Int.Bit1 k1) Int.Min \<longleftrightarrow> HOL.equal k1 Int.Min"
+ "HOL.equal (Int.Bit0 k1) (Int.Bit0 k2) \<longleftrightarrow> HOL.equal k1 k2"
+ "HOL.equal (Int.Bit0 k1) (Int.Bit1 k2) \<longleftrightarrow> False"
+ "HOL.equal (Int.Bit1 k1) (Int.Bit0 k2) \<longleftrightarrow> False"
+ "HOL.equal (Int.Bit1 k1) (Int.Bit1 k2) \<longleftrightarrow> HOL.equal k1 k2"
+ unfolding equal_eq by simp_all
lemma eq_int_refl [code nbe]:
- "eq_class.eq (k::int) k \<longleftrightarrow> True"
- by (rule HOL.eq_refl)
+ "HOL.equal (k::int) k \<longleftrightarrow> True"
+ by (rule equal_refl)
lemma less_eq_number_of_int_code [code]:
"(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
--- a/src/HOL/Lazy_Sequence.thy Fri Aug 27 22:30:25 2010 +0200
+++ b/src/HOL/Lazy_Sequence.thy Sat Aug 28 11:42:33 2010 +0200
@@ -39,10 +39,14 @@
"size xq = (case yield xq of None => 0 | Some (x, xq') => size xq' + 1)"
by (cases xq) auto
-lemma [code]: "eq_class.eq xq yq = (case (yield xq, yield yq) of
- (None, None) => True | (Some (x, xq'), Some (y, yq')) => (HOL.eq x y) \<and> (eq_class.eq xq yq) | _ => False)"
-apply (cases xq) apply (cases yq) apply (auto simp add: eq_class.eq_equals)
-apply (cases yq) apply (auto simp add: eq_class.eq_equals) done
+lemma [code]: "HOL.equal xq yq = (case (yield xq, yield yq) of
+ (None, None) => True | (Some (x, xq'), Some (y, yq')) => (HOL.equal x y) \<and> (HOL.equal xq yq) | _ => False)"
+apply (cases xq) apply (cases yq) apply (auto simp add: equal_eq)
+apply (cases yq) apply (auto simp add: equal_eq) done
+
+lemma [code nbe]:
+ "HOL.equal (x :: 'a lazy_sequence) x \<longleftrightarrow> True"
+ by (fact equal_refl)
lemma seq_case [code]:
"lazy_sequence_case f g xq = (case (yield xq) of None => f | Some (x, xq') => g x xq')"
--- a/src/HOL/Library/AssocList.thy Fri Aug 27 22:30:25 2010 +0200
+++ b/src/HOL/Library/AssocList.thy Sat Aug 28 11:42:33 2010 +0200
@@ -701,7 +701,44 @@
"Mapping.bulkload vs = Mapping (map (\<lambda>n. (n, vs ! n)) [0..<length vs])"
by (rule mapping_eqI) (simp add: map_of_map_restrict expand_fun_eq)
-lemma [code, code del]:
- "HOL.eq (x :: (_, _) mapping) y \<longleftrightarrow> x = y" by (fact eq_equals) (*FIXME*)
+lemma map_of_eqI: (*FIXME move to Map.thy*)
+ assumes set_eq: "set (map fst xs) = set (map fst ys)"
+ assumes map_eq: "\<forall>k\<in>set (map fst xs). map_of xs k = map_of ys k"
+ shows "map_of xs = map_of ys"
+proof (rule ext)
+ fix k show "map_of xs k = map_of ys k"
+ proof (cases "map_of xs k")
+ case None then have "k \<notin> set (map fst xs)" by (simp add: map_of_eq_None_iff)
+ with set_eq have "k \<notin> set (map fst ys)" by simp
+ then have "map_of ys k = None" by (simp add: map_of_eq_None_iff)
+ with None show ?thesis by simp
+ next
+ case (Some v) then have "k \<in> set (map fst xs)" by (auto simp add: dom_map_of_conv_image_fst [symmetric])
+ with map_eq show ?thesis by auto
+ qed
+qed
+
+lemma map_of_eq_dom: (*FIXME move to Map.thy*)
+ assumes "map_of xs = map_of ys"
+ shows "fst ` set xs = fst ` set ys"
+proof -
+ from assms have "dom (map_of xs) = dom (map_of ys)" by simp
+ then show ?thesis by (simp add: dom_map_of_conv_image_fst)
+qed
+
+lemma equal_Mapping [code]:
+ "HOL.equal (Mapping xs) (Mapping ys) \<longleftrightarrow>
+ (let ks = map fst xs; ls = map fst ys
+ 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))"
+proof -
+ 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)
+ show ?thesis
+ by (auto intro!: map_of_eqI simp add: Let_def equal Mapping_def)
+ (auto dest!: map_of_eq_dom intro: aux)
+qed
+
+lemma [code nbe]:
+ "HOL.equal (x :: ('a, 'b) mapping) x \<longleftrightarrow> True"
+ by (fact equal_refl)
end
--- a/src/HOL/Library/Code_Char.thy Fri Aug 27 22:30:25 2010 +0200
+++ b/src/HOL/Library/Code_Char.thy Sat Aug 28 11:42:33 2010 +0200
@@ -19,7 +19,7 @@
#> String_Code.add_literal_list_string "Haskell"
*}
-code_instance char :: eq
+code_instance char :: equal
(Haskell -)
code_reserved SML
@@ -31,7 +31,7 @@
code_reserved Scala
char
-code_const "eq_class.eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
+code_const "HOL.equal \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
(SML "!((_ : char) = _)")
(OCaml "!((_ : char) = _)")
(Haskell infixl 4 "==")
--- a/src/HOL/Library/Code_Integer.thy Fri Aug 27 22:30:25 2010 +0200
+++ b/src/HOL/Library/Code_Integer.thy Sat Aug 28 11:42:33 2010 +0200
@@ -21,7 +21,7 @@
(Scala "BigInt")
(Eval "int")
-code_instance int :: eq
+code_instance int :: equal
(Haskell -)
setup {*
@@ -96,7 +96,7 @@
(Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))")
(Eval "Integer.div'_mod/ (abs _)/ (abs _)")
-code_const "eq_class.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
+code_const "HOL.equal \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
(SML "!((_ : IntInf.int) = _)")
(OCaml "Big'_int.eq'_big'_int")
(Haskell infixl 4 "==")
--- a/src/HOL/Library/Code_Natural.thy Fri Aug 27 22:30:25 2010 +0200
+++ b/src/HOL/Library/Code_Natural.thy Sat Aug 28 11:42:33 2010 +0200
@@ -112,7 +112,7 @@
false Code_Printer.literal_alternative_numeral) ["Haskell", "Scala"]
*}
-code_instance code_numeral :: eq
+code_instance code_numeral :: equal
(Haskell -)
code_const "op + \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
@@ -131,7 +131,7 @@
(Haskell "divMod")
(Scala infixl 8 "/%")
-code_const "eq_class.eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
+code_const "HOL.equal \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
(Haskell infixl 4 "==")
(Scala infixl 5 "==")
--- a/src/HOL/Library/Dlist.thy Fri Aug 27 22:30:25 2010 +0200
+++ b/src/HOL/Library/Dlist.thy Sat Aug 28 11:42:33 2010 +0200
@@ -109,16 +109,20 @@
text {* Equality *}
-instantiation dlist :: (eq) eq
+instantiation dlist :: (equal) equal
begin
-definition "HOL.eq dxs dys \<longleftrightarrow> HOL.eq (list_of_dlist dxs) (list_of_dlist dys)"
+definition "HOL.equal dxs dys \<longleftrightarrow> HOL.equal (list_of_dlist dxs) (list_of_dlist dys)"
instance proof
-qed (simp add: eq_dlist_def eq list_of_dlist_inject)
+qed (simp add: equal_dlist_def equal list_of_dlist_inject)
end
+lemma [code nbe]:
+ "HOL.equal (dxs :: 'a::equal dlist) dxs \<longleftrightarrow> True"
+ by (fact equal_refl)
+
section {* Induction principle and case distinction *}
--- a/src/HOL/Library/Efficient_Nat.thy Fri Aug 27 22:30:25 2010 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy Sat Aug 28 11:42:33 2010 +0200
@@ -55,12 +55,12 @@
by (simp add: prod_fun_def split_def pdivmod_def nat_div_distrib nat_mod_distrib divmod_nat_div_mod)
lemma eq_nat_code [code]:
- "eq_class.eq n m \<longleftrightarrow> eq_class.eq (of_nat n \<Colon> int) (of_nat m)"
- by (simp add: eq)
+ "HOL.equal n m \<longleftrightarrow> HOL.equal (of_nat n \<Colon> int) (of_nat m)"
+ by (simp add: equal)
lemma eq_nat_refl [code nbe]:
- "eq_class.eq (n::nat) n \<longleftrightarrow> True"
- by (rule HOL.eq_refl)
+ "HOL.equal (n::nat) n \<longleftrightarrow> True"
+ by (rule equal_refl)
lemma less_eq_nat_code [code]:
"n \<le> m \<longleftrightarrow> (of_nat n \<Colon> int) \<le> of_nat m"
@@ -332,7 +332,7 @@
(Haskell "Nat.Nat")
(Scala "Nat.Nat")
-code_instance nat :: eq
+code_instance nat :: equal
(Haskell -)
text {*
@@ -442,7 +442,7 @@
(Scala infixl 8 "/%")
(Eval "Integer.div'_mod")
-code_const "eq_class.eq \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
+code_const "HOL.equal \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
(SML "!((_ : IntInf.int) = _)")
(OCaml "Big'_int.eq'_big'_int")
(Haskell infixl 4 "==")
--- a/src/HOL/Library/Enum.thy Fri Aug 27 22:30:25 2010 +0200
+++ b/src/HOL/Library/Enum.thy Sat Aug 28 11:42:33 2010 +0200
@@ -35,17 +35,21 @@
subsection {* Equality and order on functions *}
-instantiation "fun" :: (enum, eq) eq
+instantiation "fun" :: (enum, equal) equal
begin
definition
- "eq_class.eq f g \<longleftrightarrow> (\<forall>x \<in> set enum. f x = g x)"
+ "HOL.equal f g \<longleftrightarrow> (\<forall>x \<in> set enum. f x = g x)"
instance proof
-qed (simp_all add: eq_fun_def enum_all expand_fun_eq)
+qed (simp_all add: equal_fun_def enum_all expand_fun_eq)
end
+lemma [code nbe]:
+ "HOL.equal (f :: _ \<Rightarrow> _) f \<longleftrightarrow> True"
+ by (fact equal_refl)
+
lemma order_fun [code]:
fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>order"
shows "f \<le> g \<longleftrightarrow> list_all (\<lambda>x. f x \<le> g x) enum"
@@ -169,7 +173,7 @@
end
-lemma enum_fun_code [code]: "enum = (let enum_a = (enum \<Colon> 'a\<Colon>{enum, eq} list)
+lemma enum_fun_code [code]: "enum = (let enum_a = (enum \<Colon> 'a\<Colon>{enum, equal} list)
in map (\<lambda>ys. the o map_of (zip enum_a ys)) (n_lists (length enum_a) enum))"
by (simp add: enum_fun_def Let_def)
--- a/src/HOL/Library/Fset.thy Fri Aug 27 22:30:25 2010 +0200
+++ b/src/HOL/Library/Fset.thy Sat Aug 28 11:42:33 2010 +0200
@@ -227,17 +227,21 @@
"A < B \<longleftrightarrow> A \<le> B \<and> \<not> B \<le> (A :: 'a fset)"
by (fact less_le_not_le)
-instantiation fset :: (type) eq
+instantiation fset :: (type) equal
begin
definition
- "eq_fset A B \<longleftrightarrow> A \<le> B \<and> B \<le> (A :: 'a fset)"
+ "HOL.equal A B \<longleftrightarrow> A \<le> B \<and> B \<le> (A :: 'a fset)"
instance proof
-qed (simp add: eq_fset_def set_eq [symmetric])
+qed (simp add: equal_fset_def set_eq [symmetric])
end
+lemma [code nbe]:
+ "HOL.equal (A :: 'a fset) A \<longleftrightarrow> True"
+ by (fact equal_refl)
+
subsection {* Functorial operations *}
--- a/src/HOL/Library/List_Prefix.thy Fri Aug 27 22:30:25 2010 +0200
+++ b/src/HOL/Library/List_Prefix.thy Sat Aug 28 11:42:33 2010 +0200
@@ -81,9 +81,9 @@
by (auto simp add: prefix_def)
lemma less_eq_list_code [code]:
- "([]\<Colon>'a\<Colon>{eq, ord} list) \<le> xs \<longleftrightarrow> True"
- "(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> [] \<longleftrightarrow> False"
- "(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> y # ys \<longleftrightarrow> x = y \<and> xs \<le> ys"
+ "([]\<Colon>'a\<Colon>{equal, ord} list) \<le> xs \<longleftrightarrow> True"
+ "(x\<Colon>'a\<Colon>{equal, ord}) # xs \<le> [] \<longleftrightarrow> False"
+ "(x\<Colon>'a\<Colon>{equal, ord}) # xs \<le> y # ys \<longleftrightarrow> x = y \<and> xs \<le> ys"
by simp_all
lemma same_prefix_prefix [simp]: "(xs @ ys \<le> xs @ zs) = (ys \<le> zs)"
--- a/src/HOL/Library/List_lexord.thy Fri Aug 27 22:30:25 2010 +0200
+++ b/src/HOL/Library/List_lexord.thy Sat Aug 28 11:42:33 2010 +0200
@@ -103,15 +103,15 @@
end
lemma less_list_code [code]:
- "xs < ([]\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> False"
- "[] < (x\<Colon>'a\<Colon>{eq, order}) # xs \<longleftrightarrow> True"
- "(x\<Colon>'a\<Colon>{eq, order}) # xs < y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs < ys"
+ "xs < ([]\<Colon>'a\<Colon>{equal, order} list) \<longleftrightarrow> False"
+ "[] < (x\<Colon>'a\<Colon>{equal, order}) # xs \<longleftrightarrow> True"
+ "(x\<Colon>'a\<Colon>{equal, order}) # xs < y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs < ys"
by simp_all
lemma less_eq_list_code [code]:
- "x # xs \<le> ([]\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> False"
- "[] \<le> (xs\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> True"
- "(x\<Colon>'a\<Colon>{eq, order}) # xs \<le> y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs \<le> ys"
+ "x # xs \<le> ([]\<Colon>'a\<Colon>{equal, order} list) \<longleftrightarrow> False"
+ "[] \<le> (xs\<Colon>'a\<Colon>{equal, order} list) \<longleftrightarrow> True"
+ "(x\<Colon>'a\<Colon>{equal, order}) # xs \<le> y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs \<le> ys"
by simp_all
end
--- a/src/HOL/Library/Mapping.thy Fri Aug 27 22:30:25 2010 +0200
+++ b/src/HOL/Library/Mapping.thy Sat Aug 28 11:42:33 2010 +0200
@@ -280,14 +280,14 @@
code_datatype empty update
-instantiation mapping :: (type, type) eq
+instantiation mapping :: (type, type) equal
begin
definition [code del]:
- "HOL.eq m n \<longleftrightarrow> lookup m = lookup n"
+ "HOL.equal m n \<longleftrightarrow> lookup m = lookup n"
instance proof
-qed (simp add: eq_mapping_def)
+qed (simp add: equal_mapping_def)
end
--- a/src/HOL/Library/Multiset.thy Fri Aug 27 22:30:25 2010 +0200
+++ b/src/HOL/Library/Multiset.thy Sat Aug 28 11:42:33 2010 +0200
@@ -938,17 +938,21 @@
qed
qed
-instantiation multiset :: (eq) eq
+instantiation multiset :: (equal) equal
begin
definition
- "HOL.eq A B \<longleftrightarrow> (A::'a multiset) \<le> B \<and> B \<le> A"
+ "HOL.equal A B \<longleftrightarrow> (A::'a multiset) \<le> B \<and> B \<le> A"
instance proof
-qed (simp add: eq_multiset_def eq_iff)
+qed (simp add: equal_multiset_def eq_iff)
end
+lemma [code nbe]:
+ "HOL.equal (A :: 'a::equal multiset) A \<longleftrightarrow> True"
+ by (fact equal_refl)
+
definition (in term_syntax)
bagify :: "('a\<Colon>typerep \<times> nat) list \<times> (unit \<Rightarrow> Code_Evaluation.term)
\<Rightarrow> 'a multiset \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
--- a/src/HOL/Library/Nested_Environment.thy Fri Aug 27 22:30:25 2010 +0200
+++ b/src/HOL/Library/Nested_Environment.thy Sat Aug 28 11:42:33 2010 +0200
@@ -521,22 +521,21 @@
text {* Environments and code generation *}
lemma [code, code del]:
- fixes e1 e2 :: "('b\<Colon>eq, 'a\<Colon>eq, 'c\<Colon>eq) env"
- shows "eq_class.eq e1 e2 \<longleftrightarrow> eq_class.eq e1 e2" ..
+ "(HOL.equal :: (_, _, _) env \<Rightarrow> _) = HOL.equal" ..
-lemma eq_env_code [code]:
- fixes x y :: "'a\<Colon>eq"
- and f g :: "'c\<Colon>{eq, finite} \<Rightarrow> ('b\<Colon>eq, 'a, 'c) env option"
- shows "eq_class.eq (Env x f) (Env y g) \<longleftrightarrow>
- eq_class.eq x y \<and> (\<forall>z\<in>UNIV. case f z
+lemma equal_env_code [code]:
+ fixes x y :: "'a\<Colon>equal"
+ and f g :: "'c\<Colon>{equal, finite} \<Rightarrow> ('b\<Colon>equal, 'a, 'c) env option"
+ shows "HOL.equal (Env x f) (Env y g) \<longleftrightarrow>
+ HOL.equal x y \<and> (\<forall>z\<in>UNIV. case f z
of None \<Rightarrow> (case g z
of None \<Rightarrow> True | Some _ \<Rightarrow> False)
| Some a \<Rightarrow> (case g z
- of None \<Rightarrow> False | Some b \<Rightarrow> eq_class.eq a b))" (is ?env)
- and "eq_class.eq (Val a) (Val b) \<longleftrightarrow> eq_class.eq a b"
- and "eq_class.eq (Val a) (Env y g) \<longleftrightarrow> False"
- and "eq_class.eq (Env x f) (Val b) \<longleftrightarrow> False"
-proof (unfold eq)
+ of None \<Rightarrow> False | Some b \<Rightarrow> HOL.equal a b))" (is ?env)
+ and "HOL.equal (Val a) (Val b) \<longleftrightarrow> HOL.equal a b"
+ and "HOL.equal (Val a) (Env y g) \<longleftrightarrow> False"
+ and "HOL.equal (Env x f) (Val b) \<longleftrightarrow> False"
+proof (unfold equal)
have "f = g \<longleftrightarrow> (\<forall>z. case f z
of None \<Rightarrow> (case g z
of None \<Rightarrow> True | Some _ \<Rightarrow> False)
@@ -562,6 +561,10 @@
of None \<Rightarrow> False | Some b \<Rightarrow> a = b))" by simp
qed simp_all
+lemma [code nbe]:
+ "HOL.equal (x :: (_, _, _) env) x \<longleftrightarrow> True"
+ by (fact equal_refl)
+
lemma [code, code del]:
"(Code_Evaluation.term_of :: ('a::{term_of, type}, 'b::{term_of, type}, 'c::{term_of, type}) env \<Rightarrow> term) = Code_Evaluation.term_of" ..
--- a/src/HOL/Library/Polynomial.thy Fri Aug 27 22:30:25 2010 +0200
+++ b/src/HOL/Library/Polynomial.thy Sat Aug 28 11:42:33 2010 +0200
@@ -1505,23 +1505,27 @@
declare pCons_0_0 [code_post]
-instantiation poly :: ("{zero,eq}") eq
+instantiation poly :: ("{zero, equal}") equal
begin
definition
- "eq_class.eq (p::'a poly) q \<longleftrightarrow> p = q"
+ "HOL.equal (p::'a poly) q \<longleftrightarrow> p = q"
-instance
- by default (rule eq_poly_def)
+instance proof
+qed (rule equal_poly_def)
end
lemma eq_poly_code [code]:
- "eq_class.eq (0::_ poly) (0::_ poly) \<longleftrightarrow> True"
- "eq_class.eq (0::_ poly) (pCons b q) \<longleftrightarrow> eq_class.eq 0 b \<and> eq_class.eq 0 q"
- "eq_class.eq (pCons a p) (0::_ poly) \<longleftrightarrow> eq_class.eq a 0 \<and> eq_class.eq p 0"
- "eq_class.eq (pCons a p) (pCons b q) \<longleftrightarrow> eq_class.eq a b \<and> eq_class.eq p q"
-unfolding eq by simp_all
+ "HOL.equal (0::_ poly) (0::_ poly) \<longleftrightarrow> True"
+ "HOL.equal (0::_ poly) (pCons b q) \<longleftrightarrow> HOL.equal 0 b \<and> HOL.equal 0 q"
+ "HOL.equal (pCons a p) (0::_ poly) \<longleftrightarrow> HOL.equal a 0 \<and> HOL.equal p 0"
+ "HOL.equal (pCons a p) (pCons b q) \<longleftrightarrow> HOL.equal a b \<and> HOL.equal p q"
+ by (simp_all add: equal)
+
+lemma [code nbe]:
+ "HOL.equal (p :: _ poly) p \<longleftrightarrow> True"
+ by (fact equal_refl)
lemmas coeff_code [code] =
coeff_0 coeff_pCons_0 coeff_pCons_Suc
--- a/src/HOL/Library/Product_ord.thy Fri Aug 27 22:30:25 2010 +0200
+++ b/src/HOL/Library/Product_ord.thy Sat Aug 28 11:42:33 2010 +0200
@@ -22,8 +22,8 @@
end
lemma [code]:
- "(x1\<Colon>'a\<Colon>{ord, eq}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 \<le> y2"
- "(x1\<Colon>'a\<Colon>{ord, eq}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 < y2"
+ "(x1\<Colon>'a\<Colon>{ord, equal}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 \<le> y2"
+ "(x1\<Colon>'a\<Colon>{ord, equal}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 < y2"
unfolding prod_le_def prod_less_def by simp_all
instance prod :: (preorder, preorder) preorder proof
--- a/src/HOL/Library/RBT.thy Fri Aug 27 22:30:25 2010 +0200
+++ b/src/HOL/Library/RBT.thy Sat Aug 28 11:42:33 2010 +0200
@@ -222,12 +222,14 @@
"Mapping.bulkload vs = Mapping (bulkload (List.map (\<lambda>n. (n, vs ! n)) [0..<length vs]))"
by (rule mapping_eqI) (simp add: map_of_map_restrict expand_fun_eq)
-lemma [code, code del]:
- "HOL.eq (x :: (_, _) mapping) y \<longleftrightarrow> x = y" by (fact eq_equals) (*FIXME*)
+lemma equal_Mapping [code]:
+ "HOL.equal (Mapping t1) (Mapping t2) \<longleftrightarrow> entries t1 = entries t2"
+ by (simp add: equal Mapping_def entries_lookup)
-lemma eq_Mapping [code]:
- "HOL.eq (Mapping t1) (Mapping t2) \<longleftrightarrow> entries t1 = entries t2"
- by (simp add: eq Mapping_def entries_lookup)
+lemma [code nbe]:
+ "HOL.equal (x :: (_, _) mapping) x \<longleftrightarrow> True"
+ by (fact equal_refl)
+
hide_const (open) impl_of lookup empty insert delete
entries keys bulkload map_entry map fold
--- a/src/HOL/List.thy Fri Aug 27 22:30:25 2010 +0200
+++ b/src/HOL/List.thy Sat Aug 28 11:42:33 2010 +0200
@@ -4721,8 +4721,8 @@
by (simp add: null_def)
lemma equal_Nil_null [code_unfold]:
- "eq_class.eq xs [] \<longleftrightarrow> null xs"
- by (simp add: eq eq_Nil_null)
+ "HOL.equal xs [] \<longleftrightarrow> null xs"
+ by (simp add: equal eq_Nil_null)
definition maps :: "('a \<Rightarrow> 'b list) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
[code_post]: "maps f xs = concat (map f xs)"
@@ -4821,10 +4821,10 @@
(Haskell "[]")
(Scala "!Nil")
-code_instance list :: eq
+code_instance list :: equal
(Haskell -)
-code_const "eq_class.eq \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool"
+code_const "HOL.equal \<Colon> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
(Haskell infixl 4 "==")
code_reserved SML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Fri Aug 27 22:30:25 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Sat Aug 28 11:42:33 2010 +0200
@@ -202,7 +202,7 @@
(@{const_name "top_fun_inst.top_fun"}, "'a"),
(@{const_name "Pure.term"}, "'a"),
(@{const_name "top_class.top"}, "'a"),
- (@{const_name "eq_class.eq"}, "'a"),
+ (@{const_name "HOL.equal"}, "'a"),
(@{const_name "Quotient.Quot_True"}, "'a")(*,
(@{const_name "uminus"}, "'a"),
(@{const_name "Nat.size"}, "'a"),
@@ -237,7 +237,7 @@
@{const_name "top_fun_inst.top_fun"},
@{const_name "Pure.term"},
@{const_name "top_class.top"},
- @{const_name "eq_class.eq"},
+ @{const_name "HOL.equal"},
@{const_name "Quotient.Quot_True"}]
fun is_forbidden_mutant t =
--- a/src/HOL/Option.thy Fri Aug 27 22:30:25 2010 +0200
+++ b/src/HOL/Option.thy Sat Aug 28 11:42:33 2010 +0200
@@ -99,8 +99,8 @@
by (simp add: is_none_def)
lemma [code_unfold]:
- "eq_class.eq x None \<longleftrightarrow> is_none x"
- by (simp add: eq is_none_none)
+ "HOL.equal x None \<longleftrightarrow> is_none x"
+ by (simp add: equal is_none_none)
hide_const (open) is_none
@@ -116,10 +116,10 @@
(Haskell "Nothing" and "Just")
(Scala "!None" and "Some")
-code_instance option :: eq
+code_instance option :: equal
(Haskell -)
-code_const "eq_class.eq \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool"
+code_const "HOL.equal \<Colon> 'a option \<Rightarrow> 'a option \<Rightarrow> bool"
(Haskell infixl 4 "==")
code_reserved SML
--- a/src/HOL/Predicate.thy Fri Aug 27 22:30:25 2010 +0200
+++ b/src/HOL/Predicate.thy Sat Aug 28 11:42:33 2010 +0200
@@ -808,8 +808,12 @@
lemma eq_pred_code [code]:
fixes P Q :: "'a pred"
- shows "eq_class.eq P Q \<longleftrightarrow> P \<le> Q \<and> Q \<le> P"
- unfolding eq by auto
+ shows "HOL.equal P Q \<longleftrightarrow> P \<le> Q \<and> Q \<le> P"
+ by (auto simp add: equal)
+
+lemma [code nbe]:
+ "HOL.equal (x :: 'a pred) x \<longleftrightarrow> True"
+ by (fact equal_refl)
lemma [code]:
"pred_case f P = f (eval P)"
--- a/src/HOL/Product_Type.thy Fri Aug 27 22:30:25 2010 +0200
+++ b/src/HOL/Product_Type.thy Sat Aug 28 11:42:33 2010 +0200
@@ -21,17 +21,17 @@
-- "prefer plain propositional version"
lemma
- shows [code]: "eq_class.eq False P \<longleftrightarrow> \<not> P"
- and [code]: "eq_class.eq True P \<longleftrightarrow> P"
- and [code]: "eq_class.eq P False \<longleftrightarrow> \<not> P"
- and [code]: "eq_class.eq P True \<longleftrightarrow> P"
- and [code nbe]: "eq_class.eq P P \<longleftrightarrow> True"
- by (simp_all add: eq)
+ shows [code]: "HOL.equal False P \<longleftrightarrow> \<not> P"
+ and [code]: "HOL.equal True P \<longleftrightarrow> P"
+ and [code]: "HOL.equal P False \<longleftrightarrow> \<not> P"
+ and [code]: "HOL.equal P True \<longleftrightarrow> P"
+ and [code nbe]: "HOL.equal P P \<longleftrightarrow> True"
+ by (simp_all add: equal)
-code_const "eq_class.eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
+code_const "HOL.equal \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
(Haskell infixl 4 "==")
-code_instance bool :: eq
+code_instance bool :: equal
(Haskell -)
@@ -92,7 +92,7 @@
end
lemma [code]:
- "eq_class.eq (u\<Colon>unit) v \<longleftrightarrow> True" unfolding eq unit_eq [of u] unit_eq [of v] by rule+
+ "HOL.equal (u\<Colon>unit) v \<longleftrightarrow> True" unfolding equal unit_eq [of u] unit_eq [of v] by rule+
code_type unit
(SML "unit")
@@ -106,10 +106,10 @@
(Haskell "()")
(Scala "()")
-code_instance unit :: eq
+code_instance unit :: equal
(Haskell -)
-code_const "eq_class.eq \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
+code_const "HOL.equal \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
(Haskell infixl 4 "==")
code_reserved SML
@@ -277,10 +277,10 @@
(Haskell "!((_),/ (_))")
(Scala "!((_),/ (_))")
-code_instance prod :: eq
+code_instance prod :: equal
(Haskell -)
-code_const "eq_class.eq \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
+code_const "HOL.equal \<Colon> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
(Haskell infixl 4 "==")
types_code
--- a/src/HOL/Quickcheck.thy Fri Aug 27 22:30:25 2010 +0200
+++ b/src/HOL/Quickcheck.thy Sat Aug 28 11:42:33 2010 +0200
@@ -97,7 +97,7 @@
\<Rightarrow> Random.seed \<Rightarrow> (('a\<Colon>term_of \<Rightarrow> 'b\<Colon>typerep) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
"random_fun_lift f = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Evaluation.term_of f Random.split_seed"
-instantiation "fun" :: ("{eq, term_of}", random) random
+instantiation "fun" :: ("{equal, term_of}", random) random
begin
definition random_fun :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
--- a/src/HOL/Rat.thy Fri Aug 27 22:30:25 2010 +0200
+++ b/src/HOL/Rat.thy Sat Aug 28 11:42:33 2010 +0200
@@ -1083,18 +1083,18 @@
by (cases "0::int" a rule: linorder_cases) (simp_all add: quotient_of_Fract)
qed
-instantiation rat :: eq
+instantiation rat :: equal
begin
definition [code]:
- "eq_class.eq a b \<longleftrightarrow> quotient_of a = quotient_of b"
+ "HOL.equal a b \<longleftrightarrow> quotient_of a = quotient_of b"
instance proof
-qed (simp add: eq_rat_def quotient_of_inject_eq)
+qed (simp add: equal_rat_def quotient_of_inject_eq)
lemma rat_eq_refl [code nbe]:
- "eq_class.eq (r::rat) r \<longleftrightarrow> True"
- by (rule HOL.eq_refl)
+ "HOL.equal (r::rat) r \<longleftrightarrow> True"
+ by (rule equal_refl)
end
--- a/src/HOL/RealDef.thy Fri Aug 27 22:30:25 2010 +0200
+++ b/src/HOL/RealDef.thy Sat Aug 28 11:42:33 2010 +0200
@@ -1697,19 +1697,21 @@
"Ratreal (number_of r / number_of s) = number_of r / number_of s"
unfolding Ratreal_number_of_quotient [symmetric] Ratreal_def of_rat_divide ..
-instantiation real :: eq
+instantiation real :: equal
begin
-definition "eq_class.eq (x\<Colon>real) y \<longleftrightarrow> x - y = 0"
+definition "HOL.equal (x\<Colon>real) y \<longleftrightarrow> x - y = 0"
-instance by default (simp add: eq_real_def)
+instance proof
+qed (simp add: equal_real_def)
-lemma real_eq_code [code]: "eq_class.eq (Ratreal x) (Ratreal y) \<longleftrightarrow> eq_class.eq x y"
- by (simp add: eq_real_def eq)
+lemma real_equal_code [code]:
+ "HOL.equal (Ratreal x) (Ratreal y) \<longleftrightarrow> HOL.equal x y"
+ by (simp add: equal_real_def equal)
-lemma real_eq_refl [code nbe]:
- "eq_class.eq (x::real) x \<longleftrightarrow> True"
- by (rule HOL.eq_refl)
+lemma [code nbe]:
+ "HOL.equal (x::real) x \<longleftrightarrow> True"
+ by (rule equal_refl)
end
--- a/src/HOL/String.thy Fri Aug 27 22:30:25 2010 +0200
+++ b/src/HOL/String.thy Sat Aug 28 11:42:33 2010 +0200
@@ -183,10 +183,10 @@
fold String_Code.add_literal_string ["SML", "OCaml", "Haskell", "Scala"]
*}
-code_instance literal :: eq
+code_instance literal :: equal
(Haskell -)
-code_const "eq_class.eq \<Colon> literal \<Rightarrow> literal \<Rightarrow> bool"
+code_const "HOL.equal \<Colon> literal \<Rightarrow> literal \<Rightarrow> bool"
(SML "!((_ : string) = _)")
(OCaml "!((_ : string) = _)")
(Haskell infixl 4 "==")
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML Fri Aug 27 22:30:25 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Sat Aug 28 11:42:33 2010 +0200
@@ -68,7 +68,7 @@
val { descr, index, inject = inject_thms, distinct = distinct_thms, ... } =
Datatype_Data.the_info thy tyco;
val ty = Type (tyco, map TFree vs);
- fun mk_eq (t1, t2) = Const (@{const_name eq_class.eq}, ty --> ty --> HOLogic.boolT)
+ fun mk_eq (t1, t2) = Const (@{const_name HOL.equal}, ty --> ty --> HOLogic.boolT)
$ t1 $ t2;
fun true_eq t12 = HOLogic.mk_eq (mk_eq t12, HOLogic.true_const);
fun false_eq t12 = HOLogic.mk_eq (mk_eq t12, HOLogic.false_const);
@@ -83,7 +83,7 @@
val distincts = maps prep_distinct (snd (nth (Datatype_Prop.make_distincts [descr] vs) index));
val refl = HOLogic.mk_Trueprop (true_eq (Free ("x", ty), Free ("x", ty)));
val simpset = Simplifier.global_context thy (HOL_basic_ss addsimps
- (map Simpdata.mk_eq (@{thm eq} :: @{thm eq_True} :: inject_thms @ distinct_thms)));
+ (map Simpdata.mk_eq (@{thm equal} :: @{thm eq_True} :: inject_thms @ distinct_thms)));
fun prove prop = Skip_Proof.prove_global thy [] [] prop (K (ALLGOALS (simp_tac simpset)))
|> Simpdata.mk_eq;
in (map prove (triv_injects @ injects @ distincts), prove refl) end;
@@ -96,7 +96,7 @@
fun mk_side const_name = Const (const_name, ty --> ty --> HOLogic.boolT)
$ Free ("x", ty) $ Free ("y", ty);
val def = HOLogic.mk_Trueprop (HOLogic.mk_eq
- (mk_side @{const_name eq_class.eq}, mk_side @{const_name "op ="}));
+ (mk_side @{const_name HOL.equal}, mk_side @{const_name "op ="}));
val def' = Syntax.check_term lthy def;
val ((_, (_, thm)), lthy') = Specification.definition
(NONE, (Attrib.empty_binding, def')) lthy;
@@ -115,7 +115,7 @@
#> snd
in
thy
- |> Class.instantiation (tycos, vs, [HOLogic.class_eq])
+ |> Class.instantiation (tycos, vs, [HOLogic.class_equal])
|> fold_map add_def tycos
|-> (fn def_thms => Class.prove_instantiation_exit_result (map o Morphism.thm)
(fn _ => fn def_thms => tac def_thms) def_thms)
@@ -135,7 +135,7 @@
val case_rewrites = maps (#case_rewrites o Datatype_Data.the_info thy) tycos;
val certs = map (mk_case_cert thy) tycos;
val tycos_eq = filter_out
- (fn tyco => can (Sorts.mg_domain (Sign.classes_of thy) tyco) [HOLogic.class_eq]) tycos;
+ (fn tyco => can (Sorts.mg_domain (Sign.classes_of thy) tyco) [HOLogic.class_equal]) tycos;
in
if null css then thy
else thy
--- a/src/HOL/Tools/Nitpick/nitpick.ML Fri Aug 27 22:30:25 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Sat Aug 28 11:42:33 2010 +0200
@@ -182,7 +182,7 @@
fun none_true assigns = forall (not_equal (SOME true) o snd) assigns
val syntactic_sorts =
- @{sort "{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,eq}"} @
+ @{sort "{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,equal}"} @
@{sort number}
fun has_tfree_syntactic_sort (TFree (_, S as _ :: _)) =
subset (op =) (S, syntactic_sorts)
--- a/src/HOL/Tools/hologic.ML Fri Aug 27 22:30:25 2010 +0200
+++ b/src/HOL/Tools/hologic.ML Sat Aug 28 11:42:33 2010 +0200
@@ -49,7 +49,7 @@
val exists_const: typ -> term
val mk_exists: string * typ * term -> term
val choice_const: typ -> term
- val class_eq: string
+ val class_equal: string
val mk_binop: string -> term * term -> term
val mk_binrel: string -> term * term -> term
val dest_bin: string -> typ -> term -> term * term
@@ -251,7 +251,7 @@
fun choice_const T = Const("Hilbert_Choice.Eps", (T --> boolT) --> T);
-val class_eq = "HOL.eq";
+val class_equal = "HOL.equal";
(* binary operations and relations *)
--- a/src/HOL/Tools/record.ML Fri Aug 27 22:30:25 2010 +0200
+++ b/src/HOL/Tools/record.ML Sat Aug 28 11:42:33 2010 +0200
@@ -1844,7 +1844,7 @@
let
val eq =
(HOLogic.mk_Trueprop o HOLogic.mk_eq)
- (Const (@{const_name eq_class.eq}, extT --> extT --> HOLogic.boolT),
+ (Const (@{const_name HOL.equal}, extT --> extT --> HOLogic.boolT),
Const (@{const_name "op ="}, extT --> extT --> HOLogic.boolT));
fun tac eq_def =
Class.intro_classes_tac []
@@ -1853,15 +1853,15 @@
fun mk_eq thy eq_def = Simplifier.rewrite_rule
[(AxClass.unoverload thy o Thm.symmetric o Simpdata.mk_eq) eq_def] inject;
fun mk_eq_refl thy =
- @{thm HOL.eq_refl}
+ @{thm equal_refl}
|> Thm.instantiate
- ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT_global extT)], [])
+ ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort equal}), Logic.varifyT_global extT)], [])
|> AxClass.unoverload thy;
in
thy
|> Code.add_datatype [ext]
|> fold Code.add_default_eqn simps
- |> Class.instantiation ([ext_tyco], vs, [HOLogic.class_eq])
+ |> Class.instantiation ([ext_tyco], vs, [HOLogic.class_equal])
|> `(fn lthy => Syntax.check_term lthy eq)
|-> (fn eq => Specification.definition
(NONE, (Attrib.empty_binding, eq)))
--- a/src/HOL/Typerep.thy Fri Aug 27 22:30:25 2010 +0200
+++ b/src/HOL/Typerep.thy Sat Aug 28 11:42:33 2010 +0200
@@ -78,9 +78,13 @@
*}
lemma [code]:
- "eq_class.eq (Typerep tyco1 tys1) (Typerep tyco2 tys2) \<longleftrightarrow> eq_class.eq tyco1 tyco2
- \<and> list_all2 eq_class.eq tys1 tys2"
- by (auto simp add: equals_eq [symmetric] list_all2_eq [symmetric])
+ "HOL.equal (Typerep tyco1 tys1) (Typerep tyco2 tys2) \<longleftrightarrow> HOL.equal tyco1 tyco2
+ \<and> list_all2 HOL.equal tys1 tys2"
+ by (auto simp add: eq_equal [symmetric] list_all2_eq [symmetric])
+
+lemma [code nbe]:
+ "HOL.equal (x :: typerep) x \<longleftrightarrow> True"
+ by (fact equal_refl)
code_type typerep
(Eval "Term.typ")
--- a/src/HOL/Word/Word.thy Fri Aug 27 22:30:25 2010 +0200
+++ b/src/HOL/Word/Word.thy Sat Aug 28 11:42:33 2010 +0200
@@ -953,14 +953,14 @@
text {* Executable equality *}
-instantiation word :: ("{len0}") eq
+instantiation word :: (len0) equal
begin
-definition eq_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool" where
- "eq_word k l \<longleftrightarrow> HOL.eq (uint k) (uint l)"
+definition equal_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool" where
+ "equal_word k l \<longleftrightarrow> HOL.equal (uint k) (uint l)"
instance proof
-qed (simp add: eq eq_word_def)
+qed (simp add: equal equal_word_def)
end
--- a/src/HOL/ex/Numeral.thy Fri Aug 27 22:30:25 2010 +0200
+++ b/src/HOL/ex/Numeral.thy Sat Aug 28 11:42:33 2010 +0200
@@ -845,7 +845,7 @@
"(uminus :: int \<Rightarrow> int) = uminus"
"(op - :: int \<Rightarrow> int \<Rightarrow> int) = op -"
"(op * :: int \<Rightarrow> int \<Rightarrow> int) = op *"
- "(eq_class.eq :: int \<Rightarrow> int \<Rightarrow> bool) = eq_class.eq"
+ "(HOL.equal :: int \<Rightarrow> int \<Rightarrow> bool) = HOL.equal"
"(op \<le> :: int \<Rightarrow> int \<Rightarrow> bool) = op \<le>"
"(op < :: int \<Rightarrow> int \<Rightarrow> bool) = op <"
by rule+
@@ -928,16 +928,20 @@
by simp_all
lemma eq_int_code [code]:
- "eq_class.eq 0 (0::int) \<longleftrightarrow> True"
- "eq_class.eq 0 (Pls l) \<longleftrightarrow> False"
- "eq_class.eq 0 (Mns l) \<longleftrightarrow> False"
- "eq_class.eq (Pls k) 0 \<longleftrightarrow> False"
- "eq_class.eq (Pls k) (Pls l) \<longleftrightarrow> eq_class.eq k l"
- "eq_class.eq (Pls k) (Mns l) \<longleftrightarrow> False"
- "eq_class.eq (Mns k) 0 \<longleftrightarrow> False"
- "eq_class.eq (Mns k) (Pls l) \<longleftrightarrow> False"
- "eq_class.eq (Mns k) (Mns l) \<longleftrightarrow> eq_class.eq k l"
- by (auto simp add: eq dest: sym)
+ "HOL.equal 0 (0::int) \<longleftrightarrow> True"
+ "HOL.equal 0 (Pls l) \<longleftrightarrow> False"
+ "HOL.equal 0 (Mns l) \<longleftrightarrow> False"
+ "HOL.equal (Pls k) 0 \<longleftrightarrow> False"
+ "HOL.equal (Pls k) (Pls l) \<longleftrightarrow> HOL.equal k l"
+ "HOL.equal (Pls k) (Mns l) \<longleftrightarrow> False"
+ "HOL.equal (Mns k) 0 \<longleftrightarrow> False"
+ "HOL.equal (Mns k) (Pls l) \<longleftrightarrow> False"
+ "HOL.equal (Mns k) (Mns l) \<longleftrightarrow> HOL.equal k l"
+ by (auto simp add: equal dest: sym)
+
+lemma [code nbe]:
+ "HOL.equal (k::int) k \<longleftrightarrow> True"
+ by (fact equal_refl)
lemma less_eq_int_code [code]:
"0 \<le> (0::int) \<longleftrightarrow> True"
@@ -1078,7 +1082,7 @@
(Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))")
(Eval "Integer.div'_mod/ (abs _)/ (abs _)")
-code_const "eq_class.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
+code_const "HOL.equal \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
(SML "!((_ : IntInf.int) = _)")
(OCaml "Big'_int.eq'_big'_int")
(Haskell infixl 4 "==")
--- a/src/Tools/Code/code_scala.ML Fri Aug 27 22:30:25 2010 +0200
+++ b/src/Tools/Code/code_scala.ML Sat Aug 28 11:42:33 2010 +0200
@@ -444,18 +444,15 @@
(make_vars reserved) args_num is_singleton_constr;
(* print nodes *)
+ fun print_module base implicit_ps p = Pretty.chunks2
+ ([str ("object " ^ base ^ " {")]
+ @ (if null implicit_ps then [] else (single o Pretty.block)
+ (str "import /*implicits*/" :: Pretty.brk 1 :: commas implicit_ps))
+ @ [p, str ("} /* object " ^ base ^ " */")]);
fun print_implicit prefix_fragments implicit =
let
val s = deresolver prefix_fragments implicit;
in if length (Long_Name.explode s) = 1 then NONE else SOME (str s) end;
- fun print_implicits prefix_fragments implicits =
- case map_filter (print_implicit prefix_fragments) implicits
- of [] => NONE
- | ps => (SOME o Pretty.block)
- (str "import /*implicits*/" :: Pretty.brk 1 :: commas ps);
- fun print_module prefix_fragments base implicits p = Pretty.chunks2
- ([str ("object " ^ base ^ " {")] @ the_list (print_implicits prefix_fragments implicits)
- @ [p, str ("} /* object " ^ base ^ " */")]);
fun print_node _ (_, Dummy) = NONE
| print_node prefix_fragments (name, Stmt stmt) =
if null presentation_stmt_names
@@ -464,10 +461,14 @@
else NONE
| print_node prefix_fragments (name_fragment, Module (implicits, nodes)) =
if null presentation_stmt_names
- then case print_nodes (prefix_fragments @ [name_fragment]) nodes
- of NONE => NONE
- | SOME p => SOME (print_module prefix_fragments
- (Long_Name.base_name name_fragment) implicits p)
+ then
+ let
+ val prefix_fragments' = prefix_fragments @ [name_fragment];
+ in
+ Option.map (print_module name_fragment
+ (map_filter (print_implicit prefix_fragments') implicits))
+ (print_nodes prefix_fragments' nodes)
+ end
else print_nodes [] nodes
and print_nodes prefix_fragments nodes = let
val ps = map_filter (fn name => print_node prefix_fragments (name,
@@ -477,7 +478,7 @@
(* serialization *)
val p_includes = if null presentation_stmt_names
- then map (fn (base, p) => print_module [] base [] p) includes else [];
+ then map (fn (base, p) => print_module base [] p) includes else [];
val p = Pretty.chunks2 (p_includes @ the_list (print_nodes [] sca_program));
in
Code_Target.mk_serialization target