[isabelle-dev] [isabelle] safe for boolean equality

[Jasmin Christian Blanchette]

Am 15.06.2010 um 11:03 schrieb Lawrence Paulson:

> Altering the behaviour of the safe method on locale constants might be feasible, because it would affect only a few proofs. Can anybody tell me whether there is an easy way to identify whether a free variable is actually a locale constant?

I ran into the same problem in Nitpick and solved it with the following (ugly) code:

ML {*
fun is_fixed_equation fixes
                      (Const (@{const_name "=="}, _) $ Free (s, _) $ Const _) =
    member (op =) fixes s
  | is_fixed_equation _ _ = false
fun extract_fixed_frees ctxt assms =
  let
    val fixes = Variable.fixes_of ctxt |> map snd
    val (subst, other_assms) =
      List.partition (is_fixed_equation fixes) assms
      |>> map Logic.dest_equals
  in (subst, other_assms) end
*}

The function "extract_fixed_frees" returns the "Free" constants as well as their definition. Examples:

function f where
"f 0 = 0" |
"f (Suc x) = x"
ML_val {* extract_fixed_frees @{context} (map term_of (Assumption.all_assms_of @{context})) *}
oops

lemma "f x = f y"
ML_val {* extract_fixed_frees @{context} (map term_of (Assumption.all_assms_of @{context})) *}
oops

I wouldn't be surprised if there's a better way of achieving the same effect.

Jasmin