--- a/src/HOL/IsaMakefile Tue Sep 19 15:22:05 2006 +0200
+++ b/src/HOL/IsaMakefile Tue Sep 19 15:22:21 2006 +0200
@@ -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 OrderedGroup.ML OrderedGroup.thy \
+ Nat.ML Nat.thy NatArith.thy OperationalEquality.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 \
@@ -647,7 +647,7 @@
ex/Abstract_NAT.thy ex/Antiquote.thy ex/BT.thy ex/BinEx.thy \
ex/Chinese.thy ex/Classical.thy ex/Classpackage.thy ex/CodeCollections.thy \
ex/CodeEmbed.thy ex/CodeRandom.thy ex/CodeRevappl.thy \
- ex/CodeOperationalEquality.thy ex/Codegenerator.thy ex/Commutative_RingEx.thy \
+ ex/Codegenerator.thy ex/Commutative_RingEx.thy \
ex/Commutative_Ring_Complete.thy ex/Guess.thy ex/Hebrew.thy \
ex/Higher_Order_Logic.thy ex/Hilbert_Classical.thy ex/InSort.thy \
ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy \
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/OperationalEquality.thy Tue Sep 19 15:22:21 2006 +0200
@@ -0,0 +1,130 @@
+(* 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)"
+
+ML {*
+local
+ val thy = the_context ();
+ val const_eq = Sign.intern_const thy "eq";
+ val type_bool = Type (Sign.intern_type thy "bool", []);
+in
+ val eq_def_sym = Thm.symmetric (thm "eq_def");
+ val class_eq = Sign.intern_class thy "eq";
+end
+*}
+
+
+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 {* preprocessor *}
+
+ML {*
+fun constrain_op_eq thy thms =
+ 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 (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;
+*}
+
+
+subsection {* codegenerator setup *}
+
+setup {*
+ CodegenData.add_preproc constrain_op_eq
+*}
+
+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