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
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
