# HG changeset patch
# User Lukas Bulwahn <lukas.bulwahn@gmail.com>
# Date 1452453690 -3600
# Node ID c8a93680b80d7494785e446adf326f52a1cf4781
# Parent  a7cf464933f778844dd50fe7df96b1ae50cdf733
filter non-matching prems rather than fail in proof procedure in rare cases; include derived example motivating change and some similar other ones

diff -r a7cf464933f7 -r c8a93680b80d src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Sat Jan 09 22:22:17 2016 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Sun Jan 10 20:21:30 2016 +0100
@@ -85,10 +85,47 @@
 
 inductive Fact :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
 where
-"Fact a' a'"
+  "Fact a' a'"
 
 code_pred (expected_modes: o => o => bool, i => o => bool, o => i => bool, i => i => bool) Fact .
 
+text {*
+  The following example was derived from an predicate in the CakeML formalisation provided by Lars Hupel.
+*}
+inductive predicate_where_argument_is_condition :: "bool \<Rightarrow> bool"
+where
+  "ck \<Longrightarrow> predicate_where_argument_is_condition ck"
+
+code_pred predicate_where_argument_is_condition .
+
+text {* Other similar examples of this kind: *}
+
+inductive predicate_where_argument_is_in_equation :: "bool \<Rightarrow> bool"
+where
+  "ck = True \<Longrightarrow> predicate_where_argument_is_in_equation ck"
+
+code_pred predicate_where_argument_is_in_equation .
+
+inductive predicate_where_argument_is_condition_and_value :: "bool \<Rightarrow> bool"
+where
+  "predicate_where_argument_is_condition_and_value ck \<Longrightarrow> ck
+     \<Longrightarrow> predicate_where_argument_is_condition_and_value ck"
+
+code_pred predicate_where_argument_is_condition_and_value .
+
+inductive predicate_where_argument_is_neg_condition :: "bool \<Rightarrow> bool"
+where
+  "\<not> ck \<Longrightarrow> predicate_where_argument_is_neg_condition ck"
+
+code_pred predicate_where_argument_is_neg_condition .
+
+inductive predicate_where_argument_is_neg_condition_and_in_equation :: "bool \<Rightarrow> bool"
+where
+  "\<not> ck \<Longrightarrow> ck = False \<Longrightarrow> predicate_where_argument_is_neg_condition_and_in_equation ck"
+
+code_pred predicate_where_argument_is_neg_condition_and_in_equation .
+
+
 inductive zerozero :: "nat * nat => bool"
 where
   "zerozero (0, 0)"
diff -r a7cf464933f7 -r c8a93680b80d src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Sat Jan 09 22:22:17 2016 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Sun Jan 10 20:21:30 2016 +0100
@@ -195,6 +195,7 @@
            (fn {context = ctxt', prems, ...} =>
             let
               val prems' = maps dest_conjunct_prem (take nargs prems)
+                |> filter is_equationlike
             in
               rewrite_goal_tac ctxt' (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
             end) ctxt 1