discontinued special treatment of op = vs. eq_class.eq
--- a/src/HOL/Code_Eval.thy Wed Sep 24 19:39:25 2008 +0200
+++ b/src/HOL/Code_Eval.thy Thu Sep 25 09:28:03 2008 +0200
@@ -135,7 +135,7 @@
subsubsection {* Code generator setup *}
lemmas [code func del] = term.recs term.cases term.size
-lemma [code func, code func del]: "(t1\<Colon>term) = t2 \<longleftrightarrow> t1 = t2" ..
+lemma [code func, code func del]: "eq_class.eq (t1\<Colon>term) t2 \<longleftrightarrow> eq_class.eq t1 t2" ..
lemma [code func, code func del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
lemma [code func, code func del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
--- a/src/HOL/Code_Setup.thy Wed Sep 24 19:39:25 2008 +0200
+++ b/src/HOL/Code_Setup.thy Thu Sep 25 09:28:03 2008 +0200
@@ -77,7 +77,10 @@
text {* using built-in Haskell equality *}
code_class eq
- (Haskell "Eq" where "op =" \<equiv> "(==)")
+ (Haskell "Eq" where "eq_class.eq" \<equiv> "(==)")
+
+code_const "eq_class.eq"
+ (Haskell infixl 4 "==")
code_const "op ="
(Haskell infixl 4 "==")
--- a/src/HOL/Datatype.thy Wed Sep 24 19:39:25 2008 +0200
+++ b/src/HOL/Datatype.thy Thu Sep 25 09:28:03 2008 +0200
@@ -686,7 +686,7 @@
code_instance option :: eq
(Haskell -)
-code_const "op = \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool"
+code_const "eq_class.eq \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool"
(Haskell infixl 4 "==")
code_reserved SML
--- a/src/HOL/HOL.thy Wed Sep 24 19:39:25 2008 +0200
+++ b/src/HOL/HOL.thy Thu Sep 25 09:28:03 2008 +0200
@@ -1710,16 +1710,24 @@
class eq = type +
fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
- assumes eq: "eq x y \<longleftrightarrow> x = y "
+ assumes eq_equals: "eq x y \<longleftrightarrow> x = y "
begin
+lemma eq: "eq = (op =)"
+ by (rule ext eq_equals)+
+
lemma equals_eq [code inline, code func]: "op = \<equiv> eq"
- by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq)
+ by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals)
declare equals_eq [symmetric, code post]
+lemma eq_refl: "eq x x \<longleftrightarrow> True"
+ unfolding eq by rule+
+
end
+declare simp_thms(6) [code nbe]
+
hide (open) const eq
hide const eq
--- a/src/HOL/Library/Code_Char.thy Wed Sep 24 19:39:25 2008 +0200
+++ b/src/HOL/Library/Code_Char.thy Thu Sep 25 09:28:03 2008 +0200
@@ -28,7 +28,7 @@
code_reserved OCaml
char
-code_const "op = \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
+code_const "eq_class.eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
(SML "!((_ : char) = _)")
(OCaml "!((_ : char) = _)")
(Haskell infixl 4 "==")
--- a/src/HOL/Library/Code_Index.thy Wed Sep 24 19:39:25 2008 +0200
+++ b/src/HOL/Library/Code_Index.thy Thu Sep 25 09:28:03 2008 +0200
@@ -111,8 +111,8 @@
qed
lemma [code func]:
- "k = l \<longleftrightarrow> nat_of_index k = nat_of_index l"
- by (cases k, cases l) simp
+ "eq_class.eq k l \<longleftrightarrow> eq_class.eq (nat_of_index k) (nat_of_index l)"
+ by (cases k, cases l) (simp add: eq)
subsection {* Indices as datatype of ints *}
@@ -319,7 +319,7 @@
(OCaml "(fun n -> fun m ->/ (n '/ m, n mod m))")
(Haskell "divMod")
-code_const "op = \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
+code_const "eq_class.eq \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
(SML "!((_ : Int.int) = _)")
(OCaml "!((_ : int) = _)")
(Haskell infixl 4 "==")
--- a/src/HOL/Library/Code_Integer.thy Wed Sep 24 19:39:25 2008 +0200
+++ b/src/HOL/Library/Code_Integer.thy Thu Sep 25 09:28:03 2008 +0200
@@ -72,7 +72,7 @@
(OCaml "Big'_int.mult'_big'_int")
(Haskell infixl 7 "*")
-code_const "op = \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
+code_const "eq_class.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
(SML "!((_ : IntInf.int) = _)")
(OCaml "Big'_int.eq'_big'_int")
(Haskell infixl 4 "==")
--- a/src/HOL/Library/Code_Message.thy Wed Sep 24 19:39:25 2008 +0200
+++ b/src/HOL/Library/Code_Message.thy Thu Sep 25 09:28:03 2008 +0200
@@ -50,7 +50,7 @@
code_instance message_string :: eq
(Haskell -)
-code_const "op = \<Colon> message_string \<Rightarrow> message_string \<Rightarrow> bool"
+code_const "eq_class.eq \<Colon> message_string \<Rightarrow> message_string \<Rightarrow> bool"
(SML "!((_ : string) = _)")
(OCaml "!((_ : string) = _)")
(Haskell infixl 4 "==")
--- a/src/HOL/Library/Efficient_Nat.thy Wed Sep 24 19:39:25 2008 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy Thu Sep 25 09:28:03 2008 +0200
@@ -400,7 +400,7 @@
(OCaml "Big'_int.quomod'_big'_int")
(Haskell "divMod")
-code_const "op = \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
+code_const "eq_class.eq \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
(SML "!((_ : IntInf.int) = _)")
(OCaml "Big'_int.eq'_big'_int")
(Haskell infixl 4 "==")
--- a/src/HOL/Library/RType.thy Wed Sep 24 19:39:25 2008 +0200
+++ b/src/HOL/Library/RType.thy Thu Sep 25 09:28:03 2008 +0200
@@ -91,9 +91,9 @@
*}
lemma [code func]:
- "Typerep tyco1 tys1 = Typerep tyco2 tys2 \<longleftrightarrow> tyco1 = tyco2
- \<and> list_all2 (op =) tys1 tys2"
- by (auto simp add: list_all2_eq [symmetric])
+ "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])
code_type typerep
(SML "Term.typ")
--- a/src/HOL/List.thy Wed Sep 24 19:39:25 2008 +0200
+++ b/src/HOL/List.thy Thu Sep 25 09:28:03 2008 +0200
@@ -3625,7 +3625,7 @@
code_instance list :: eq
(Haskell -)
-code_const "op = \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool"
+code_const "eq_class.eq \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool"
(Haskell infixl 4 "==")
setup {*
--- a/src/HOL/Product_Type.thy Wed Sep 24 19:39:25 2008 +0200
+++ b/src/HOL/Product_Type.thy Thu Sep 25 09:28:03 2008 +0200
@@ -22,13 +22,15 @@
declare case_split [cases type: bool]
-- "prefer plain propositional version"
-lemma [code func]:
- shows "False = P \<longleftrightarrow> \<not> P"
- and "True = P \<longleftrightarrow> P"
- and "P = False \<longleftrightarrow> \<not> P"
- and "P = True \<longleftrightarrow> P" by simp_all
+lemma
+ shows [code func]: "eq_class.eq False P \<longleftrightarrow> \<not> P"
+ and [code func]: "eq_class.eq True P \<longleftrightarrow> P"
+ and [code func]: "eq_class.eq P False \<longleftrightarrow> \<not> P"
+ and [code func]: "eq_class.eq P True \<longleftrightarrow> P"
+ and [code nbe]: "eq_class.eq P P \<longleftrightarrow> True"
+ by (simp_all add: eq)
-code_const "op = \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
+code_const "eq_class.eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
(Haskell infixl 4 "==")
code_instance bool :: eq
@@ -88,7 +90,7 @@
instance unit :: eq ..
lemma [code func]:
- "(u\<Colon>unit) = v \<longleftrightarrow> True" unfolding unit_eq [of u] unit_eq [of v] by rule+
+ "eq_class.eq (u\<Colon>unit) v \<longleftrightarrow> True" unfolding eq unit_eq [of u] unit_eq [of v] by rule+
code_type unit
(SML "unit")
@@ -98,7 +100,7 @@
code_instance unit :: eq
(Haskell -)
-code_const "op = \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
+code_const "eq_class.eq \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
(Haskell infixl 4 "==")
code_const Unity
@@ -916,7 +918,7 @@
instance * :: (eq, eq) eq ..
lemma [code func]:
- "(x1\<Colon>'a\<Colon>eq, y1\<Colon>'b\<Colon>eq) = (x2, y2) \<longleftrightarrow> x1 = x2 \<and> y1 = y2" by auto
+ "eq_class.eq (x1\<Colon>'a\<Colon>eq, y1\<Colon>'b\<Colon>eq) (x2, y2) \<longleftrightarrow> x1 = x2 \<and> y1 = y2" by (simp add: eq)
lemma split_case_cert:
assumes "CASE \<equiv> split f"
@@ -935,7 +937,7 @@
code_instance * :: eq
(Haskell -)
-code_const "op = \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
+code_const "eq_class.eq \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
(Haskell infixl 4 "==")
code_const Pair
--- a/src/Pure/Isar/code_unit.ML Wed Sep 24 19:39:25 2008 +0200
+++ b/src/Pure/Isar/code_unit.ML Thu Sep 25 09:28:03 2008 +0200
@@ -20,9 +20,8 @@
(*constant aliasses*)
val add_const_alias: thm -> theory -> theory
- val subst_alias: theory -> string -> string
+ val triv_classes: theory -> class list
val resubst_alias: theory -> string -> string
- val triv_classes: theory -> class list
(*constants*)
val string_of_typ: theory -> typ -> string
@@ -39,7 +38,7 @@
(*defining equations*)
val assert_rew: thm -> thm
val mk_rew: thm -> thm
- val mk_func: thm -> thm
+ val mk_func: bool -> thm -> thm
val head_func: thm -> string * ((string * sort) list * typ)
val expand_eta: int -> thm -> thm
val rewrite_func: simpset -> thm -> thm
@@ -223,6 +222,7 @@
|> map Drule.zero_var_indexes
end;
+
(* const aliasses *)
structure ConstAlias = TheoryDataFun
@@ -252,16 +252,6 @@
((c_c', thm) :: alias, fold (insert (op =)) some_class classes))
end;
-fun rew_alias thm =
- let
- val thy = Thm.theory_of_thm thm;
- in rewrite_head ((map snd o fst o ConstAlias.get) thy) thm end;
-
-fun subst_alias thy c = ConstAlias.get thy
- |> fst
- |> get_first (fn ((c', c''), _) => if c = c' then SOME c'' else NONE)
- |> the_default c;
-
fun resubst_alias thy =
let
val alias = fst (ConstAlias.get thy);
@@ -275,19 +265,18 @@
val triv_classes = snd o ConstAlias.get;
+
(* reading constants as terms *)
fun check_bare_const thy t = case try dest_Const t
of SOME c_ty => c_ty
| NONE => error ("Not a constant: " ^ Syntax.string_of_term_global thy t);
-fun check_const thy = subst_alias thy o AxClass.unoverload_const thy o apfst (subst_alias thy)
- o check_bare_const thy;
+fun check_const thy = AxClass.unoverload_const thy o check_bare_const thy;
fun read_bare_const thy = check_bare_const thy o Syntax.read_term_global thy;
-fun read_const thy = subst_alias thy o AxClass.unoverload_const thy o apfst (subst_alias thy)
- o read_bare_const thy;
+fun read_const thy = AxClass.unoverload_const thy o read_bare_const thy;
(* constructor sets *)
@@ -372,7 +361,7 @@
(* defining equations *)
-fun assert_func thm =
+fun assert_func linear thm =
let
val thy = Thm.theory_of_thm thm;
val (head, args) = (strip_comb o fst o Logic.dest_equals
@@ -380,7 +369,7 @@
val _ = case head of Const _ => () | _ =>
bad_thm ("Equation not headed by constant\n" ^ Display.string_of_thm thm);
val _ =
- if has_duplicates (op =)
+ if linear andalso has_duplicates (op =)
((fold o fold_aterms) (fn Var (v, _) => cons v
| _ => I
) args [])
@@ -403,7 +392,7 @@
val _ = map (check 0) args;
in thm end;
-val mk_func = rew_alias o assert_func o mk_rew;
+fun mk_func linear = assert_func linear o mk_rew;
fun head_func thm =
let
@@ -454,6 +443,6 @@
fun case_cert thm = case_certificate thm
handle Bind => error "bad case certificate"
- | TERM _ => error "bad case certificate";
+ | TERM _ => error "bad case certificate";
end;
--- a/src/Tools/code/code_name.ML Wed Sep 24 19:39:25 2008 +0200
+++ b/src/Tools/code/code_name.ML Thu Sep 25 09:28:03 2008 +0200
@@ -45,9 +45,8 @@
val thy' = case some_thyname
of SOME thyname => ThyInfo.the_theory thyname thy
| NONE => thy;
- val raw_cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
+ val cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
((snd o #constants o Consts.dest o #consts o Sign.rep_sg) thy') [];
- val cs = map (Code_Unit.subst_alias thy') raw_cs;
fun belongs_here c =
not (exists (fn thy'' => Sign.declared_const thy'' c) (Theory.parents_of thy'))
in case some_thyname