Re: [isabelle] Atomisation of free variables



Hallo,

apparently not. My lemma looks like this:

lemma "x ≥ (0::real) ⟹ x*x ≥ 0"

I would now like to apply some tactic to rewrite this to "∀x. x ≥
(0::real) ⟶ x*x ≥ 0".

For some odd reason, your code seems to loop indefinitely on this
example when I try to turn it into a tactic.

Manuel


On 09.09.2014 18:51, René Thiemann wrote:
>> Dear Manuel,
>>
>> I don't know whether this is exactly what you want, but perhaps the following snippet is of help:
>>
>> consts P :: "'a ⇒ 'b ⇒ 'c ⇒ bool"
>> consts Q :: "'a ⇒ 'b ⇒ 'c ⇒ bool"
>>
>> axiomatization where foo: "P a b c ⟹ Q a b c"
>>
>> ML {*
>> fun transform ctxt thm =  
>>   let 
>>     val thm' = forall_intr_vars thm
>>     val meta_eq = Object_Logic.atomize ctxt (cprop_of thm')
>>   in
>>     Raw_Simplifier.rewrite_rule ctxt [meta_eq] thm'
>>   end
>>
>> val new_thm = transform @{context} @{thm foo}
>>
>> *}
>>
>> Best,
>> René





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