# HG changeset patch
# User haftmann
# Date 1161000451 -7200
# Node ID fe1db2f991a7aeefb8d394ca237c9af0990518ba
# Parent  66d6d1b0ddfab0395512cf8e767d00cadc5d779e
moved HOL code generator setup to Code_Generator

diff -r 66d6d1b0ddfa -r fe1db2f991a7 src/HOL/Code_Generator.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Code_Generator.thy	Mon Oct 16 14:07:31 2006 +0200
@@ -0,0 +1,195 @@
+(*  ID:         $Id$
+    Author:     Florian Haftmann, TU Muenchen
+*)
+
+header {* Setup of code generator tools *}
+
+theory Code_Generator
+imports HOL
+begin
+
+subsection {* ML code generator *}
+
+types_code
+  "bool"  ("bool")
+attach (term_of) {*
+fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
+*}
+attach (test) {*
+fun gen_bool i = one_of [false, true];
+*}
+  "prop"  ("bool")
+attach (term_of) {*
+fun term_of_prop b =
+  HOLogic.mk_Trueprop (if b then HOLogic.true_const else HOLogic.false_const);
+*}
+
+consts_code
+  "Trueprop" ("(_)")
+  "True"    ("true")
+  "False"   ("false")
+  "Not"     ("not")
+  "op |"    ("(_ orelse/ _)")
+  "op &"    ("(_ andalso/ _)")
+  "HOL.If"      ("(if _/ then _/ else _)")
+
+setup {*
+let
+
+fun eq_codegen thy defs gr dep thyname b t =
+    (case strip_comb t of
+       (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE
+     | (Const ("op =", _), [t, u]) =>
+          let
+            val (gr', pt) = Codegen.invoke_codegen thy defs dep thyname false (gr, t);
+            val (gr'', pu) = Codegen.invoke_codegen thy defs dep thyname false (gr', u);
+            val (gr''', _) = Codegen.invoke_tycodegen thy defs dep thyname false (gr'', HOLogic.boolT)
+          in
+            SOME (gr''', Codegen.parens
+              (Pretty.block [pt, Pretty.str " =", Pretty.brk 1, pu]))
+          end
+     | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
+         thy defs dep thyname b (gr, Codegen.eta_expand t ts 2))
+     | _ => NONE);
+
+in
+
+Codegen.add_codegen "eq_codegen" eq_codegen
+
+end
+*}
+
+text {* Evaluation *}
+
+setup {*
+let
+
+fun evaluation_tac i = Tactical.PRIMITIVE (Drule.fconv_rule
+  (Drule.goals_conv (equal i) Codegen.evaluation_conv));
+
+val evaluation_meth =
+  Method.no_args (Method.METHOD (fn _ => evaluation_tac 1 THEN rtac HOL.TrueI 1));
+
+in
+
+Method.add_method ("evaluation", evaluation_meth, "solve goal by evaluation")
+
+end;
+*}
+
+
+subsection {* Generic code generator setup *}
+
+text {* itself as a code generator datatype *}
+
+setup {*
+let fun add_itself thy =
+  let
+    val v = ("'a", []);
+    val t = Logic.mk_type (TFree v);
+    val Const (c, ty) = t;
+    val (_, Type (dtco, _)) = strip_type ty;
+  in
+    thy
+    |> CodegenData.add_datatype (dtco, (([v], [(c, [])]), CodegenData.lazy (fn () => [])))
+  end
+in add_itself end;
+*} 
+
+
+text {* code generation for arbitrary as exception *}
+
+setup {*
+  CodegenSerializer.add_undefined "SML" "arbitrary" "(raise Fail \"arbitrary\")"
+*}
+
+code_const arbitrary
+  (Haskell target_atom "(error \"arbitrary\")")
+
+
+subsection {* Operational equality for code generation *}
+
+subsubsection {* eq class *}
+
+class eq =
+  fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+
+defs
+  eq_def: "eq x y \<equiv> (x = y)"
+
+
+subsubsection {* bool type *}
+
+instance bool :: eq ..
+
+lemma [code func]:
+  "eq True p = p" unfolding eq_def by auto
+
+lemma [code func]:
+  "eq False p = (\<not> p)" unfolding eq_def by auto
+
+lemma [code func]:
+  "eq p True = p" unfolding eq_def by auto
+
+lemma [code func]:
+  "eq p False = (\<not> p)" unfolding eq_def by auto
+
+code_constname
+  "eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool" "HOL.eq_bool"
+
+
+subsubsection {* preprocessors *}
+
+setup {*
+let
+  fun constrain_op_eq thy ts =
+    let
+      fun add_eq (Const ("op =", ty)) =
+            fold (insert (eq_fst (op = : indexname * indexname -> bool)))
+              (Term.add_tvarsT ty [])
+        | add_eq _ =
+            I
+      val eqs = (fold o fold_aterms) add_eq ts [];
+      val inst = map (fn (v_i, _) => (v_i, [HOLogic.class_eq])) eqs;
+    in inst end;
+in CodegenData.add_constrains constrain_op_eq end
+*}
+
+declare eq_def [symmetric, code inline]
+
+
+subsubsection {* Haskell *}
+
+code_class eq
+  (Haskell "Eq" where eq \<equiv> "(==)")
+
+code_const eq
+  (Haskell infixl 4 "==")
+
+code_instance bool :: eq
+  (Haskell -)
+
+code_const "eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
+  (Haskell infixl 4 "==")
+
+
+subsection {* normalization by evaluation *}
+
+lemma eq_refl: "eq x x"
+  unfolding eq_def ..
+
+setup {*
+let
+  val eq_refl = thm "eq_refl";
+  fun normalization_tac i = Tactical.PRIMITIVE (Drule.fconv_rule
+    (Drule.goals_conv (equal i) (HOL.Trueprop_conv NBE.normalization_conv)));
+  val normalization_meth =
+    Method.no_args (Method.METHOD (fn _ => normalization_tac 1 THEN resolve_tac [TrueI, refl, eq_refl] 1));
+in
+  Method.add_method ("normalization", normalization_meth, "solve goal by normalization")
+end;
+*}
+
+hide (open) const eq
+
+end
\ No newline at end of file
diff -r 66d6d1b0ddfa -r fe1db2f991a7 src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Mon Oct 16 14:07:21 2006 +0200
+++ b/src/HOL/Datatype.thy	Mon Oct 16 14:07:31 2006 +0200
@@ -804,7 +804,7 @@
 code_instance option :: eq
   (Haskell -)
 
-code_const "OperationalEquality.eq \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool"
+code_const "Code_Generator.eq \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool"
   (Haskell infixl 4 "==")
 
 ML
diff -r 66d6d1b0ddfa -r fe1db2f991a7 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Mon Oct 16 14:07:21 2006 +0200
+++ b/src/HOL/HOL.thy	Mon Oct 16 14:07:31 2006 +0200
@@ -954,9 +954,44 @@
 
 fun case_tac a = res_inst_tac [("P", a)] case_split;
 
+(* combination of (spec RS spec RS ...(j times) ... spec RS mp) *)
+local
+  fun wrong_prem (Const ("All", _) $ (Abs (_, _, t))) = wrong_prem t
+    | wrong_prem (Bound _) = true
+    | wrong_prem _ = false;
+  val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.prems_of);
+in
+  fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp]);
+  fun smp_tac j = EVERY'[dresolve_tac (smp j), atac];
+end;
+
+fun strip_tac i = REPEAT (resolve_tac [impI, allI] i);
+
 val Blast_tac = Blast.Blast_tac;
 val blast_tac = Blast.blast_tac;
 
+fun Trueprop_conv conv ct = (case term_of ct of
+    Const ("Trueprop", _) $ _ =>
+      let val (ct1, ct2) = Thm.dest_comb ct
+      in Thm.combination (Thm.reflexive ct1) (conv ct2) end
+  | _ => raise TERM ("Trueprop_conv", []));
+
+fun constrain_op_eq_thms thy thms =
+  let
+    fun add_eq (Const ("op =", ty)) =
+          fold (insert (eq_fst (op =)))
+            (Term.add_tvarsT ty [])
+      | add_eq _ =
+          I
+    val eqs = fold (fold_aterms add_eq o Thm.prop_of) thms [];
+    val instT = map (fn (v_i, sort) =>
+      (Thm.ctyp_of thy (TVar (v_i, sort)),
+         Thm.ctyp_of thy (TVar (v_i, Sorts.inter_sort (Sign.classes_of thy) (sort, [HOLogic.class_eq]))))) eqs;
+  in
+    thms
+    |> map (Thm.instantiate (instT, []))
+  end;
+
 end;
 *}
 
@@ -1428,99 +1463,6 @@
 setup InductMethod.setup
 
 
-subsubsection {* Code generator setup *}
-
-types_code
-  "bool"  ("bool")
-attach (term_of) {*
-fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
-*}
-attach (test) {*
-fun gen_bool i = one_of [false, true];
-*}
-  "prop"  ("bool")
-attach (term_of) {*
-fun term_of_prop b =
-  HOLogic.mk_Trueprop (if b then HOLogic.true_const else HOLogic.false_const);
-*}
-
-consts_code
-  "Trueprop" ("(_)")
-  "True"    ("true")
-  "False"   ("false")
-  "Not"     ("not")
-  "op |"    ("(_ orelse/ _)")
-  "op &"    ("(_ andalso/ _)")
-  "HOL.If"      ("(if _/ then _/ else _)")
-
-setup {*
-let
-
-fun eq_codegen thy defs gr dep thyname b t =
-    (case strip_comb t of
-       (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE
-     | (Const ("op =", _), [t, u]) =>
-          let
-            val (gr', pt) = Codegen.invoke_codegen thy defs dep thyname false (gr, t);
-            val (gr'', pu) = Codegen.invoke_codegen thy defs dep thyname false (gr', u);
-            val (gr''', _) = Codegen.invoke_tycodegen thy defs dep thyname false (gr'', HOLogic.boolT)
-          in
-            SOME (gr''', Codegen.parens
-              (Pretty.block [pt, Pretty.str " =", Pretty.brk 1, pu]))
-          end
-     | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
-         thy defs dep thyname b (gr, Codegen.eta_expand t ts 2))
-     | _ => NONE);
-
-in
-
-Codegen.add_codegen "eq_codegen" eq_codegen
-
-end
-*}
-
-setup {*
-let
-
-fun evaluation_tac i = Tactical.PRIMITIVE (Drule.fconv_rule
-  (Drule.goals_conv (equal i) Codegen.evaluation_conv));
-
-val evaluation_meth =
-  Method.no_args (Method.METHOD (fn _ => evaluation_tac 1 THEN rtac HOL.TrueI 1));
-
-in
-
-Method.add_method ("evaluation", evaluation_meth, "solve goal by evaluation")
-
-end;
-*}
-
-
-text {* itself as a code generator datatype *}
-
-setup {*
-let fun add_itself thy =
-  let
-    val v = ("'a", []);
-    val t = Logic.mk_type (TFree v);
-    val Const (c, ty) = t;
-    val (_, Type (dtco, _)) = strip_type ty;
-  in
-    thy
-    |> CodegenData.add_datatype (dtco, (([v], [(c, [])]), CodegenData.lazy (fn () => [])))
-  end
-in add_itself end;
-*} 
-
-text {* code generation for arbitrary as exception *}
-
-setup {*
-  CodegenSerializer.add_undefined "SML" "arbitrary" "(raise Fail \"arbitrary\")"
-*}
-
-code_const arbitrary
-  (Haskell target_atom "(error \"arbitrary\")")
-
 
 subsection {* Other simple lemmas and lemma duplicates *}
 
@@ -1553,29 +1495,4 @@
   shows "f x (f y z) = f y (f x z)"
   by (rule trans [OF trans [OF c a] arg_cong [OF c, of "f y"]])
 
-
-subsection {* Conclude HOL structure *}
-
-ML {*
-structure HOL =
-struct
-
-open HOL;
-
-(* combination of (spec RS spec RS ...(j times) ... spec RS mp) *)
-local
-  fun wrong_prem (Const ("All", _) $ (Abs (_, _, t))) = wrong_prem t
-    | wrong_prem (Bound _) = true
-    | wrong_prem _ = false;
-  val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.prems_of);
-in
-  fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp]);
-  fun smp_tac j = EVERY'[dresolve_tac (smp j), atac];
-end;
-
-fun strip_tac i = REPEAT (resolve_tac [impI, allI] i);
-
-end;
-*}
-
 end
diff -r 66d6d1b0ddfa -r fe1db2f991a7 src/HOL/Integ/IntArith.thy
--- a/src/HOL/Integ/IntArith.thy	Mon Oct 16 14:07:21 2006 +0200
+++ b/src/HOL/Integ/IntArith.thy	Mon Oct 16 14:07:31 2006 +0200
@@ -375,7 +375,7 @@
   "Numeral.Min" "IntDef.min"
   "Numeral.Bit" "IntDef.bit"
   "Numeral.bit.bit_case" "IntDef.bit_case"
-  "OperationalEquality.eq \<Colon> bit \<Rightarrow> bit \<Rightarrow> bool" "IntDef.eq_bit"
+  "Code_Generator.eq \<Colon> bit \<Rightarrow> bit \<Rightarrow> bool" "IntDef.eq_bit"
   "Numeral.B0" "IntDef.b0"
   "Numeral.B1" "IntDef.b1"
 
diff -r 66d6d1b0ddfa -r fe1db2f991a7 src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Mon Oct 16 14:07:21 2006 +0200
+++ b/src/HOL/Integ/IntDef.thy	Mon Oct 16 14:07:31 2006 +0200
@@ -915,7 +915,7 @@
 code_instance int :: eq
   (Haskell -)
 
-code_const "OperationalEquality.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
+code_const "Code_Generator.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
   (SML "(op =) (_ : IntInf.int, _)")
   (Haskell infixl 4 "==")
 
diff -r 66d6d1b0ddfa -r fe1db2f991a7 src/HOL/Integ/Presburger.thy
--- a/src/HOL/Integ/Presburger.thy	Mon Oct 16 14:07:21 2006 +0200
+++ b/src/HOL/Integ/Presburger.thy	Mon Oct 16 14:07:31 2006 +0200
@@ -10,8 +10,9 @@
 
 theory Presburger
 imports NatSimprocs
-uses ("cooper_dec.ML") ("cooper_proof.ML") ("qelim.ML") 
-	("reflected_presburger.ML") ("reflected_cooper.ML") ("presburger.ML")
+uses
+  ("cooper_dec.ML") ("cooper_proof.ML") ("qelim.ML") 
+  ("reflected_presburger.ML") ("reflected_cooper.ML") ("presburger.ML")
 begin
 
 text {* Theorem for unitifying the coeffitients of @{text x} in an existential formula*}
@@ -1094,7 +1095,7 @@
 *}
 
 lemma eq_number_of [code func]:
-  "OperationalEquality.eq ((number_of k)\<Colon>int) (number_of l) \<longleftrightarrow> OperationalEquality.eq k l"
+  "Code_Generator.eq ((number_of k)\<Colon>int) (number_of l) \<longleftrightarrow> Code_Generator.eq k l"
   unfolding number_of_is_id ..
 
 lemma less_eq_number_of [code func]:
@@ -1102,56 +1103,56 @@
   unfolding number_of_is_id ..
 
 lemma eq_Pls_Pls:
-  "OperationalEquality.eq Numeral.Pls Numeral.Pls"
+  "Code_Generator.eq Numeral.Pls Numeral.Pls"
   unfolding eq_def ..
 
 lemma eq_Pls_Min:
-  "\<not> OperationalEquality.eq Numeral.Pls Numeral.Min"
+  "\<not> Code_Generator.eq Numeral.Pls Numeral.Min"
   unfolding eq_def Pls_def Min_def by auto
 
 lemma eq_Pls_Bit0:
-  "OperationalEquality.eq Numeral.Pls (Numeral.Bit k bit.B0) \<longleftrightarrow> OperationalEquality.eq Numeral.Pls k"
+  "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
 
 lemma eq_Pls_Bit1:
-  "\<not> OperationalEquality.eq Numeral.Pls (Numeral.Bit k bit.B1)"
+  "\<not> Code_Generator.eq Numeral.Pls (Numeral.Bit k bit.B1)"
   unfolding eq_def Pls_def Bit_def bit.cases by arith
 
 lemma eq_Min_Pls:
-  "\<not> OperationalEquality.eq Numeral.Min Numeral.Pls"
+  "\<not> Code_Generator.eq Numeral.Min Numeral.Pls"
   unfolding eq_def Pls_def Min_def by auto
 
 lemma eq_Min_Min:
-  "OperationalEquality.eq Numeral.Min Numeral.Min"
+  "Code_Generator.eq Numeral.Min Numeral.Min"
   unfolding eq_def ..
 
 lemma eq_Min_Bit0:
-  "\<not> OperationalEquality.eq Numeral.Min (Numeral.Bit k bit.B0)"
+  "\<not> Code_Generator.eq Numeral.Min (Numeral.Bit k bit.B0)"
   unfolding eq_def Min_def Bit_def bit.cases by arith
 
 lemma eq_Min_Bit1:
-  "OperationalEquality.eq Numeral.Min (Numeral.Bit k bit.B1) \<longleftrightarrow> OperationalEquality.eq Numeral.Min k"
+  "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
 
 lemma eq_Bit0_Pls:
-  "OperationalEquality.eq (Numeral.Bit k bit.B0) Numeral.Pls \<longleftrightarrow> OperationalEquality.eq Numeral.Pls k"
+  "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
 
 lemma eq_Bit1_Pls:
-  "\<not> OperationalEquality.eq (Numeral.Bit k bit.B1) Numeral.Pls"
+  "\<not> Code_Generator.eq (Numeral.Bit k bit.B1) Numeral.Pls"
   unfolding eq_def Pls_def Bit_def bit.cases by arith
 
 lemma eq_Bit0_Min:
-  "\<not> OperationalEquality.eq (Numeral.Bit k bit.B0) Numeral.Min"
+  "\<not> Code_Generator.eq (Numeral.Bit k bit.B0) Numeral.Min"
   unfolding eq_def Min_def Bit_def bit.cases by arith
 
 lemma eq_Bit1_Min:
-  "OperationalEquality.eq (Numeral.Bit k bit.B1) Numeral.Min \<longleftrightarrow> OperationalEquality.eq Numeral.Min k"
+  "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
 
 lemma eq_Bit_Bit:
-  "OperationalEquality.eq (Numeral.Bit k1 v1) (Numeral.Bit k2 v2) \<longleftrightarrow>
-    OperationalEquality.eq v1 v2 \<and> OperationalEquality.eq k1 k2"
+  "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
   apply (cases v1)
   apply (cases v2)
diff -r 66d6d1b0ddfa -r fe1db2f991a7 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Oct 16 14:07:21 2006 +0200
+++ b/src/HOL/IsaMakefile	Mon Oct 16 14:07:31 2006 +0200
@@ -84,7 +84,7 @@
   $(SRC)/TFL/rules.ML $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML			\
   $(SRC)/TFL/thry.ML $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML			\
   Tools/res_atpset.ML \
-  Binomial.thy Datatype.ML Datatype.thy			\
+  Binomial.thy Code_Generator.thy Datatype.ML Datatype.thy			\
   Divides.thy						\
   Equiv_Relations.thy Extraction.thy Finite_Set.ML Finite_Set.thy		\
   FixedPoint.thy Fun.thy HOL.ML HOL.thy Hilbert_Choice.thy Inductive.thy	\
@@ -95,7 +95,7 @@
   Integ/reflected_cooper.ML Integ/int_arith1.ML Integ/int_factor_simprocs.ML	\
   Integ/nat_simprocs.ML Integ/presburger.ML Integ/qelim.ML LOrder.thy		\
   Lattice_Locales.thy List.ML List.thy Main.ML Main.thy Map.thy			\
-  Nat.ML Nat.thy NatArith.thy OperationalEquality.thy OrderedGroup.ML OrderedGroup.thy	\
+  Nat.ML Nat.thy NatArith.thy OrderedGroup.ML OrderedGroup.thy	\
   Orderings.ML Orderings.thy Power.thy PreList.thy Product_Type.thy		\
   ROOT.ML Recdef.thy Reconstruction.thy Record.thy Refute.thy			\
   Relation.ML Relation.thy Relation_Power.thy Ring_and_Field.thy SAT.thy Set.ML		\
diff -r 66d6d1b0ddfa -r fe1db2f991a7 src/HOL/Library/EfficientNat.thy
--- a/src/HOL/Library/EfficientNat.thy	Mon Oct 16 14:07:21 2006 +0200
+++ b/src/HOL/Library/EfficientNat.thy	Mon Oct 16 14:07:31 2006 +0200
@@ -53,7 +53,7 @@
 qed
 
 lemma [code inline]:
-  "nat_case f g n = (if OperationalEquality.eq n 0 then f else g (nat_of_int (int n - 1)))"
+  "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)
 
 text {*
@@ -100,7 +100,7 @@
   by simp
 lemma [code func, code inline]: "(m \<le> n) \<longleftrightarrow> (int m \<le> int n)"
   by simp
-lemma [code func, code inline]: "OperationalEquality.eq m n \<longleftrightarrow> OperationalEquality.eq (int m) (int n)"
+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]: "nat k = (if k < 0 then 0 else nat_of_int k)"
 proof (cases "k < 0")
diff -r 66d6d1b0ddfa -r fe1db2f991a7 src/HOL/Library/ExecutableRat.thy
--- a/src/HOL/Library/ExecutableRat.thy	Mon Oct 16 14:07:21 2006 +0200
+++ b/src/HOL/Library/ExecutableRat.thy	Mon Oct 16 14:07:31 2006 +0200
@@ -113,7 +113,7 @@
   "op * \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat" "Rational.erat_times"
   "inverse  \<Colon> erat \<Rightarrow> erat" "Rational.erat_inverse"
   "op \<le> \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool" "Rational.erat_le"
-  "OperationalEquality.eq \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool" "Rational.erat_eq"
+  "Code_Generator.eq \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool" "Rational.erat_eq"
 
 
 section {* rat as abstype *}
@@ -127,7 +127,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"
-   "OperationalEquality.eq \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" \<equiv> eq_erat
+   "Code_Generator.eq \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" \<equiv> eq_erat
 
 code_const div_zero
   (SML "raise/ (Fail/ \"Division by zero\")")
@@ -142,7 +142,7 @@
   "op * \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat"
   "inverse \<Colon> rat \<Rightarrow> rat"
   "op \<le> \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool"
-   "OperationalEquality.eq \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool"
+   "Code_Generator.eq \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool"
   (SML -)
 
 
diff -r 66d6d1b0ddfa -r fe1db2f991a7 src/HOL/Library/ExecutableSet.thy
--- a/src/HOL/Library/ExecutableSet.thy	Mon Oct 16 14:07:21 2006 +0200
+++ b/src/HOL/Library/ExecutableSet.thy	Mon Oct 16 14:07:31 2006 +0200
@@ -18,7 +18,7 @@
   by blast
 
 lemma [code func]:
-  "OperationalEquality.eq A B = (A \<subseteq> B \<and> B \<subseteq> A)"
+  "Code_Generator.eq A B = (A \<subseteq> B \<and> B \<subseteq> A)"
   unfolding eq_def by blast
 
 declare bex_triv_one_point1 [symmetric, standard, code]
diff -r 66d6d1b0ddfa -r fe1db2f991a7 src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Oct 16 14:07:21 2006 +0200
+++ b/src/HOL/List.thy	Mon Oct 16 14:07:31 2006 +0200
@@ -2764,10 +2764,10 @@
 code_instance list :: eq and char :: eq
   (Haskell - and -)
 
-code_const "OperationalEquality.eq \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool"
+code_const "Code_Generator.eq \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool"
   (Haskell infixl 4 "==")
 
-code_const "OperationalEquality.eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
+code_const "Code_Generator.eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
   (Haskell infixl 4 "==")
 
 setup {*
diff -r 66d6d1b0ddfa -r fe1db2f991a7 src/HOL/OperationalEquality.thy
--- a/src/HOL/OperationalEquality.thy	Mon Oct 16 14:07:21 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,112 +0,0 @@
-(*  ID:         $Id$
-    Author:     Florian Haftmann, TU Muenchen
-*)
-
-header {* Operational equality for code generation *}
-
-theory OperationalEquality
-imports HOL
-begin
-
-section {* Operational equality for code generation *}
-
-subsection {* eq class *}
-
-class eq =
-  fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
-
-defs
-  eq_def: "eq x y \<equiv> (x = y)"
-
-
-subsection {* bool type *}
-
-instance bool :: eq ..
-
-lemma [code func]:
-  "eq True p = p" unfolding eq_def by auto
-
-lemma [code func]:
-  "eq False p = (\<not> p)" unfolding eq_def by auto
-
-lemma [code func]:
-  "eq p True = p" unfolding eq_def by auto
-
-lemma [code func]:
-  "eq p False = (\<not> p)" unfolding eq_def by auto
-
-
-subsection {* code generator setup *}
-
-subsubsection {* preprocessor *}
-
-setup {*
-let
-  val class_eq = "OperationalEquality.eq";
-  fun constrain_op_eq thy ts =
-    let
-      fun add_eq (Const ("op =", ty)) =
-            fold (insert (eq_fst (op = : indexname * indexname -> bool)))
-              (Term.add_tvarsT ty [])
-        | add_eq _ =
-            I
-      val eqs = (fold o fold_aterms) add_eq ts [];
-      val inst = map (fn (v_i, _) => (v_i, [class_eq])) eqs;
-    in inst end;
-in CodegenData.add_constrains constrain_op_eq end
-*}
-
-declare eq_def [symmetric, code inline]
-
-code_constname
-  "eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool" "HOL.eq_bool"
-
-
-subsection {* haskell setup *}
-
-code_class eq
-  (Haskell "Eq" where eq \<equiv> "(==)")
-
-code_const eq
-  (Haskell infixl 4 "==")
-
-code_instance bool :: eq
-  (Haskell -)
-
-code_const "eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
-  (Haskell infixl 4 "==")
-
-
-subsection {* nbe setup *}
-
-lemma eq_refl: "eq x x"
-  unfolding eq_def ..
-
-setup {*
-let
-
-val eq_refl = thm "eq_refl";
-
-fun Trueprop_conv conv ct = (case term_of ct of
-    Const ("Trueprop", _) $ _ =>
-      let val (ct1, ct2) = Thm.dest_comb ct
-      in Thm.combination (Thm.reflexive ct1) (conv ct2) end
-  | _ => raise TERM ("Trueprop_conv", []));
-
-fun normalization_tac i = Tactical.PRIMITIVE (Drule.fconv_rule
-  (Drule.goals_conv (equal i) (Trueprop_conv NBE.normalization_conv)));
-
-val normalization_meth =
-  Method.no_args (Method.METHOD (fn _ => normalization_tac 1 THEN resolve_tac [TrueI, refl, eq_refl] 1));
-
-in
-
-Method.add_method ("normalization", normalization_meth, "solve goal by normalization")
-
-end;
-*}
-
-
-hide (open) const eq
-
-end
\ No newline at end of file
diff -r 66d6d1b0ddfa -r fe1db2f991a7 src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Mon Oct 16 14:07:21 2006 +0200
+++ b/src/HOL/Presburger.thy	Mon Oct 16 14:07:31 2006 +0200
@@ -10,8 +10,9 @@
 
 theory Presburger
 imports NatSimprocs
-uses ("cooper_dec.ML") ("cooper_proof.ML") ("qelim.ML") 
-	("reflected_presburger.ML") ("reflected_cooper.ML") ("presburger.ML")
+uses
+  ("cooper_dec.ML") ("cooper_proof.ML") ("qelim.ML") 
+  ("reflected_presburger.ML") ("reflected_cooper.ML") ("presburger.ML")
 begin
 
 text {* Theorem for unitifying the coeffitients of @{text x} in an existential formula*}
@@ -1094,7 +1095,7 @@
 *}
 
 lemma eq_number_of [code func]:
-  "OperationalEquality.eq ((number_of k)\<Colon>int) (number_of l) \<longleftrightarrow> OperationalEquality.eq k l"
+  "Code_Generator.eq ((number_of k)\<Colon>int) (number_of l) \<longleftrightarrow> Code_Generator.eq k l"
   unfolding number_of_is_id ..
 
 lemma less_eq_number_of [code func]:
@@ -1102,56 +1103,56 @@
   unfolding number_of_is_id ..
 
 lemma eq_Pls_Pls:
-  "OperationalEquality.eq Numeral.Pls Numeral.Pls"
+  "Code_Generator.eq Numeral.Pls Numeral.Pls"
   unfolding eq_def ..
 
 lemma eq_Pls_Min:
-  "\<not> OperationalEquality.eq Numeral.Pls Numeral.Min"
+  "\<not> Code_Generator.eq Numeral.Pls Numeral.Min"
   unfolding eq_def Pls_def Min_def by auto
 
 lemma eq_Pls_Bit0:
-  "OperationalEquality.eq Numeral.Pls (Numeral.Bit k bit.B0) \<longleftrightarrow> OperationalEquality.eq Numeral.Pls k"
+  "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
 
 lemma eq_Pls_Bit1:
-  "\<not> OperationalEquality.eq Numeral.Pls (Numeral.Bit k bit.B1)"
+  "\<not> Code_Generator.eq Numeral.Pls (Numeral.Bit k bit.B1)"
   unfolding eq_def Pls_def Bit_def bit.cases by arith
 
 lemma eq_Min_Pls:
-  "\<not> OperationalEquality.eq Numeral.Min Numeral.Pls"
+  "\<not> Code_Generator.eq Numeral.Min Numeral.Pls"
   unfolding eq_def Pls_def Min_def by auto
 
 lemma eq_Min_Min:
-  "OperationalEquality.eq Numeral.Min Numeral.Min"
+  "Code_Generator.eq Numeral.Min Numeral.Min"
   unfolding eq_def ..
 
 lemma eq_Min_Bit0:
-  "\<not> OperationalEquality.eq Numeral.Min (Numeral.Bit k bit.B0)"
+  "\<not> Code_Generator.eq Numeral.Min (Numeral.Bit k bit.B0)"
   unfolding eq_def Min_def Bit_def bit.cases by arith
 
 lemma eq_Min_Bit1:
-  "OperationalEquality.eq Numeral.Min (Numeral.Bit k bit.B1) \<longleftrightarrow> OperationalEquality.eq Numeral.Min k"
+  "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
 
 lemma eq_Bit0_Pls:
-  "OperationalEquality.eq (Numeral.Bit k bit.B0) Numeral.Pls \<longleftrightarrow> OperationalEquality.eq Numeral.Pls k"
+  "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
 
 lemma eq_Bit1_Pls:
-  "\<not> OperationalEquality.eq (Numeral.Bit k bit.B1) Numeral.Pls"
+  "\<not> Code_Generator.eq (Numeral.Bit k bit.B1) Numeral.Pls"
   unfolding eq_def Pls_def Bit_def bit.cases by arith
 
 lemma eq_Bit0_Min:
-  "\<not> OperationalEquality.eq (Numeral.Bit k bit.B0) Numeral.Min"
+  "\<not> Code_Generator.eq (Numeral.Bit k bit.B0) Numeral.Min"
   unfolding eq_def Min_def Bit_def bit.cases by arith
 
 lemma eq_Bit1_Min:
-  "OperationalEquality.eq (Numeral.Bit k bit.B1) Numeral.Min \<longleftrightarrow> OperationalEquality.eq Numeral.Min k"
+  "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
 
 lemma eq_Bit_Bit:
-  "OperationalEquality.eq (Numeral.Bit k1 v1) (Numeral.Bit k2 v2) \<longleftrightarrow>
-    OperationalEquality.eq v1 v2 \<and> OperationalEquality.eq k1 k2"
+  "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
   apply (cases v1)
   apply (cases v2)
diff -r 66d6d1b0ddfa -r fe1db2f991a7 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Mon Oct 16 14:07:21 2006 +0200
+++ b/src/HOL/Product_Type.thy	Mon Oct 16 14:07:31 2006 +0200
@@ -764,7 +764,7 @@
 instance unit :: eq ..
 
 lemma [code func]:
-  "OperationalEquality.eq (u\<Colon>unit) v = True" unfolding eq_def unit_eq [of u] unit_eq [of v] by rule+
+  "Code_Generator.eq (u\<Colon>unit) v = True" unfolding eq_def unit_eq [of u] unit_eq [of v] by rule+
 
 code_instance unit :: eq
   (Haskell -)
@@ -772,16 +772,16 @@
 instance * :: (eq, eq) eq ..
 
 lemma [code func]:
-  "OperationalEquality.eq (x1, y1) (x2, y2) = (OperationalEquality.eq x1 x2 \<and> OperationalEquality.eq y1 y2)"
+  "Code_Generator.eq (x1, y1) (x2, y2) = (Code_Generator.eq x1 x2 \<and> Code_Generator.eq y1 y2)"
   unfolding eq_def by auto
 
 code_instance * :: eq
   (Haskell -)
 
-code_const "OperationalEquality.eq \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
+code_const "Code_Generator.eq \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
   (Haskell infixl 4 "==")
 
-code_const "OperationalEquality.eq \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
+code_const "Code_Generator.eq \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
   (Haskell infixl 4 "==")
 
 types_code
diff -r 66d6d1b0ddfa -r fe1db2f991a7 src/HOL/Sum_Type.thy
--- a/src/HOL/Sum_Type.thy	Mon Oct 16 14:07:21 2006 +0200
+++ b/src/HOL/Sum_Type.thy	Mon Oct 16 14:07:31 2006 +0200
@@ -197,19 +197,19 @@
 instance "+" :: (eq, eq) eq ..
 
 lemma [code func]:
-  "OperationalEquality.eq (Inl x) (Inl y) = OperationalEquality.eq x y"
+  "Code_Generator.eq (Inl x) (Inl y) = Code_Generator.eq x y"
   unfolding eq_def Inl_eq ..
 
 lemma [code func]:
-  "OperationalEquality.eq (Inr x) (Inr y) = OperationalEquality.eq x y"
+  "Code_Generator.eq (Inr x) (Inr y) = Code_Generator.eq x y"
   unfolding eq_def Inr_eq ..
 
 lemma [code func]:
-  "OperationalEquality.eq (Inl x) (Inr y) = False"
+  "Code_Generator.eq (Inl x) (Inr y) = False"
   unfolding eq_def using Inl_not_Inr by auto
 
 lemma [code func]:
-  "OperationalEquality.eq (Inr x) (Inl y) = False"
+  "Code_Generator.eq (Inr x) (Inl y) = False"
   unfolding eq_def using Inr_not_Inl by auto
 
 ML
diff -r 66d6d1b0ddfa -r fe1db2f991a7 src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Mon Oct 16 14:07:21 2006 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML	Mon Oct 16 14:07:31 2006 +0200
@@ -490,30 +490,14 @@
 
 local
   val eq_def_sym = thm "eq_def" |> Thm.symmetric;
-  val class_eq = "OperationalEquality.eq";
   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];
-  fun constrain_op_eq_thms thy thms =
-    let
-      fun add_eq (Const ("op =", ty)) =
-            fold (insert (eq_fst (op =)))
-              (Term.add_tvarsT ty [])
-        | add_eq _ =
-            I
-      val eqs = fold (fold_aterms add_eq o Thm.prop_of) thms [];
-      val instT = map (fn (v_i, sort) =>
-        (Thm.ctyp_of thy (TVar (v_i, sort)),
-           Thm.ctyp_of thy (TVar (v_i, Sorts.inter_sort (Sign.classes_of thy) (sort, [class_eq]))))) eqs;
-    in
-      thms
-      |> map (Thm.instantiate (instT, []))
-    end;
 in
   fun get_eq thy tyco =
     get_eq_thms thy tyco
     |> maps ((#mk o #mk_rews o snd o MetaSimplifier.rep_ss o Simplifier.simpset_of) thy)
-    |> constrain_op_eq_thms thy
+    |> HOL.constrain_op_eq_thms thy
     |> map (Tactic.rewrite_rule [eq_def_sym])
 end;
 
@@ -615,15 +599,13 @@
 
 (* operational equality *)
 
-local
-  val class_eq = "OperationalEquality.eq";
-in fun eq_hook specs =
+fun eq_hook specs =
   let
     fun add_eq_thms (dtco, (_, (vs, cs))) thy =
       let
         val thy_ref = Theory.self_ref thy;
         val ty = Type (dtco, map TFree vs) |> Logic.varifyT;
-        val c = CodegenConsts.norm thy ("OperationalEquality.eq", [ty]);
+        val c = CodegenConsts.norm thy ("Code_Generator.eq", [ty]);
         val get_thms = (fn () => get_eq (Theory.deref thy_ref) dtco |> rev);
       in
         CodegenData.add_funcl (c, CodegenData.lazy get_thms) thy
@@ -631,9 +613,8 @@
   in
     prove_codetypes_arities (K (ClassPackage.intro_classes_tac []))
       (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
-      [class_eq] ((K o K o pair) []) ((K o K) (fold add_eq_thms specs))
+      [HOLogic.class_eq] ((K o K o pair) []) ((K o K) (fold add_eq_thms specs))
   end;
-end; (*local*)
 
 
 
diff -r 66d6d1b0ddfa -r fe1db2f991a7 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Mon Oct 16 14:07:21 2006 +0200
+++ b/src/HOL/Tools/meson.ML	Mon Oct 16 14:07:31 2006 +0200
@@ -204,7 +204,7 @@
 fun resop nf [prem] = resolve_tac (nf prem) 1;
 
 (*Any need to extend this list with 
-  "HOL.type_class","OperationalEquality.eq_class","ProtoPure.term"?*)
+  "HOL.type_class","Code_Generator.eq_class","ProtoPure.term"?*)
 val has_meta_conn = 
     exists_Const (fn (c,_) => c mem_string ["==", "==>", "all", "prop"]);
 
diff -r 66d6d1b0ddfa -r fe1db2f991a7 src/HOL/ex/Codegenerator.thy
--- a/src/HOL/ex/Codegenerator.thy	Mon Oct 16 14:07:21 2006 +0200
+++ b/src/HOL/ex/Codegenerator.thy	Mon Oct 16 14:07:31 2006 +0200
@@ -184,16 +184,16 @@
   "op mod :: int \<Rightarrow> int \<Rightarrow> int"  
   (SML) (Haskell)
 code_gen
-  "OperationalEquality.eq :: bool \<Rightarrow> bool \<Rightarrow> bool"
-  "OperationalEquality.eq :: nat \<Rightarrow> nat \<Rightarrow> bool"
-  "OperationalEquality.eq :: int \<Rightarrow> int \<Rightarrow> bool"
-  "OperationalEquality.eq :: ('a\<Colon>eq) * ('b\<Colon>eq) \<Rightarrow> 'a * 'b \<Rightarrow> bool"
-  "OperationalEquality.eq :: ('a\<Colon>eq) + ('b\<Colon>eq) \<Rightarrow> 'a + 'b \<Rightarrow> bool"
-  "OperationalEquality.eq :: ('a\<Colon>eq) option \<Rightarrow> 'a option \<Rightarrow> bool"
-  "OperationalEquality.eq :: ('a\<Colon>eq) list \<Rightarrow> 'a list \<Rightarrow> bool"
-  "OperationalEquality.eq :: mut1 \<Rightarrow> mut1 \<Rightarrow> bool"
-  "OperationalEquality.eq :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
-  "OperationalEquality.eq :: ('a\<Colon>eq) point_scheme \<Rightarrow> 'a point_scheme \<Rightarrow> bool"
+  "Code_Generator.eq :: bool \<Rightarrow> bool \<Rightarrow> bool"
+  "Code_Generator.eq :: nat \<Rightarrow> nat \<Rightarrow> bool"
+  "Code_Generator.eq :: int \<Rightarrow> int \<Rightarrow> bool"
+  "Code_Generator.eq :: ('a\<Colon>eq) * ('b\<Colon>eq) \<Rightarrow> 'a * 'b \<Rightarrow> bool"
+  "Code_Generator.eq :: ('a\<Colon>eq) + ('b\<Colon>eq) \<Rightarrow> 'a + 'b \<Rightarrow> bool"
+  "Code_Generator.eq :: ('a\<Colon>eq) option \<Rightarrow> 'a option \<Rightarrow> bool"
+  "Code_Generator.eq :: ('a\<Colon>eq) list \<Rightarrow> 'a list \<Rightarrow> bool"
+  "Code_Generator.eq :: mut1 \<Rightarrow> mut1 \<Rightarrow> bool"
+  "Code_Generator.eq :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
+  "Code_Generator.eq :: ('a\<Colon>eq) point_scheme \<Rightarrow> 'a point_scheme \<Rightarrow> bool"
 
 code_gen (SML -)
 
diff -r 66d6d1b0ddfa -r fe1db2f991a7 src/HOL/ex/NormalForm.thy
--- a/src/HOL/ex/NormalForm.thy	Mon Oct 16 14:07:21 2006 +0200
+++ b/src/HOL/ex/NormalForm.thy	Mon Oct 16 14:07:31 2006 +0200
@@ -127,8 +127,8 @@
 
 hide (open) const delayed_if
 
-normal_form "OperationalEquality.eq [2..<4] [2,3]"
-(*lemma "OperationalEquality.eq [2..<4] [2,3]" by normalization*)
+normal_form "Code_Generator.eq [2..<4] [2,3]"
+(*lemma "Code_Generator.eq [2..<4] [2,3]" by normalization*)
 
 definition
  andalso :: "bool \<Rightarrow> bool \<Rightarrow> bool"