# 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 \ 'a \ bool" where "eq x x" + +lemma eq_is_eq: "eq x y \ (x = y)" +by (rule eq_reflection) (auto intro: eq.intros elim: eq.cases) + no_notation inf (infixl "\" 70) and sup (infixl "\" 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 *)