--- a/src/HOL/Code_Generator.thy Wed Nov 22 10:20:11 2006 +0100
+++ b/src/HOL/Code_Generator.thy Wed Nov 22 10:20:12 2006 +0100
@@ -192,13 +192,8 @@
subsubsection {* eq class *}
-class eq =
- fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
-
-defs
- eq_def [normal post]: "eq \<equiv> (op =)"
-
-lemmas [symmetric, code inline, code func] = eq_def
+axclass eq \<subseteq> type
+ attach "op ="
subsubsection {* bool type *}
@@ -206,36 +201,36 @@
instance bool :: eq ..
lemma [code func]:
- "eq True p = p" unfolding eq_def by auto
+ "True = P \<longleftrightarrow> P" by simp
lemma [code func]:
- "eq False p = (\<not> p)" unfolding eq_def by auto
+ "False = P \<longleftrightarrow> \<not> P" by simp
lemma [code func]:
- "eq p True = p" unfolding eq_def by auto
+ "P = True \<longleftrightarrow> P" by simp
lemma [code func]:
- "eq p False = (\<not> p)" unfolding eq_def by auto
+ "P = False \<longleftrightarrow> \<not> P" by simp
subsubsection {* Haskell *}
code_class eq
- (Haskell "Eq" where eq \<equiv> "(==)")
+ (Haskell "Eq" where "op =" \<equiv> "(==)")
-code_const eq
+code_const "op ="
(Haskell infixl 4 "==")
code_instance bool :: eq
(Haskell -)
-code_const "eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
+code_const "op = \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
(Haskell infixl 4 "==")
code_reserved Haskell
Eq eq
-hide (open) const eq if_delayed
+hide (open) const if_delayed
end
\ No newline at end of file
--- a/src/HOL/Datatype.thy Wed Nov 22 10:20:11 2006 +0100
+++ b/src/HOL/Datatype.thy Wed Nov 22 10:20:12 2006 +0100
@@ -799,7 +799,7 @@
code_instance option :: eq
(Haskell -)
-code_const "Code_Generator.eq \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool"
+code_const "op = \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool"
(Haskell infixl 4 "==")
code_reserved SML
--- a/src/HOL/Integ/IntDef.thy Wed Nov 22 10:20:11 2006 +0100
+++ b/src/HOL/Integ/IntDef.thy Wed Nov 22 10:20:12 2006 +0100
@@ -917,7 +917,7 @@
code_instance int :: eq
(Haskell -)
-code_const "Code_Generator.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
+code_const "op = \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
(SML "!((_ : IntInf.int) = _)")
(Haskell infixl 4 "==")
--- a/src/HOL/Integ/Presburger.thy Wed Nov 22 10:20:11 2006 +0100
+++ b/src/HOL/Integ/Presburger.thy Wed Nov 22 10:20:12 2006 +0100
@@ -1090,12 +1090,12 @@
text {* Code generator setup *}
text {*
- Presburger arithmetic is neccesary to prove some
+ Presburger arithmetic is necessary (at least convenient) to prove some
of the following code lemmas on integer numerals.
*}
lemma eq_number_of [code func]:
- "Code_Generator.eq ((number_of k)\<Colon>int) (number_of l) \<longleftrightarrow> Code_Generator.eq k l"
+ "((number_of k)\<Colon>int) = number_of l \<longleftrightarrow> k = l"
unfolding number_of_is_id ..
lemma less_eq_number_of [code func]:
@@ -1103,57 +1103,55 @@
unfolding number_of_is_id ..
lemma eq_Pls_Pls:
- "Code_Generator.eq Numeral.Pls Numeral.Pls"
- unfolding eq_def ..
+ "Numeral.Pls = Numeral.Pls" ..
lemma eq_Pls_Min:
- "\<not> Code_Generator.eq Numeral.Pls Numeral.Min"
- unfolding eq_def Pls_def Min_def by auto
+ "Numeral.Pls \<noteq> Numeral.Min"
+ unfolding Pls_def Min_def by auto
lemma eq_Pls_Bit0:
- "Code_Generator.eq Numeral.Pls (Numeral.Bit k bit.B0) \<longleftrightarrow> Code_Generator.eq Numeral.Pls k"
- unfolding eq_def Pls_def Bit_def bit.cases by auto
+ "Numeral.Pls = Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Pls = k"
+ unfolding Pls_def Bit_def bit.cases by auto
lemma eq_Pls_Bit1:
- "\<not> Code_Generator.eq Numeral.Pls (Numeral.Bit k bit.B1)"
- unfolding eq_def Pls_def Bit_def bit.cases by arith
+ "Numeral.Pls \<noteq> Numeral.Bit k bit.B1"
+ unfolding Pls_def Bit_def bit.cases by arith
lemma eq_Min_Pls:
- "\<not> Code_Generator.eq Numeral.Min Numeral.Pls"
- unfolding eq_def Pls_def Min_def by auto
+ "Numeral.Min \<noteq> Numeral.Pls"
+ unfolding Pls_def Min_def by auto
lemma eq_Min_Min:
- "Code_Generator.eq Numeral.Min Numeral.Min"
- unfolding eq_def ..
+ "Numeral.Min = Numeral.Min" ..
lemma eq_Min_Bit0:
- "\<not> Code_Generator.eq Numeral.Min (Numeral.Bit k bit.B0)"
- unfolding eq_def Min_def Bit_def bit.cases by arith
+ "Numeral.Min \<noteq> Numeral.Bit k bit.B0"
+ unfolding Min_def Bit_def bit.cases by arith
lemma eq_Min_Bit1:
- "Code_Generator.eq Numeral.Min (Numeral.Bit k bit.B1) \<longleftrightarrow> Code_Generator.eq Numeral.Min k"
- unfolding eq_def Min_def Bit_def bit.cases by auto
+ "Numeral.Min = Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Min = k"
+ unfolding Min_def Bit_def bit.cases by auto
lemma eq_Bit0_Pls:
- "Code_Generator.eq (Numeral.Bit k bit.B0) Numeral.Pls \<longleftrightarrow> Code_Generator.eq Numeral.Pls k"
- unfolding eq_def Pls_def Bit_def bit.cases by auto
+ "Numeral.Bit k bit.B0 = Numeral.Pls \<longleftrightarrow> Numeral.Pls = k"
+ unfolding Pls_def Bit_def bit.cases by auto
lemma eq_Bit1_Pls:
- "\<not> Code_Generator.eq (Numeral.Bit k bit.B1) Numeral.Pls"
- unfolding eq_def Pls_def Bit_def bit.cases by arith
+ "Numeral.Bit k bit.B1 \<noteq> Numeral.Pls"
+ unfolding Pls_def Bit_def bit.cases by arith
lemma eq_Bit0_Min:
- "\<not> Code_Generator.eq (Numeral.Bit k bit.B0) Numeral.Min"
- unfolding eq_def Min_def Bit_def bit.cases by arith
+ "Numeral.Bit k bit.B0 \<noteq> Numeral.Min"
+ unfolding Min_def Bit_def bit.cases by arith
lemma eq_Bit1_Min:
- "Code_Generator.eq (Numeral.Bit k bit.B1) Numeral.Min \<longleftrightarrow> Code_Generator.eq Numeral.Min k"
- unfolding eq_def Min_def Bit_def bit.cases by auto
+ "(Numeral.Bit k bit.B1) = Numeral.Min \<longleftrightarrow> Numeral.Min = k"
+ unfolding Min_def Bit_def bit.cases by auto
lemma eq_Bit_Bit:
- "Code_Generator.eq (Numeral.Bit k1 v1) (Numeral.Bit k2 v2) \<longleftrightarrow>
- Code_Generator.eq v1 v2 \<and> Code_Generator.eq k1 k2"
- unfolding eq_def Bit_def
+ "Numeral.Bit k1 v1 = Numeral.Bit k2 v2 \<longleftrightarrow>
+ v1 = v2 \<and> k1 = k2"
+ unfolding Bit_def
apply (cases v1)
apply (cases v2)
apply auto
--- a/src/HOL/Library/EfficientNat.thy Wed Nov 22 10:20:11 2006 +0100
+++ b/src/HOL/Library/EfficientNat.thy Wed Nov 22 10:20:12 2006 +0100
@@ -50,8 +50,8 @@
qed
lemma [code inline]:
- "nat_case f g n = (if Code_Generator.eq n 0 then f else g (nat_of_int (int n - 1)))"
- by (cases n) (simp_all add: eq_def nat_of_int_int)
+ "nat_case f g n = (if n = 0 then f else g (nat_of_int (int n - 1)))"
+ by (cases n) (simp_all add: nat_of_int_int)
text {*
Most standard arithmetic functions on natural numbers are implemented
@@ -97,8 +97,8 @@
by simp
lemma [code func, code inline]: "(m \<le> n) \<longleftrightarrow> (int m \<le> int n)"
by simp
-lemma [code func, code inline]: "Code_Generator.eq m n \<longleftrightarrow> Code_Generator.eq (int m) (int n)"
- unfolding eq_def by simp
+lemma [code func, code inline]: "m = n \<longleftrightarrow> int m = int n"
+ by simp
lemma [code func]: "nat k = (if k < 0 then 0 else nat_of_int k)"
proof (cases "k < 0")
case True then show ?thesis by simp
--- a/src/HOL/Library/ExecutableRat.thy Wed Nov 22 10:20:11 2006 +0100
+++ b/src/HOL/Library/ExecutableRat.thy Wed Nov 22 10:20:12 2006 +0100
@@ -121,7 +121,7 @@
"op * \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat" \<equiv> "op * \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat"
"inverse \<Colon> rat \<Rightarrow> rat" \<equiv> "inverse \<Colon> erat \<Rightarrow> erat"
"op \<le> \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" \<equiv> "op \<le> \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool"
- "Code_Generator.eq \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" \<equiv> eq_erat
+ "op = \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" \<equiv> eq_erat
code_const div_zero
(SML "raise/ (Fail/ \"Division by zero\")")
@@ -136,7 +136,7 @@
"op * \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat"
"inverse \<Colon> rat \<Rightarrow> rat"
"op \<le> \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool"
- "Code_Generator.eq \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool"
+ "op = \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool"
(SML *)
--- a/src/HOL/Library/ExecutableSet.thy Wed Nov 22 10:20:11 2006 +0100
+++ b/src/HOL/Library/ExecutableSet.thy Wed Nov 22 10:20:12 2006 +0100
@@ -32,10 +32,6 @@
by blast
lemma [code func]:
- "Code_Generator.eq A B \<longleftrightarrow> subset A B \<and> subset B A"
- unfolding eq_def subset_def by blast
-
-lemma [code func]:
"subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
unfolding subset_def Set.subset_def ..
--- a/src/HOL/Presburger.thy Wed Nov 22 10:20:11 2006 +0100
+++ b/src/HOL/Presburger.thy Wed Nov 22 10:20:12 2006 +0100
@@ -1090,12 +1090,12 @@
text {* Code generator setup *}
text {*
- Presburger arithmetic is neccesary to prove some
+ Presburger arithmetic is necessary (at least convenient) to prove some
of the following code lemmas on integer numerals.
*}
lemma eq_number_of [code func]:
- "Code_Generator.eq ((number_of k)\<Colon>int) (number_of l) \<longleftrightarrow> Code_Generator.eq k l"
+ "((number_of k)\<Colon>int) = number_of l \<longleftrightarrow> k = l"
unfolding number_of_is_id ..
lemma less_eq_number_of [code func]:
@@ -1103,57 +1103,55 @@
unfolding number_of_is_id ..
lemma eq_Pls_Pls:
- "Code_Generator.eq Numeral.Pls Numeral.Pls"
- unfolding eq_def ..
+ "Numeral.Pls = Numeral.Pls" ..
lemma eq_Pls_Min:
- "\<not> Code_Generator.eq Numeral.Pls Numeral.Min"
- unfolding eq_def Pls_def Min_def by auto
+ "Numeral.Pls \<noteq> Numeral.Min"
+ unfolding Pls_def Min_def by auto
lemma eq_Pls_Bit0:
- "Code_Generator.eq Numeral.Pls (Numeral.Bit k bit.B0) \<longleftrightarrow> Code_Generator.eq Numeral.Pls k"
- unfolding eq_def Pls_def Bit_def bit.cases by auto
+ "Numeral.Pls = Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Pls = k"
+ unfolding Pls_def Bit_def bit.cases by auto
lemma eq_Pls_Bit1:
- "\<not> Code_Generator.eq Numeral.Pls (Numeral.Bit k bit.B1)"
- unfolding eq_def Pls_def Bit_def bit.cases by arith
+ "Numeral.Pls \<noteq> Numeral.Bit k bit.B1"
+ unfolding Pls_def Bit_def bit.cases by arith
lemma eq_Min_Pls:
- "\<not> Code_Generator.eq Numeral.Min Numeral.Pls"
- unfolding eq_def Pls_def Min_def by auto
+ "Numeral.Min \<noteq> Numeral.Pls"
+ unfolding Pls_def Min_def by auto
lemma eq_Min_Min:
- "Code_Generator.eq Numeral.Min Numeral.Min"
- unfolding eq_def ..
+ "Numeral.Min = Numeral.Min" ..
lemma eq_Min_Bit0:
- "\<not> Code_Generator.eq Numeral.Min (Numeral.Bit k bit.B0)"
- unfolding eq_def Min_def Bit_def bit.cases by arith
+ "Numeral.Min \<noteq> Numeral.Bit k bit.B0"
+ unfolding Min_def Bit_def bit.cases by arith
lemma eq_Min_Bit1:
- "Code_Generator.eq Numeral.Min (Numeral.Bit k bit.B1) \<longleftrightarrow> Code_Generator.eq Numeral.Min k"
- unfolding eq_def Min_def Bit_def bit.cases by auto
+ "Numeral.Min = Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Min = k"
+ unfolding Min_def Bit_def bit.cases by auto
lemma eq_Bit0_Pls:
- "Code_Generator.eq (Numeral.Bit k bit.B0) Numeral.Pls \<longleftrightarrow> Code_Generator.eq Numeral.Pls k"
- unfolding eq_def Pls_def Bit_def bit.cases by auto
+ "Numeral.Bit k bit.B0 = Numeral.Pls \<longleftrightarrow> Numeral.Pls = k"
+ unfolding Pls_def Bit_def bit.cases by auto
lemma eq_Bit1_Pls:
- "\<not> Code_Generator.eq (Numeral.Bit k bit.B1) Numeral.Pls"
- unfolding eq_def Pls_def Bit_def bit.cases by arith
+ "Numeral.Bit k bit.B1 \<noteq> Numeral.Pls"
+ unfolding Pls_def Bit_def bit.cases by arith
lemma eq_Bit0_Min:
- "\<not> Code_Generator.eq (Numeral.Bit k bit.B0) Numeral.Min"
- unfolding eq_def Min_def Bit_def bit.cases by arith
+ "Numeral.Bit k bit.B0 \<noteq> Numeral.Min"
+ unfolding Min_def Bit_def bit.cases by arith
lemma eq_Bit1_Min:
- "Code_Generator.eq (Numeral.Bit k bit.B1) Numeral.Min \<longleftrightarrow> Code_Generator.eq Numeral.Min k"
- unfolding eq_def Min_def Bit_def bit.cases by auto
+ "(Numeral.Bit k bit.B1) = Numeral.Min \<longleftrightarrow> Numeral.Min = k"
+ unfolding Min_def Bit_def bit.cases by auto
lemma eq_Bit_Bit:
- "Code_Generator.eq (Numeral.Bit k1 v1) (Numeral.Bit k2 v2) \<longleftrightarrow>
- Code_Generator.eq v1 v2 \<and> Code_Generator.eq k1 k2"
- unfolding eq_def Bit_def
+ "Numeral.Bit k1 v1 = Numeral.Bit k2 v2 \<longleftrightarrow>
+ v1 = v2 \<and> k1 = k2"
+ unfolding Bit_def
apply (cases v1)
apply (cases v2)
apply auto
--- a/src/HOL/Product_Type.thy Wed Nov 22 10:20:11 2006 +0100
+++ b/src/HOL/Product_Type.thy Wed Nov 22 10:20:12 2006 +0100
@@ -776,7 +776,7 @@
instance unit :: eq ..
lemma [code func]:
- "Code_Generator.eq (u\<Colon>unit) v = True" unfolding eq_def unit_eq [of u] unit_eq [of v] by rule+
+ "(u\<Colon>unit) = v \<longleftrightarrow> True" unfolding unit_eq [of u] unit_eq [of v] by rule+
code_instance unit :: eq
(Haskell -)
@@ -784,16 +784,15 @@
instance * :: (eq, eq) eq ..
lemma [code func]:
- "Code_Generator.eq (x1, y1) (x2, y2) = (Code_Generator.eq x1 x2 \<and> Code_Generator.eq y1 y2)"
- unfolding eq_def by auto
+ "(x1\<Colon>'a\<Colon>eq, y1\<Colon>'b\<Colon>eq) = (x2, y2) \<longleftrightarrow> x1 = x2 \<and> y1 = y2" by auto
code_instance * :: eq
(Haskell -)
-code_const "Code_Generator.eq \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
+code_const "op = \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
(Haskell infixl 4 "==")
-code_const "Code_Generator.eq \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
+code_const "op = \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
(Haskell infixl 4 "==")
types_code
--- a/src/HOL/Sum_Type.thy Wed Nov 22 10:20:11 2006 +0100
+++ b/src/HOL/Sum_Type.thy Wed Nov 22 10:20:12 2006 +0100
@@ -197,20 +197,20 @@
instance "+" :: (eq, eq) eq ..
lemma [code func]:
- "Code_Generator.eq (Inl x) (Inl y) = Code_Generator.eq x y"
- unfolding eq_def Inl_eq ..
+ "(Inl x \<Colon> 'a\<Colon>eq + 'b\<Colon>eq) = Inl y \<longleftrightarrow> x = y"
+ unfolding Inl_eq ..
lemma [code func]:
- "Code_Generator.eq (Inr x) (Inr y) = Code_Generator.eq x y"
- unfolding eq_def Inr_eq ..
+ "(Inr x \<Colon> 'a\<Colon>eq + 'b\<Colon>eq) = Inr y \<longleftrightarrow> x = y"
+ unfolding Inr_eq ..
lemma [code func]:
- "Code_Generator.eq (Inl x) (Inr y) = False"
- unfolding eq_def using Inl_not_Inr by auto
+ "Inl (x\<Colon>'a\<Colon>eq) = Inr (y\<Colon>'b\<Colon>eq) \<longleftrightarrow> False"
+ using Inl_not_Inr by auto
lemma [code func]:
- "Code_Generator.eq (Inr x) (Inl y) = False"
- unfolding eq_def using Inr_not_Inl by auto
+ "Inr (x\<Colon>'b\<Colon>eq) = Inl (y\<Colon>'a\<Colon>eq) \<longleftrightarrow> False"
+ using Inr_not_Inl by auto
ML
{*
--- a/src/HOL/Tools/datatype_codegen.ML Wed Nov 22 10:20:11 2006 +0100
+++ b/src/HOL/Tools/datatype_codegen.ML Wed Nov 22 10:20:12 2006 +0100
@@ -489,7 +489,6 @@
| get_cert thy (false, dtco) = [TypecopyPackage.get_cert thy dtco];
local
- val eq_def_sym = thm "eq_def" |> Thm.symmetric;
fun get_eq_thms thy tyco = case DatatypePackage.get_datatype thy tyco
of SOME _ => get_eq_datatype thy tyco
| NONE => [TypecopyPackage.get_eq thy tyco];
@@ -498,7 +497,6 @@
get_eq_thms thy tyco
|> maps ((#mk o #mk_rews o snd o MetaSimplifier.rep_ss o Simplifier.simpset_of) thy)
|> HOL.constrain_op_eq_thms thy
- |> map (Tactic.rewrite_rule [eq_def_sym])
end;
type hook = (string * (bool * ((string * sort) list * (string * typ list) list))) list
@@ -605,7 +603,7 @@
let
val thy_ref = Theory.self_ref thy;
val ty = Type (dtco, map TFree vs) |> Logic.varifyT;
- val c = CodegenConsts.norm thy ("Code_Generator.eq", [ty]);
+ val c = CodegenConsts.norm thy ("op =", [ty]);
val get_thms = (fn () => get_eq (Theory.deref thy_ref) dtco |> rev);
in
CodegenData.add_funcl (c, CodegenData.lazy get_thms) thy