[isabelle] odd behaviour of simplifier




In the following output

Level 4 (2 subgoals)
bv_to_obin (norm_signed bs) = mk_norm_obin (bv_to_obin bs)
 1. !!a list.
       [| bs = a # list; a = \<zero> |]
       ==> bv_to_obin (norm_signed bs) = mk_norm_obin (bv_to_obin bs)
 2. !!a list.
       [| bs = a # list; a = \<one> |]
       ==> bv_to_obin (norm_signed bs) = mk_norm_obin (bv_to_obin bs)
val it = () : unit
> by    (ALLGOALS (asm_simp_tac (simpset () addsimps [norm_signed_Cons])))
# ;
### Warning: same as previous level
Level 5 (2 subgoals)
bv_to_obin (norm_signed bs) = mk_norm_obin (bv_to_obin bs)
 1. !!a list.
       [| bs = a # list; a = \<zero> |]
       ==> bv_to_obin (norm_signed bs) = mk_norm_obin (bv_to_obin bs)
 2. !!a list.
       [| bs = a # list; a = \<one> |]
       ==> bv_to_obin (norm_signed bs) = mk_norm_obin (bv_to_obin bs)
val it = () : unit
> by    (ALLGOALS (asm_simp_tac (simpset () addsimps [])))
# ;
Level 6 (2 subgoals)
bv_to_obin (norm_signed bs) = mk_norm_obin (bv_to_obin bs)
 1. !!a list.
       [| bs = a # list; a = \<zero> |]
       ==> bv_to_obin (norm_signed (\<zero> # list)) =
           mk_norm_obin (bv_to_obin_aux oPls list)
 2. !!a list.
       [| bs = a # list; a = \<one> |]
       ==> bv_to_obin (norm_signed (\<one> # list)) =
           mk_norm_obin (bv_to_obin_aux oMin list)
val it = () : unit

In the first simplification step - using
(asm_simp_tac (simpset () addsimps [norm_signed_Cons]))
the simplifier does not use the subgoal assumptions to simplify the
conclusion.

In the second step, using (asm_simp_tac (simpset () addsimps [])),
it does.

I've never noticed this sort of behaviour before.
This is using a recent development version of Isabelle.

Why is this?

Regards,

Jeremy





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.