author haftmann Fri, 07 Mar 2008 13:53:08 +0100 changeset 26239 e105d24d15c1 parent 26238 c30bb8182da2 child 26240 cc630a75b62a
some steps towards a refined treatment of equality
--- a/src/Pure/Isar/code_unit.ML	Fri Mar 07 13:53:07 2008 +0100
+++ b/src/Pure/Isar/code_unit.ML	Fri Mar 07 13:53:08 2008 +0100
@@ -20,6 +20,7 @@
val constrain_thm: sort -> thm -> thm

(*constants*)
+  val add_const_ident: thm -> theory -> theory
val string_of_typ: theory -> typ -> string
val string_of_const: theory -> string -> string
val no_args: theory -> string -> int
@@ -159,7 +160,7 @@
in uncurry match end;

-(* making rewrite theorems *)
+(* rewrite theorems *)

fun assert_rew thm =
let
@@ -200,7 +201,31 @@
end;

-(* making defining equations *)
+(* defining equations *)
+
+structure ConstIdent = TheoryDataFun
+(
+  type T = thm list;
+  val empty = [];
+  val copy = I;
+  val extend = copy;
+  fun merge _ = Library.merge Thm.eq_thm_prop;
+);
+
+  let
+    val t = Thm.prop_of thm;
+    val lhs_rhs = case try Logic.dest_equals t
+     of SOME lhs_rhs => lhs_rhs
+      | _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm);
+    val _ = if can (pairself dest_Const) lhs_rhs then ()
+      else bad_thm ("Not an equation with two constants: " ^ Display.string_of_thm thm);
+  in ConstIdent.map (cons thm) end;
+
+fun apply_ident thm =
+  let
+    val thy = Thm.theory_of_thm thm;
+  in MetaSimplifier.rewrite_rule (ConstIdent.get thy) thm end;

fun assert_func thm =
let
@@ -233,7 +258,7 @@
val _ = map (check 0) args;
in thm end;

-val mk_func = assert_func o mk_rew;
+val mk_func = apply_ident o assert_func o mk_rew;