1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Code_Generator.thy	Mon Oct 16 14:07:31 2006 +0200
     1.3 @@ -0,0 +1,195 @@
     1.4 +(*  ID:         $Id$
     1.5 +    Author:     Florian Haftmann, TU Muenchen
     1.6 +*)
     1.7 +
     1.8 +header {* Setup of code generator tools *}
     1.9 +
    1.10 +theory Code_Generator
    1.11 +imports HOL
    1.12 +begin
    1.13 +
    1.14 +subsection {* ML code generator *}
    1.15 +
    1.16 +types_code
    1.17 +  "bool"  ("bool")
    1.18 +attach (term_of) {*
    1.19 +fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
    1.20 +*}
    1.21 +attach (test) {*
    1.22 +fun gen_bool i = one_of [false, true];
    1.23 +*}
    1.24 +  "prop"  ("bool")
    1.25 +attach (term_of) {*
    1.26 +fun term_of_prop b =
    1.27 +  HOLogic.mk_Trueprop (if b then HOLogic.true_const else HOLogic.false_const);
    1.28 +*}
    1.29 +
    1.30 +consts_code
    1.31 +  "Trueprop" ("(_)")
    1.32 +  "True"    ("true")
    1.33 +  "False"   ("false")
    1.34 +  "Not"     ("not")
    1.35 +  "op |"    ("(_ orelse/ _)")
    1.36 +  "op &"    ("(_ andalso/ _)")
    1.37 +  "HOL.If"      ("(if _/ then _/ else _)")
    1.38 +
    1.39 +setup {*
    1.40 +let
    1.41 +
    1.42 +fun eq_codegen thy defs gr dep thyname b t =
    1.43 +    (case strip_comb t of
    1.44 +       (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE
    1.45 +     | (Const ("op =", _), [t, u]) =>
    1.46 +          let
    1.47 +            val (gr', pt) = Codegen.invoke_codegen thy defs dep thyname false (gr, t);
    1.48 +            val (gr'', pu) = Codegen.invoke_codegen thy defs dep thyname false (gr', u);
    1.49 +            val (gr''', _) = Codegen.invoke_tycodegen thy defs dep thyname false (gr'', HOLogic.boolT)
    1.50 +          in
    1.51 +            SOME (gr''', Codegen.parens
    1.52 +              (Pretty.block [pt, Pretty.str " =", Pretty.brk 1, pu]))
    1.53 +          end
    1.54 +     | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
    1.55 +         thy defs dep thyname b (gr, Codegen.eta_expand t ts 2))
    1.56 +     | _ => NONE);
    1.57 +
    1.58 +in
    1.59 +
    1.60 +Codegen.add_codegen "eq_codegen" eq_codegen
    1.61 +
    1.62 +end
    1.63 +*}
    1.64 +
    1.65 +text {* Evaluation *}
    1.66 +
    1.67 +setup {*
    1.68 +let
    1.69 +
    1.70 +fun evaluation_tac i = Tactical.PRIMITIVE (Drule.fconv_rule
    1.71 +  (Drule.goals_conv (equal i) Codegen.evaluation_conv));
    1.72 +
    1.73 +val evaluation_meth =
    1.74 +  Method.no_args (Method.METHOD (fn _ => evaluation_tac 1 THEN rtac HOL.TrueI 1));
    1.75 +
    1.76 +in
    1.77 +
    1.78 +Method.add_method ("evaluation", evaluation_meth, "solve goal by evaluation")
    1.79 +
    1.80 +end;
    1.81 +*}
    1.82 +
    1.83 +
    1.84 +subsection {* Generic code generator setup *}
    1.85 +
    1.86 +text {* itself as a code generator datatype *}
    1.87 +
    1.88 +setup {*
    1.89 +let fun add_itself thy =
    1.90 +  let
    1.91 +    val v = ("'a", []);
    1.92 +    val t = Logic.mk_type (TFree v);
    1.93 +    val Const (c, ty) = t;
    1.94 +    val (_, Type (dtco, _)) = strip_type ty;
    1.95 +  in
    1.96 +    thy
    1.97 +    |> CodegenData.add_datatype (dtco, (([v], [(c, [])]), CodegenData.lazy (fn () => [])))
    1.98 +  end
    1.99 +in add_itself end;
   1.100 +*} 
   1.101 +
   1.102 +
   1.103 +text {* code generation for arbitrary as exception *}
   1.104 +
   1.105 +setup {*
   1.106 +  CodegenSerializer.add_undefined "SML" "arbitrary" "(raise Fail \"arbitrary\")"
   1.107 +*}
   1.108 +
   1.109 +code_const arbitrary
   1.110 +  (Haskell target_atom "(error \"arbitrary\")")
   1.111 +
   1.112 +
   1.113 +subsection {* Operational equality for code generation *}
   1.114 +
   1.115 +subsubsection {* eq class *}
   1.116 +
   1.117 +class eq =
   1.118 +  fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   1.119 +
   1.120 +defs
   1.121 +  eq_def: "eq x y \<equiv> (x = y)"
   1.122 +
   1.123 +
   1.124 +subsubsection {* bool type *}
   1.125 +
   1.126 +instance bool :: eq ..
   1.127 +
   1.128 +lemma [code func]:
   1.129 +  "eq True p = p" unfolding eq_def by auto
   1.130 +
   1.131 +lemma [code func]:
   1.132 +  "eq False p = (\<not> p)" unfolding eq_def by auto
   1.133 +
   1.134 +lemma [code func]:
   1.135 +  "eq p True = p" unfolding eq_def by auto
   1.136 +
   1.137 +lemma [code func]:
   1.138 +  "eq p False = (\<not> p)" unfolding eq_def by auto
   1.139 +
   1.140 +code_constname
   1.141 +  "eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool" "HOL.eq_bool"
   1.142 +
   1.143 +
   1.144 +subsubsection {* preprocessors *}
   1.145 +
   1.146 +setup {*
   1.147 +let
   1.148 +  fun constrain_op_eq thy ts =
   1.149 +    let
   1.150 +      fun add_eq (Const ("op =", ty)) =
   1.151 +            fold (insert (eq_fst (op = : indexname * indexname -> bool)))
   1.152 +              (Term.add_tvarsT ty [])
   1.153 +        | add_eq _ =
   1.154 +            I
   1.155 +      val eqs = (fold o fold_aterms) add_eq ts [];
   1.156 +      val inst = map (fn (v_i, _) => (v_i, [HOLogic.class_eq])) eqs;
   1.157 +    in inst end;
   1.158 +in CodegenData.add_constrains constrain_op_eq end
   1.159 +*}
   1.160 +
   1.161 +declare eq_def [symmetric, code inline]
   1.162 +
   1.163 +
   1.164 +subsubsection {* Haskell *}
   1.165 +
   1.166 +code_class eq
   1.167 +  (Haskell "Eq" where eq \<equiv> "(==)")
   1.168 +
   1.169 +code_const eq
   1.170 +  (Haskell infixl 4 "==")
   1.171 +
   1.172 +code_instance bool :: eq
   1.173 +  (Haskell -)
   1.174 +
   1.175 +code_const "eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
   1.176 +  (Haskell infixl 4 "==")
   1.177 +
   1.178 +
   1.179 +subsection {* normalization by evaluation *}
   1.180 +
   1.181 +lemma eq_refl: "eq x x"
   1.182 +  unfolding eq_def ..
   1.183 +
   1.184 +setup {*
   1.185 +let
   1.186 +  val eq_refl = thm "eq_refl";
   1.187 +  fun normalization_tac i = Tactical.PRIMITIVE (Drule.fconv_rule
   1.188 +    (Drule.goals_conv (equal i) (HOL.Trueprop_conv NBE.normalization_conv)));
   1.189 +  val normalization_meth =
   1.190 +    Method.no_args (Method.METHOD (fn _ => normalization_tac 1 THEN resolve_tac [TrueI, refl, eq_refl] 1));
   1.191 +in
   1.192 +  Method.add_method ("normalization", normalization_meth, "solve goal by normalization")
   1.193 +end;
   1.194 +*}
   1.195 +
   1.196 +hide (open) const eq
   1.197 +
   1.198 +end
   1.199 \ No newline at end of file

     2.1 --- a/src/HOL/Datatype.thy	Mon Oct 16 14:07:21 2006 +0200
     2.2 +++ b/src/HOL/Datatype.thy	Mon Oct 16 14:07:31 2006 +0200
     2.3 @@ -804,7 +804,7 @@
     2.4  code_instance option :: eq
     2.5    (Haskell -)
     2.6  
     2.7 -code_const "OperationalEquality.eq \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool"
     2.8 +code_const "Code_Generator.eq \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool"
     2.9    (Haskell infixl 4 "==")
    2.10  
    2.11  ML

     3.1 --- a/src/HOL/HOL.thy	Mon Oct 16 14:07:21 2006 +0200
     3.2 +++ b/src/HOL/HOL.thy	Mon Oct 16 14:07:31 2006 +0200
     3.3 @@ -954,9 +954,44 @@
     3.4  
     3.5  fun case_tac a = res_inst_tac [("P", a)] case_split;
     3.6  
     3.7 +(* combination of (spec RS spec RS ...(j times) ... spec RS mp) *)
     3.8 +local
     3.9 +  fun wrong_prem (Const ("All", _) $ (Abs (_, _, t))) = wrong_prem t
    3.10 +    | wrong_prem (Bound _) = true
    3.11 +    | wrong_prem _ = false;
    3.12 +  val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.prems_of);
    3.13 +in
    3.14 +  fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp]);
    3.15 +  fun smp_tac j = EVERY'[dresolve_tac (smp j), atac];
    3.16 +end;
    3.17 +
    3.18 +fun strip_tac i = REPEAT (resolve_tac [impI, allI] i);
    3.19 +
    3.20  val Blast_tac = Blast.Blast_tac;
    3.21  val blast_tac = Blast.blast_tac;
    3.22  
    3.23 +fun Trueprop_conv conv ct = (case term_of ct of
    3.24 +    Const ("Trueprop", _) $ _ =>
    3.25 +      let val (ct1, ct2) = Thm.dest_comb ct
    3.26 +      in Thm.combination (Thm.reflexive ct1) (conv ct2) end
    3.27 +  | _ => raise TERM ("Trueprop_conv", []));
    3.28 +
    3.29 +fun constrain_op_eq_thms thy thms =
    3.30 +  let
    3.31 +    fun add_eq (Const ("op =", ty)) =
    3.32 +          fold (insert (eq_fst (op =)))
    3.33 +            (Term.add_tvarsT ty [])
    3.34 +      | add_eq _ =
    3.35 +          I
    3.36 +    val eqs = fold (fold_aterms add_eq o Thm.prop_of) thms [];
    3.37 +    val instT = map (fn (v_i, sort) =>
    3.38 +      (Thm.ctyp_of thy (TVar (v_i, sort)),
    3.39 +         Thm.ctyp_of thy (TVar (v_i, Sorts.inter_sort (Sign.classes_of thy) (sort, [HOLogic.class_eq]))))) eqs;
    3.40 +  in
    3.41 +    thms
    3.42 +    |> map (Thm.instantiate (instT, []))
    3.43 +  end;
    3.44 +
    3.45  end;
    3.46  *}
    3.47  
    3.48 @@ -1428,99 +1463,6 @@
    3.49  setup InductMethod.setup
    3.50  
    3.51  
    3.52 -subsubsection {* Code generator setup *}
    3.53 -
    3.54 -types_code
    3.55 -  "bool"  ("bool")
    3.56 -attach (term_of) {*
    3.57 -fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
    3.58 -*}
    3.59 -attach (test) {*
    3.60 -fun gen_bool i = one_of [false, true];
    3.61 -*}
    3.62 -  "prop"  ("bool")
    3.63 -attach (term_of) {*
    3.64 -fun term_of_prop b =
    3.65 -  HOLogic.mk_Trueprop (if b then HOLogic.true_const else HOLogic.false_const);
    3.66 -*}
    3.67 -
    3.68 -consts_code
    3.69 -  "Trueprop" ("(_)")
    3.70 -  "True"    ("true")
    3.71 -  "False"   ("false")
    3.72 -  "Not"     ("not")
    3.73 -  "op |"    ("(_ orelse/ _)")
    3.74 -  "op &"    ("(_ andalso/ _)")
    3.75 -  "HOL.If"      ("(if _/ then _/ else _)")
    3.76 -
    3.77 -setup {*
    3.78 -let
    3.79 -
    3.80 -fun eq_codegen thy defs gr dep thyname b t =
    3.81 -    (case strip_comb t of
    3.82 -       (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE
    3.83 -     | (Const ("op =", _), [t, u]) =>
    3.84 -          let
    3.85 -            val (gr', pt) = Codegen.invoke_codegen thy defs dep thyname false (gr, t);
    3.86 -            val (gr'', pu) = Codegen.invoke_codegen thy defs dep thyname false (gr', u);
    3.87 -            val (gr''', _) = Codegen.invoke_tycodegen thy defs dep thyname false (gr'', HOLogic.boolT)
    3.88 -          in
    3.89 -            SOME (gr''', Codegen.parens
    3.90 -              (Pretty.block [pt, Pretty.str " =", Pretty.brk 1, pu]))
    3.91 -          end
    3.92 -     | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
    3.93 -         thy defs dep thyname b (gr, Codegen.eta_expand t ts 2))
    3.94 -     | _ => NONE);
    3.95 -
    3.96 -in
    3.97 -
    3.98 -Codegen.add_codegen "eq_codegen" eq_codegen
    3.99 -
   3.100 -end
   3.101 -*}
   3.102 -
   3.103 -setup {*
   3.104 -let
   3.105 -
   3.106 -fun evaluation_tac i = Tactical.PRIMITIVE (Drule.fconv_rule
   3.107 -  (Drule.goals_conv (equal i) Codegen.evaluation_conv));
   3.108 -
   3.109 -val evaluation_meth =
   3.110 -  Method.no_args (Method.METHOD (fn _ => evaluation_tac 1 THEN rtac HOL.TrueI 1));
   3.111 -
   3.112 -in
   3.113 -
   3.114 -Method.add_method ("evaluation", evaluation_meth, "solve goal by evaluation")
   3.115 -
   3.116 -end;
   3.117 -*}
   3.118 -
   3.119 -
   3.120 -text {* itself as a code generator datatype *}
   3.121 -
   3.122 -setup {*
   3.123 -let fun add_itself thy =
   3.124 -  let
   3.125 -    val v = ("'a", []);
   3.126 -    val t = Logic.mk_type (TFree v);
   3.127 -    val Const (c, ty) = t;
   3.128 -    val (_, Type (dtco, _)) = strip_type ty;
   3.129 -  in
   3.130 -    thy
   3.131 -    |> CodegenData.add_datatype (dtco, (([v], [(c, [])]), CodegenData.lazy (fn () => [])))
   3.132 -  end
   3.133 -in add_itself end;
   3.134 -*} 
   3.135 -
   3.136 -text {* code generation for arbitrary as exception *}
   3.137 -
   3.138 -setup {*
   3.139 -  CodegenSerializer.add_undefined "SML" "arbitrary" "(raise Fail \"arbitrary\")"
   3.140 -*}
   3.141 -
   3.142 -code_const arbitrary
   3.143 -  (Haskell target_atom "(error \"arbitrary\")")
   3.144 -
   3.145  
   3.146  subsection {* Other simple lemmas and lemma duplicates *}
   3.147  
   3.148 @@ -1553,29 +1495,4 @@
   3.149    shows "f x (f y z) = f y (f x z)"
   3.150    by (rule trans [OF trans [OF c a] arg_cong [OF c, of "f y"]])
   3.151  
   3.152 -
   3.153 -subsection {* Conclude HOL structure *}
   3.154 -
   3.155 -ML {*
   3.156 -structure HOL =
   3.157 -struct
   3.158 -
   3.159 -open HOL;
   3.160 -
   3.161 -(* combination of (spec RS spec RS ...(j times) ... spec RS mp) *)
   3.162 -local
   3.163 -  fun wrong_prem (Const ("All", _) $ (Abs (_, _, t))) = wrong_prem t
   3.164 -    | wrong_prem (Bound _) = true
   3.165 -    | wrong_prem _ = false;
   3.166 -  val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.prems_of);
   3.167 -in
   3.168 -  fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp]);
   3.169 -  fun smp_tac j = EVERY'[dresolve_tac (smp j), atac];
   3.170 -end;
   3.171 -
   3.172 -fun strip_tac i = REPEAT (resolve_tac [impI, allI] i);
   3.173 -
   3.174 -end;
   3.175 -*}
   3.176 -
   3.177  end

     4.1 --- a/src/HOL/Integ/IntArith.thy	Mon Oct 16 14:07:21 2006 +0200
     4.2 +++ b/src/HOL/Integ/IntArith.thy	Mon Oct 16 14:07:31 2006 +0200
     4.3 @@ -375,7 +375,7 @@
     4.4    "Numeral.Min" "IntDef.min"
     4.5    "Numeral.Bit" "IntDef.bit"
     4.6    "Numeral.bit.bit_case" "IntDef.bit_case"
     4.7 -  "OperationalEquality.eq \<Colon> bit \<Rightarrow> bit \<Rightarrow> bool" "IntDef.eq_bit"
     4.8 +  "Code_Generator.eq \<Colon> bit \<Rightarrow> bit \<Rightarrow> bool" "IntDef.eq_bit"
     4.9    "Numeral.B0" "IntDef.b0"
    4.10    "Numeral.B1" "IntDef.b1"
    4.11  

     5.1 --- a/src/HOL/Integ/IntDef.thy	Mon Oct 16 14:07:21 2006 +0200
     5.2 +++ b/src/HOL/Integ/IntDef.thy	Mon Oct 16 14:07:31 2006 +0200
     5.3 @@ -915,7 +915,7 @@
     5.4  code_instance int :: eq
     5.5    (Haskell -)
     5.6  
     5.7 -code_const "OperationalEquality.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
     5.8 +code_const "Code_Generator.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
     5.9    (SML "(op =) (_ : IntInf.int, _)")
    5.10    (Haskell infixl 4 "==")
    5.11  

     6.1 --- a/src/HOL/Integ/Presburger.thy	Mon Oct 16 14:07:21 2006 +0200
     6.2 +++ b/src/HOL/Integ/Presburger.thy	Mon Oct 16 14:07:31 2006 +0200
     6.3 @@ -10,8 +10,9 @@
     6.4  
     6.5  theory Presburger
     6.6  imports NatSimprocs
     6.7 -uses ("cooper_dec.ML") ("cooper_proof.ML") ("qelim.ML") 
     6.8 -	("reflected_presburger.ML") ("reflected_cooper.ML") ("presburger.ML")
     6.9 +uses
    6.10 +  ("cooper_dec.ML") ("cooper_proof.ML") ("qelim.ML") 
    6.11 +  ("reflected_presburger.ML") ("reflected_cooper.ML") ("presburger.ML")
    6.12  begin
    6.13  
    6.14  text {* Theorem for unitifying the coeffitients of @{text x} in an existential formula*}
    6.15 @@ -1094,7 +1095,7 @@
    6.16  *}
    6.17  
    6.18  lemma eq_number_of [code func]:
    6.19 -  "OperationalEquality.eq ((number_of k)\<Colon>int) (number_of l) \<longleftrightarrow> OperationalEquality.eq k l"
    6.20 +  "Code_Generator.eq ((number_of k)\<Colon>int) (number_of l) \<longleftrightarrow> Code_Generator.eq k l"
    6.21    unfolding number_of_is_id ..
    6.22  
    6.23  lemma less_eq_number_of [code func]:
    6.24 @@ -1102,56 +1103,56 @@
    6.25    unfolding number_of_is_id ..
    6.26  
    6.27  lemma eq_Pls_Pls:
    6.28 -  "OperationalEquality.eq Numeral.Pls Numeral.Pls"
    6.29 +  "Code_Generator.eq Numeral.Pls Numeral.Pls"
    6.30    unfolding eq_def ..
    6.31  
    6.32  lemma eq_Pls_Min:
    6.33 -  "\<not> OperationalEquality.eq Numeral.Pls Numeral.Min"
    6.34 +  "\<not> Code_Generator.eq Numeral.Pls Numeral.Min"
    6.35    unfolding eq_def Pls_def Min_def by auto
    6.36  
    6.37  lemma eq_Pls_Bit0:
    6.38 -  "OperationalEquality.eq Numeral.Pls (Numeral.Bit k bit.B0) \<longleftrightarrow> OperationalEquality.eq Numeral.Pls k"
    6.39 +  "Code_Generator.eq Numeral.Pls (Numeral.Bit k bit.B0) \<longleftrightarrow> Code_Generator.eq Numeral.Pls k"
    6.40    unfolding eq_def Pls_def Bit_def bit.cases by auto
    6.41  
    6.42  lemma eq_Pls_Bit1:
    6.43 -  "\<not> OperationalEquality.eq Numeral.Pls (Numeral.Bit k bit.B1)"
    6.44 +  "\<not> Code_Generator.eq Numeral.Pls (Numeral.Bit k bit.B1)"
    6.45    unfolding eq_def Pls_def Bit_def bit.cases by arith
    6.46  
    6.47  lemma eq_Min_Pls:
    6.48 -  "\<not> OperationalEquality.eq Numeral.Min Numeral.Pls"
    6.49 +  "\<not> Code_Generator.eq Numeral.Min Numeral.Pls"
    6.50    unfolding eq_def Pls_def Min_def by auto
    6.51  
    6.52  lemma eq_Min_Min:
    6.53 -  "OperationalEquality.eq Numeral.Min Numeral.Min"
    6.54 +  "Code_Generator.eq Numeral.Min Numeral.Min"
    6.55    unfolding eq_def ..
    6.56  
    6.57  lemma eq_Min_Bit0:
    6.58 -  "\<not> OperationalEquality.eq Numeral.Min (Numeral.Bit k bit.B0)"
    6.59 +  "\<not> Code_Generator.eq Numeral.Min (Numeral.Bit k bit.B0)"
    6.60    unfolding eq_def Min_def Bit_def bit.cases by arith
    6.61  
    6.62  lemma eq_Min_Bit1:
    6.63 -  "OperationalEquality.eq Numeral.Min (Numeral.Bit k bit.B1) \<longleftrightarrow> OperationalEquality.eq Numeral.Min k"
    6.64 +  "Code_Generator.eq Numeral.Min (Numeral.Bit k bit.B1) \<longleftrightarrow> Code_Generator.eq Numeral.Min k"
    6.65    unfolding eq_def Min_def Bit_def bit.cases by auto
    6.66  
    6.67  lemma eq_Bit0_Pls:
    6.68 -  "OperationalEquality.eq (Numeral.Bit k bit.B0) Numeral.Pls \<longleftrightarrow> OperationalEquality.eq Numeral.Pls k"
    6.69 +  "Code_Generator.eq (Numeral.Bit k bit.B0) Numeral.Pls \<longleftrightarrow> Code_Generator.eq Numeral.Pls k"
    6.70    unfolding eq_def Pls_def Bit_def bit.cases by auto
    6.71  
    6.72  lemma eq_Bit1_Pls:
    6.73 -  "\<not> OperationalEquality.eq (Numeral.Bit k bit.B1) Numeral.Pls"
    6.74 +  "\<not> Code_Generator.eq (Numeral.Bit k bit.B1) Numeral.Pls"
    6.75    unfolding eq_def Pls_def Bit_def bit.cases by arith
    6.76  
    6.77  lemma eq_Bit0_Min:
    6.78 -  "\<not> OperationalEquality.eq (Numeral.Bit k bit.B0) Numeral.Min"
    6.79 +  "\<not> Code_Generator.eq (Numeral.Bit k bit.B0) Numeral.Min"
    6.80    unfolding eq_def Min_def Bit_def bit.cases by arith
    6.81  
    6.82  lemma eq_Bit1_Min:
    6.83 -  "OperationalEquality.eq (Numeral.Bit k bit.B1) Numeral.Min \<longleftrightarrow> OperationalEquality.eq Numeral.Min k"
    6.84 +  "Code_Generator.eq (Numeral.Bit k bit.B1) Numeral.Min \<longleftrightarrow> Code_Generator.eq Numeral.Min k"
    6.85    unfolding eq_def Min_def Bit_def bit.cases by auto
    6.86  
    6.87  lemma eq_Bit_Bit:
    6.88 -  "OperationalEquality.eq (Numeral.Bit k1 v1) (Numeral.Bit k2 v2) \<longleftrightarrow>
    6.89 -    OperationalEquality.eq v1 v2 \<and> OperationalEquality.eq k1 k2"
    6.90 +  "Code_Generator.eq (Numeral.Bit k1 v1) (Numeral.Bit k2 v2) \<longleftrightarrow>
    6.91 +    Code_Generator.eq v1 v2 \<and> Code_Generator.eq k1 k2"
    6.92    unfolding eq_def Bit_def
    6.93    apply (cases v1)
    6.94    apply (cases v2)

     7.1 --- a/src/HOL/IsaMakefile	Mon Oct 16 14:07:21 2006 +0200
     7.2 +++ b/src/HOL/IsaMakefile	Mon Oct 16 14:07:31 2006 +0200
     7.3 @@ -84,7 +84,7 @@
     7.4    $(SRC)/TFL/rules.ML $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML			\
     7.5    $(SRC)/TFL/thry.ML $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML			\
     7.6    Tools/res_atpset.ML \
     7.7 -  Binomial.thy Datatype.ML Datatype.thy			\
     7.8 +  Binomial.thy Code_Generator.thy Datatype.ML Datatype.thy			\
     7.9    Divides.thy						\
    7.10    Equiv_Relations.thy Extraction.thy Finite_Set.ML Finite_Set.thy		\
    7.11    FixedPoint.thy Fun.thy HOL.ML HOL.thy Hilbert_Choice.thy Inductive.thy	\
    7.12 @@ -95,7 +95,7 @@
    7.13    Integ/reflected_cooper.ML Integ/int_arith1.ML Integ/int_factor_simprocs.ML	\
    7.14    Integ/nat_simprocs.ML Integ/presburger.ML Integ/qelim.ML LOrder.thy		\
    7.15    Lattice_Locales.thy List.ML List.thy Main.ML Main.thy Map.thy			\
    7.16 -  Nat.ML Nat.thy NatArith.thy OperationalEquality.thy OrderedGroup.ML OrderedGroup.thy	\
    7.17 +  Nat.ML Nat.thy NatArith.thy OrderedGroup.ML OrderedGroup.thy	\
    7.18    Orderings.ML Orderings.thy Power.thy PreList.thy Product_Type.thy		\
    7.19    ROOT.ML Recdef.thy Reconstruction.thy Record.thy Refute.thy			\
    7.20    Relation.ML Relation.thy Relation_Power.thy Ring_and_Field.thy SAT.thy Set.ML		\

     8.1 --- a/src/HOL/Library/EfficientNat.thy	Mon Oct 16 14:07:21 2006 +0200
     8.2 +++ b/src/HOL/Library/EfficientNat.thy	Mon Oct 16 14:07:31 2006 +0200
     8.3 @@ -53,7 +53,7 @@
     8.4  qed
     8.5  
     8.6  lemma [code inline]:
     8.7 -  "nat_case f g n = (if OperationalEquality.eq n 0 then f else g (nat_of_int (int n - 1)))"
     8.8 +  "nat_case f g n = (if Code_Generator.eq n 0 then f else g (nat_of_int (int n - 1)))"
     8.9    by (cases n) (simp_all add: eq_def nat_of_int_int)
    8.10  
    8.11  text {*
    8.12 @@ -100,7 +100,7 @@
    8.13    by simp
    8.14  lemma [code func, code inline]: "(m \<le> n) \<longleftrightarrow> (int m \<le> int n)"
    8.15    by simp
    8.16 -lemma [code func, code inline]: "OperationalEquality.eq m n \<longleftrightarrow> OperationalEquality.eq (int m) (int n)"
    8.17 +lemma [code func, code inline]: "Code_Generator.eq m n \<longleftrightarrow> Code_Generator.eq (int m) (int n)"
    8.18    unfolding eq_def by simp
    8.19  lemma [code func]: "nat k = (if k < 0 then 0 else nat_of_int k)"
    8.20  proof (cases "k < 0")

     9.1 --- a/src/HOL/Library/ExecutableRat.thy	Mon Oct 16 14:07:21 2006 +0200
     9.2 +++ b/src/HOL/Library/ExecutableRat.thy	Mon Oct 16 14:07:31 2006 +0200
     9.3 @@ -113,7 +113,7 @@
     9.4    "op * \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat" "Rational.erat_times"
     9.5    "inverse  \<Colon> erat \<Rightarrow> erat" "Rational.erat_inverse"
     9.6    "op \<le> \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool" "Rational.erat_le"
     9.7 -  "OperationalEquality.eq \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool" "Rational.erat_eq"
     9.8 +  "Code_Generator.eq \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool" "Rational.erat_eq"
     9.9  
    9.10  
    9.11  section {* rat as abstype *}
    9.12 @@ -127,7 +127,7 @@
    9.13    "op * \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat" \<equiv> "op * \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat"
    9.14    "inverse \<Colon> rat \<Rightarrow> rat" \<equiv> "inverse \<Colon> erat \<Rightarrow> erat"
    9.15    "op \<le> \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" \<equiv>  "op \<le> \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool"
    9.16 -   "OperationalEquality.eq \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" \<equiv> eq_erat
    9.17 +   "Code_Generator.eq \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" \<equiv> eq_erat
    9.18  
    9.19  code_const div_zero
    9.20    (SML "raise/ (Fail/ \"Division by zero\")")
    9.21 @@ -142,7 +142,7 @@
    9.22    "op * \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat"
    9.23    "inverse \<Colon> rat \<Rightarrow> rat"
    9.24    "op \<le> \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool"
    9.25 -   "OperationalEquality.eq \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool"
    9.26 +   "Code_Generator.eq \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool"
    9.27    (SML -)
    9.28  
    9.29  

    10.1 --- a/src/HOL/Library/ExecutableSet.thy	Mon Oct 16 14:07:21 2006 +0200
    10.2 +++ b/src/HOL/Library/ExecutableSet.thy	Mon Oct 16 14:07:31 2006 +0200
    10.3 @@ -18,7 +18,7 @@
    10.4    by blast
    10.5  
    10.6  lemma [code func]:
    10.7 -  "OperationalEquality.eq A B = (A \<subseteq> B \<and> B \<subseteq> A)"
    10.8 +  "Code_Generator.eq A B = (A \<subseteq> B \<and> B \<subseteq> A)"
    10.9    unfolding eq_def by blast
   10.10  
   10.11  declare bex_triv_one_point1 [symmetric, standard, code]

    11.1 --- a/src/HOL/List.thy	Mon Oct 16 14:07:21 2006 +0200
    11.2 +++ b/src/HOL/List.thy	Mon Oct 16 14:07:31 2006 +0200
    11.3 @@ -2764,10 +2764,10 @@
    11.4  code_instance list :: eq and char :: eq
    11.5    (Haskell - and -)
    11.6  
    11.7 -code_const "OperationalEquality.eq \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool"
    11.8 +code_const "Code_Generator.eq \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool"
    11.9    (Haskell infixl 4 "==")
   11.10  
   11.11 -code_const "OperationalEquality.eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
   11.12 +code_const "Code_Generator.eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
   11.13    (Haskell infixl 4 "==")
   11.14  
   11.15  setup {*

    12.1 --- a/src/HOL/OperationalEquality.thy	Mon Oct 16 14:07:21 2006 +0200
    12.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.3 @@ -1,112 +0,0 @@
    12.4 -(*  ID:         $Id$
    12.5 -    Author:     Florian Haftmann, TU Muenchen
    12.6 -*)
    12.7 -
    12.8 -header {* Operational equality for code generation *}
    12.9 -
   12.10 -theory OperationalEquality
   12.11 -imports HOL
   12.12 -begin
   12.13 -
   12.14 -section {* Operational equality for code generation *}
   12.15 -
   12.16 -subsection {* eq class *}
   12.17 -
   12.18 -class eq =
   12.19 -  fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   12.20 -
   12.21 -defs
   12.22 -  eq_def: "eq x y \<equiv> (x = y)"
   12.23 -
   12.24 -
   12.25 -subsection {* bool type *}
   12.26 -
   12.27 -instance bool :: eq ..
   12.28 -
   12.29 -lemma [code func]:
   12.30 -  "eq True p = p" unfolding eq_def by auto
   12.31 -
   12.32 -lemma [code func]:
   12.33 -  "eq False p = (\<not> p)" unfolding eq_def by auto
   12.34 -
   12.35 -lemma [code func]:
   12.36 -  "eq p True = p" unfolding eq_def by auto
   12.37 -
   12.38 -lemma [code func]:
   12.39 -  "eq p False = (\<not> p)" unfolding eq_def by auto
   12.40 -
   12.41 -
   12.42 -subsection {* code generator setup *}
   12.43 -
   12.44 -subsubsection {* preprocessor *}
   12.45 -
   12.46 -setup {*
   12.47 -let
   12.48 -  val class_eq = "OperationalEquality.eq";
   12.49 -  fun constrain_op_eq thy ts =
   12.50 -    let
   12.51 -      fun add_eq (Const ("op =", ty)) =
   12.52 -            fold (insert (eq_fst (op = : indexname * indexname -> bool)))
   12.53 -              (Term.add_tvarsT ty [])
   12.54 -        | add_eq _ =
   12.55 -            I
   12.56 -      val eqs = (fold o fold_aterms) add_eq ts [];
   12.57 -      val inst = map (fn (v_i, _) => (v_i, [class_eq])) eqs;
   12.58 -    in inst end;
   12.59 -in CodegenData.add_constrains constrain_op_eq end
   12.60 -*}
   12.61 -
   12.62 -declare eq_def [symmetric, code inline]
   12.63 -
   12.64 -code_constname
   12.65 -  "eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool" "HOL.eq_bool"
   12.66 -
   12.67 -
   12.68 -subsection {* haskell setup *}
   12.69 -
   12.70 -code_class eq
   12.71 -  (Haskell "Eq" where eq \<equiv> "(==)")
   12.72 -
   12.73 -code_const eq
   12.74 -  (Haskell infixl 4 "==")
   12.75 -
   12.76 -code_instance bool :: eq
   12.77 -  (Haskell -)
   12.78 -
   12.79 -code_const "eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
   12.80 -  (Haskell infixl 4 "==")
   12.81 -
   12.82 -
   12.83 -subsection {* nbe setup *}
   12.84 -
   12.85 -lemma eq_refl: "eq x x"
   12.86 -  unfolding eq_def ..
   12.87 -
   12.88 -setup {*
   12.89 -let
   12.90 -
   12.91 -val eq_refl = thm "eq_refl";
   12.92 -
   12.93 -fun Trueprop_conv conv ct = (case term_of ct of
   12.94 -    Const ("Trueprop", _) $ _ =>
   12.95 -      let val (ct1, ct2) = Thm.dest_comb ct
   12.96 -      in Thm.combination (Thm.reflexive ct1) (conv ct2) end
   12.97 -  | _ => raise TERM ("Trueprop_conv", []));
   12.98 -
   12.99 -fun normalization_tac i = Tactical.PRIMITIVE (Drule.fconv_rule
  12.100 -  (Drule.goals_conv (equal i) (Trueprop_conv NBE.normalization_conv)));
  12.101 -
  12.102 -val normalization_meth =
  12.103 -  Method.no_args (Method.METHOD (fn _ => normalization_tac 1 THEN resolve_tac [TrueI, refl, eq_refl] 1));
  12.104 -
  12.105 -in
  12.106 -
  12.107 -Method.add_method ("normalization", normalization_meth, "solve goal by normalization")
  12.108 -
  12.109 -end;
  12.110 -*}
  12.111 -
  12.112 -
  12.113 -hide (open) const eq
  12.114 -
  12.115 -end
  12.116 \ No newline at end of file

    13.1 --- a/src/HOL/Presburger.thy	Mon Oct 16 14:07:21 2006 +0200
    13.2 +++ b/src/HOL/Presburger.thy	Mon Oct 16 14:07:31 2006 +0200
    13.3 @@ -10,8 +10,9 @@
    13.4  
    13.5  theory Presburger
    13.6  imports NatSimprocs
    13.7 -uses ("cooper_dec.ML") ("cooper_proof.ML") ("qelim.ML") 
    13.8 -	("reflected_presburger.ML") ("reflected_cooper.ML") ("presburger.ML")
    13.9 +uses
   13.10 +  ("cooper_dec.ML") ("cooper_proof.ML") ("qelim.ML") 
   13.11 +  ("reflected_presburger.ML") ("reflected_cooper.ML") ("presburger.ML")
   13.12  begin
   13.13  
   13.14  text {* Theorem for unitifying the coeffitients of @{text x} in an existential formula*}
   13.15 @@ -1094,7 +1095,7 @@
   13.16  *}
   13.17  
   13.18  lemma eq_number_of [code func]:
   13.19 -  "OperationalEquality.eq ((number_of k)\<Colon>int) (number_of l) \<longleftrightarrow> OperationalEquality.eq k l"
   13.20 +  "Code_Generator.eq ((number_of k)\<Colon>int) (number_of l) \<longleftrightarrow> Code_Generator.eq k l"
   13.21    unfolding number_of_is_id ..
   13.22  
   13.23  lemma less_eq_number_of [code func]:
   13.24 @@ -1102,56 +1103,56 @@
   13.25    unfolding number_of_is_id ..
   13.26  
   13.27  lemma eq_Pls_Pls:
   13.28 -  "OperationalEquality.eq Numeral.Pls Numeral.Pls"
   13.29 +  "Code_Generator.eq Numeral.Pls Numeral.Pls"
   13.30    unfolding eq_def ..
   13.31  
   13.32  lemma eq_Pls_Min:
   13.33 -  "\<not> OperationalEquality.eq Numeral.Pls Numeral.Min"
   13.34 +  "\<not> Code_Generator.eq Numeral.Pls Numeral.Min"
   13.35    unfolding eq_def Pls_def Min_def by auto
   13.36  
   13.37  lemma eq_Pls_Bit0:
   13.38 -  "OperationalEquality.eq Numeral.Pls (Numeral.Bit k bit.B0) \<longleftrightarrow> OperationalEquality.eq Numeral.Pls k"
   13.39 +  "Code_Generator.eq Numeral.Pls (Numeral.Bit k bit.B0) \<longleftrightarrow> Code_Generator.eq Numeral.Pls k"
   13.40    unfolding eq_def Pls_def Bit_def bit.cases by auto
   13.41  
   13.42  lemma eq_Pls_Bit1:
   13.43 -  "\<not> OperationalEquality.eq Numeral.Pls (Numeral.Bit k bit.B1)"
   13.44 +  "\<not> Code_Generator.eq Numeral.Pls (Numeral.Bit k bit.B1)"
   13.45    unfolding eq_def Pls_def Bit_def bit.cases by arith
   13.46  
   13.47  lemma eq_Min_Pls:
   13.48 -  "\<not> OperationalEquality.eq Numeral.Min Numeral.Pls"
   13.49 +  "\<not> Code_Generator.eq Numeral.Min Numeral.Pls"
   13.50    unfolding eq_def Pls_def Min_def by auto
   13.51  
   13.52  lemma eq_Min_Min:
   13.53 -  "OperationalEquality.eq Numeral.Min Numeral.Min"
   13.54 +  "Code_Generator.eq Numeral.Min Numeral.Min"
   13.55    unfolding eq_def ..
   13.56  
   13.57  lemma eq_Min_Bit0:
   13.58 -  "\<not> OperationalEquality.eq Numeral.Min (Numeral.Bit k bit.B0)"
   13.59 +  "\<not> Code_Generator.eq Numeral.Min (Numeral.Bit k bit.B0)"
   13.60    unfolding eq_def Min_def Bit_def bit.cases by arith
   13.61  
   13.62  lemma eq_Min_Bit1:
   13.63 -  "OperationalEquality.eq Numeral.Min (Numeral.Bit k bit.B1) \<longleftrightarrow> OperationalEquality.eq Numeral.Min k"
   13.64 +  "Code_Generator.eq Numeral.Min (Numeral.Bit k bit.B1) \<longleftrightarrow> Code_Generator.eq Numeral.Min k"
   13.65    unfolding eq_def Min_def Bit_def bit.cases by auto
   13.66  
   13.67  lemma eq_Bit0_Pls:
   13.68 -  "OperationalEquality.eq (Numeral.Bit k bit.B0) Numeral.Pls \<longleftrightarrow> OperationalEquality.eq Numeral.Pls k"
   13.69 +  "Code_Generator.eq (Numeral.Bit k bit.B0) Numeral.Pls \<longleftrightarrow> Code_Generator.eq Numeral.Pls k"
   13.70    unfolding eq_def Pls_def Bit_def bit.cases by auto
   13.71  
   13.72  lemma eq_Bit1_Pls:
   13.73 -  "\<not> OperationalEquality.eq (Numeral.Bit k bit.B1) Numeral.Pls"
   13.74 +  "\<not> Code_Generator.eq (Numeral.Bit k bit.B1) Numeral.Pls"
   13.75    unfolding eq_def Pls_def Bit_def bit.cases by arith
   13.76  
   13.77  lemma eq_Bit0_Min:
   13.78 -  "\<not> OperationalEquality.eq (Numeral.Bit k bit.B0) Numeral.Min"
   13.79 +  "\<not> Code_Generator.eq (Numeral.Bit k bit.B0) Numeral.Min"
   13.80    unfolding eq_def Min_def Bit_def bit.cases by arith
   13.81  
   13.82  lemma eq_Bit1_Min:
   13.83 -  "OperationalEquality.eq (Numeral.Bit k bit.B1) Numeral.Min \<longleftrightarrow> OperationalEquality.eq Numeral.Min k"
   13.84 +  "Code_Generator.eq (Numeral.Bit k bit.B1) Numeral.Min \<longleftrightarrow> Code_Generator.eq Numeral.Min k"
   13.85    unfolding eq_def Min_def Bit_def bit.cases by auto
   13.86  
   13.87  lemma eq_Bit_Bit:
   13.88 -  "OperationalEquality.eq (Numeral.Bit k1 v1) (Numeral.Bit k2 v2) \<longleftrightarrow>
   13.89 -    OperationalEquality.eq v1 v2 \<and> OperationalEquality.eq k1 k2"
   13.90 +  "Code_Generator.eq (Numeral.Bit k1 v1) (Numeral.Bit k2 v2) \<longleftrightarrow>
   13.91 +    Code_Generator.eq v1 v2 \<and> Code_Generator.eq k1 k2"
   13.92    unfolding eq_def Bit_def
   13.93    apply (cases v1)
   13.94    apply (cases v2)

    14.1 --- a/src/HOL/Product_Type.thy	Mon Oct 16 14:07:21 2006 +0200
    14.2 +++ b/src/HOL/Product_Type.thy	Mon Oct 16 14:07:31 2006 +0200
    14.3 @@ -764,7 +764,7 @@
    14.4  instance unit :: eq ..
    14.5  
    14.6  lemma [code func]:
    14.7 -  "OperationalEquality.eq (u\<Colon>unit) v = True" unfolding eq_def unit_eq [of u] unit_eq [of v] by rule+
    14.8 +  "Code_Generator.eq (u\<Colon>unit) v = True" unfolding eq_def unit_eq [of u] unit_eq [of v] by rule+
    14.9  
   14.10  code_instance unit :: eq
   14.11    (Haskell -)
   14.12 @@ -772,16 +772,16 @@
   14.13  instance * :: (eq, eq) eq ..
   14.14  
   14.15  lemma [code func]:
   14.16 -  "OperationalEquality.eq (x1, y1) (x2, y2) = (OperationalEquality.eq x1 x2 \<and> OperationalEquality.eq y1 y2)"
   14.17 +  "Code_Generator.eq (x1, y1) (x2, y2) = (Code_Generator.eq x1 x2 \<and> Code_Generator.eq y1 y2)"
   14.18    unfolding eq_def by auto
   14.19  
   14.20  code_instance * :: eq
   14.21    (Haskell -)
   14.22  
   14.23 -code_const "OperationalEquality.eq \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
   14.24 +code_const "Code_Generator.eq \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
   14.25    (Haskell infixl 4 "==")
   14.26  
   14.27 -code_const "OperationalEquality.eq \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
   14.28 +code_const "Code_Generator.eq \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
   14.29    (Haskell infixl 4 "==")
   14.30  
   14.31  types_code

    15.1 --- a/src/HOL/Sum_Type.thy	Mon Oct 16 14:07:21 2006 +0200
    15.2 +++ b/src/HOL/Sum_Type.thy	Mon Oct 16 14:07:31 2006 +0200
    15.3 @@ -197,19 +197,19 @@
    15.4  instance "+" :: (eq, eq) eq ..
    15.5  
    15.6  lemma [code func]:
    15.7 -  "OperationalEquality.eq (Inl x) (Inl y) = OperationalEquality.eq x y"
    15.8 +  "Code_Generator.eq (Inl x) (Inl y) = Code_Generator.eq x y"
    15.9    unfolding eq_def Inl_eq ..
   15.10  
   15.11  lemma [code func]:
   15.12 -  "OperationalEquality.eq (Inr x) (Inr y) = OperationalEquality.eq x y"
   15.13 +  "Code_Generator.eq (Inr x) (Inr y) = Code_Generator.eq x y"
   15.14    unfolding eq_def Inr_eq ..
   15.15  
   15.16  lemma [code func]:
   15.17 -  "OperationalEquality.eq (Inl x) (Inr y) = False"
   15.18 +  "Code_Generator.eq (Inl x) (Inr y) = False"
   15.19    unfolding eq_def using Inl_not_Inr by auto
   15.20  
   15.21  lemma [code func]:
   15.22 -  "OperationalEquality.eq (Inr x) (Inl y) = False"
   15.23 +  "Code_Generator.eq (Inr x) (Inl y) = False"
   15.24    unfolding eq_def using Inr_not_Inl by auto
   15.25  
   15.26  ML

    16.1 --- a/src/HOL/Tools/datatype_codegen.ML	Mon Oct 16 14:07:21 2006 +0200
    16.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Mon Oct 16 14:07:31 2006 +0200
    16.3 @@ -490,30 +490,14 @@
    16.4  
    16.5  local
    16.6    val eq_def_sym = thm "eq_def" |> Thm.symmetric;
    16.7 -  val class_eq = "OperationalEquality.eq";
    16.8    fun get_eq_thms thy tyco = case DatatypePackage.get_datatype thy tyco
    16.9     of SOME _ => get_eq_datatype thy tyco
   16.10      | NONE => [TypecopyPackage.get_eq thy tyco];
   16.11 -  fun constrain_op_eq_thms thy thms =
   16.12 -    let
   16.13 -      fun add_eq (Const ("op =", ty)) =
   16.14 -            fold (insert (eq_fst (op =)))
   16.15 -              (Term.add_tvarsT ty [])
   16.16 -        | add_eq _ =
   16.17 -            I
   16.18 -      val eqs = fold (fold_aterms add_eq o Thm.prop_of) thms [];
   16.19 -      val instT = map (fn (v_i, sort) =>
   16.20 -        (Thm.ctyp_of thy (TVar (v_i, sort)),
   16.21 -           Thm.ctyp_of thy (TVar (v_i, Sorts.inter_sort (Sign.classes_of thy) (sort, [class_eq]))))) eqs;
   16.22 -    in
   16.23 -      thms
   16.24 -      |> map (Thm.instantiate (instT, []))
   16.25 -    end;
   16.26  in
   16.27    fun get_eq thy tyco =
   16.28      get_eq_thms thy tyco
   16.29      |> maps ((#mk o #mk_rews o snd o MetaSimplifier.rep_ss o Simplifier.simpset_of) thy)
   16.30 -    |> constrain_op_eq_thms thy
   16.31 +    |> HOL.constrain_op_eq_thms thy
   16.32      |> map (Tactic.rewrite_rule [eq_def_sym])
   16.33  end;
   16.34  
   16.35 @@ -615,15 +599,13 @@
   16.36  
   16.37  (* operational equality *)
   16.38  
   16.39 -local
   16.40 -  val class_eq = "OperationalEquality.eq";
   16.41 -in fun eq_hook specs =
   16.42 +fun eq_hook specs =
   16.43    let
   16.44      fun add_eq_thms (dtco, (_, (vs, cs))) thy =
   16.45        let
   16.46          val thy_ref = Theory.self_ref thy;
   16.47          val ty = Type (dtco, map TFree vs) |> Logic.varifyT;
   16.48 -        val c = CodegenConsts.norm thy ("OperationalEquality.eq", [ty]);
   16.49 +        val c = CodegenConsts.norm thy ("Code_Generator.eq", [ty]);
   16.50          val get_thms = (fn () => get_eq (Theory.deref thy_ref) dtco |> rev);
   16.51        in
   16.52          CodegenData.add_funcl (c, CodegenData.lazy get_thms) thy
   16.53 @@ -631,9 +613,8 @@
   16.54    in
   16.55      prove_codetypes_arities (K (ClassPackage.intro_classes_tac []))
   16.56        (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
   16.57 -      [class_eq] ((K o K o pair) []) ((K o K) (fold add_eq_thms specs))
   16.58 +      [HOLogic.class_eq] ((K o K o pair) []) ((K o K) (fold add_eq_thms specs))
   16.59    end;
   16.60 -end; (*local*)
   16.61  
   16.62  
   16.63  

    17.1 --- a/src/HOL/Tools/meson.ML	Mon Oct 16 14:07:21 2006 +0200
    17.2 +++ b/src/HOL/Tools/meson.ML	Mon Oct 16 14:07:31 2006 +0200
    17.3 @@ -204,7 +204,7 @@
    17.4  fun resop nf [prem] = resolve_tac (nf prem) 1;
    17.5  
    17.6  (*Any need to extend this list with 
    17.7 -  "HOL.type_class","OperationalEquality.eq_class","ProtoPure.term"?*)
    17.8 +  "HOL.type_class","Code_Generator.eq_class","ProtoPure.term"?*)
    17.9  val has_meta_conn = 
   17.10      exists_Const (fn (c,_) => c mem_string ["==", "==>", "all", "prop"]);
   17.11  

    18.1 --- a/src/HOL/ex/Codegenerator.thy	Mon Oct 16 14:07:21 2006 +0200
    18.2 +++ b/src/HOL/ex/Codegenerator.thy	Mon Oct 16 14:07:31 2006 +0200
    18.3 @@ -184,16 +184,16 @@
    18.4    "op mod :: int \<Rightarrow> int \<Rightarrow> int"  
    18.5    (SML) (Haskell)
    18.6  code_gen
    18.7 -  "OperationalEquality.eq :: bool \<Rightarrow> bool \<Rightarrow> bool"
    18.8 -  "OperationalEquality.eq :: nat \<Rightarrow> nat \<Rightarrow> bool"
    18.9 -  "OperationalEquality.eq :: int \<Rightarrow> int \<Rightarrow> bool"
   18.10 -  "OperationalEquality.eq :: ('a\<Colon>eq) * ('b\<Colon>eq) \<Rightarrow> 'a * 'b \<Rightarrow> bool"
   18.11 -  "OperationalEquality.eq :: ('a\<Colon>eq) + ('b\<Colon>eq) \<Rightarrow> 'a + 'b \<Rightarrow> bool"
   18.12 -  "OperationalEquality.eq :: ('a\<Colon>eq) option \<Rightarrow> 'a option \<Rightarrow> bool"
   18.13 -  "OperationalEquality.eq :: ('a\<Colon>eq) list \<Rightarrow> 'a list \<Rightarrow> bool"
   18.14 -  "OperationalEquality.eq :: mut1 \<Rightarrow> mut1 \<Rightarrow> bool"
   18.15 -  "OperationalEquality.eq :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
   18.16 -  "OperationalEquality.eq :: ('a\<Colon>eq) point_scheme \<Rightarrow> 'a point_scheme \<Rightarrow> bool"
   18.17 +  "Code_Generator.eq :: bool \<Rightarrow> bool \<Rightarrow> bool"
   18.18 +  "Code_Generator.eq :: nat \<Rightarrow> nat \<Rightarrow> bool"
   18.19 +  "Code_Generator.eq :: int \<Rightarrow> int \<Rightarrow> bool"
   18.20 +  "Code_Generator.eq :: ('a\<Colon>eq) * ('b\<Colon>eq) \<Rightarrow> 'a * 'b \<Rightarrow> bool"
   18.21 +  "Code_Generator.eq :: ('a\<Colon>eq) + ('b\<Colon>eq) \<Rightarrow> 'a + 'b \<Rightarrow> bool"
   18.22 +  "Code_Generator.eq :: ('a\<Colon>eq) option \<Rightarrow> 'a option \<Rightarrow> bool"
   18.23 +  "Code_Generator.eq :: ('a\<Colon>eq) list \<Rightarrow> 'a list \<Rightarrow> bool"
   18.24 +  "Code_Generator.eq :: mut1 \<Rightarrow> mut1 \<Rightarrow> bool"
   18.25 +  "Code_Generator.eq :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
   18.26 +  "Code_Generator.eq :: ('a\<Colon>eq) point_scheme \<Rightarrow> 'a point_scheme \<Rightarrow> bool"
   18.27  
   18.28  code_gen (SML -)
   18.29  

    19.1 --- a/src/HOL/ex/NormalForm.thy	Mon Oct 16 14:07:21 2006 +0200
    19.2 +++ b/src/HOL/ex/NormalForm.thy	Mon Oct 16 14:07:31 2006 +0200
    19.3 @@ -127,8 +127,8 @@
    19.4  
    19.5  hide (open) const delayed_if
    19.6  
    19.7 -normal_form "OperationalEquality.eq [2..<4] [2,3]"
    19.8 -(*lemma "OperationalEquality.eq [2..<4] [2,3]" by normalization*)
    19.9 +normal_form "Code_Generator.eq [2..<4] [2,3]"
   19.10 +(*lemma "Code_Generator.eq [2..<4] [2,3]" by normalization*)
   19.11  
   19.12  definition
   19.13   andalso :: "bool \<Rightarrow> bool \<Rightarrow> bool"