[isabelle-dev] [isabelle] safe for boolean equality
Jasmin Christian Blanchette
jasmin.blanchette at gmail.com
Tue Jun 15 11:17:41 CEST 2010
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
More information about the isabelle-dev
mailing list