# HG changeset patch
# User bulwahn
# Date 1240391423 -7200
# Node ID 95f66b234086d32a18656b417ca592d32c5db19b
# Parent  bd4f255837e51acbb023419bc8b88af30667d53d
added general preprocessing of equality in predicates for code generation

diff -r bd4f255837e5 -r 95f66b234086 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Tue Apr 21 09:53:31 2009 +0200
+++ b/src/HOL/Predicate.thy	Wed Apr 22 11:10:23 2009 +0200
@@ -622,6 +622,11 @@
   "pred_rec f P = f (eval P)"
   by (cases P) simp
 
+inductive eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where "eq x x"
+
+lemma eq_is_eq: "eq x y \<equiv> (x = y)"
+by (rule eq_reflection) (auto intro: eq.intros elim: eq.cases)
+
 no_notation
   inf (infixl "\<sqinter>" 70) and
   sup (infixl "\<squnion>" 65) and
@@ -633,6 +638,6 @@
 
 hide (open) type pred seq
 hide (open) const Pred eval single bind if_pred not_pred
-  Empty Insert Join Seq member pred_of_seq "apply" adjunct
+  Empty Insert Join Seq member pred_of_seq "apply" adjunct eq
 
 end
diff -r bd4f255837e5 -r 95f66b234086 src/HOL/ex/predicate_compile.ML
--- a/src/HOL/ex/predicate_compile.ML	Tue Apr 21 09:53:31 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML	Wed Apr 22 11:10:23 2009 +0200
@@ -726,15 +726,15 @@
     Const ("Trueprop", _) $ _ => Conv.arg_conv cv ct  
   | _ => error "Trueprop_conv"
 
-fun preprocess_intro thy rule = Thm.transfer thy rule (*FIXME preprocessor
+fun preprocess_intro thy rule =
   Conv.fconv_rule
     (imp_prems_conv
-      (Trueprop_conv (Conv.try_conv (Conv.rewr_conv (Thm.symmetric @ {thm Predicate.eq_is_eq})))))
-    (Thm.transfer thy rule) *)
+      (Trueprop_conv (Conv.try_conv (Conv.rewr_conv (Thm.symmetric @{thm Predicate.eq_is_eq})))))
+    (Thm.transfer thy rule)
 
-fun preprocess_elim thy nargs elimrule = (*FIXME preprocessor -- let
+fun preprocess_elim thy nargs elimrule = let
    fun replace_eqs (Const ("Trueprop", _) $ (Const ("op =", T) $ lhs $ rhs)) =
-      HOLogic.mk_Trueprop (Const (@ {const_name Predicate.eq}, T) $ lhs $ rhs)
+      HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs)
     | replace_eqs t = t
    fun preprocess_case t = let
      val params = Logic.strip_params t
@@ -746,10 +746,10 @@
    val elimrule' = Logic.list_implies ((hd prems) :: cases', Thm.concl_of elimrule)
  in
    Thm.equal_elim
-     (Thm.symmetric (Conv.implies_concl_conv (MetaSimplifier.rewrite true [@ {thm eq_is_eq}])
+     (Thm.symmetric (Conv.implies_concl_conv (MetaSimplifier.rewrite true [@{thm eq_is_eq}])
         (cterm_of thy elimrule')))
      elimrule
- end*) elimrule;
+ end;
 
 
 (* returns true if t is an application of an datatype constructor *)