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

[Lawrence Paulson]

A solution to the more general problem (identifying if the variable is constrained by other theorems) would be even better. I have just remembered that I always advise people to use “auto” prior to trying sledgehammer, because it will split up the subgoal into manageable parts and simplify them. This is bad advice if “auto” can render the problem impossible to prove.

Larry

On 15 Jun 2010, at 10:17, Jasmin Christian Blanchette wrote:

> 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
>