filter non-matching prems rather than fail in proof procedure in rare cases; include derived example motivating change and some similar other ones
authorLukas Bulwahn <lukas.bulwahn@gmail.com>
Sun Jan 10 20:21:30 2016 +0100 (2016-01-10)
changeset 62121c8a93680b80d
parent 62114 a7cf464933f7
child 62122 eed7ca453573
filter non-matching prems rather than fail in proof procedure in rare cases; include derived example motivating change and some similar other ones
src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Sat Jan 09 22:22:17 2016 +0100
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Sun Jan 10 20:21:30 2016 +0100
     1.3 @@ -85,10 +85,47 @@
     1.4  
     1.5  inductive Fact :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
     1.6  where
     1.7 -"Fact a' a'"
     1.8 +  "Fact a' a'"
     1.9  
    1.10  code_pred (expected_modes: o => o => bool, i => o => bool, o => i => bool, i => i => bool) Fact .
    1.11  
    1.12 +text {*
    1.13 +  The following example was derived from an predicate in the CakeML formalisation provided by Lars Hupel.
    1.14 +*}
    1.15 +inductive predicate_where_argument_is_condition :: "bool \<Rightarrow> bool"
    1.16 +where
    1.17 +  "ck \<Longrightarrow> predicate_where_argument_is_condition ck"
    1.18 +
    1.19 +code_pred predicate_where_argument_is_condition .
    1.20 +
    1.21 +text {* Other similar examples of this kind: *}
    1.22 +
    1.23 +inductive predicate_where_argument_is_in_equation :: "bool \<Rightarrow> bool"
    1.24 +where
    1.25 +  "ck = True \<Longrightarrow> predicate_where_argument_is_in_equation ck"
    1.26 +
    1.27 +code_pred predicate_where_argument_is_in_equation .
    1.28 +
    1.29 +inductive predicate_where_argument_is_condition_and_value :: "bool \<Rightarrow> bool"
    1.30 +where
    1.31 +  "predicate_where_argument_is_condition_and_value ck \<Longrightarrow> ck
    1.32 +     \<Longrightarrow> predicate_where_argument_is_condition_and_value ck"
    1.33 +
    1.34 +code_pred predicate_where_argument_is_condition_and_value .
    1.35 +
    1.36 +inductive predicate_where_argument_is_neg_condition :: "bool \<Rightarrow> bool"
    1.37 +where
    1.38 +  "\<not> ck \<Longrightarrow> predicate_where_argument_is_neg_condition ck"
    1.39 +
    1.40 +code_pred predicate_where_argument_is_neg_condition .
    1.41 +
    1.42 +inductive predicate_where_argument_is_neg_condition_and_in_equation :: "bool \<Rightarrow> bool"
    1.43 +where
    1.44 +  "\<not> ck \<Longrightarrow> ck = False \<Longrightarrow> predicate_where_argument_is_neg_condition_and_in_equation ck"
    1.45 +
    1.46 +code_pred predicate_where_argument_is_neg_condition_and_in_equation .
    1.47 +
    1.48 +
    1.49  inductive zerozero :: "nat * nat => bool"
    1.50  where
    1.51    "zerozero (0, 0)"
     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Sat Jan 09 22:22:17 2016 +0100
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Sun Jan 10 20:21:30 2016 +0100
     2.3 @@ -195,6 +195,7 @@
     2.4             (fn {context = ctxt', prems, ...} =>
     2.5              let
     2.6                val prems' = maps dest_conjunct_prem (take nargs prems)
     2.7 +                |> filter is_equationlike
     2.8              in
     2.9                rewrite_goal_tac ctxt' (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
    2.10              end) ctxt 1