Re: [isabelle] Type definitions in Isabelle; article "A Consistent Foundation for Isabelle/HOL" by Kunčar/Popescu



Dear Andrei,

Answering a private communication, I referred to your paper on Isabelle/HOL
as well as to Peter Homeier’s HOL-Omega TUTORIAL in a reply at
	http://owlofminerva.net/kubota/r0-faq/

Regards,

Ken

____________________________________________________

Ken Kubota
http://doi.org/10.4444/100



> Am 26.08.2016 um 16:55 schrieb Andrei Popescu <A.Popescu at mdx.ac.uk>:
> 
> Dear Ken, 
> 
> >> My suspicion is that declarations separated from definitions generally might cause inconsistency. 
> 
> Actually, this is precisely what we prove in our paper: that, under the described checks, delayed ad hoc overloaded definitions of constants (performed via declarations followed by definitions of instances at later times) and type definitions are jointly consistent under HOL deduction.  
> 
> >> In order to experiment, I would need some hint how declarations of 
> constants (accompanied with a latter definition) work in Isabelle 2016, as asked for at
>         https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-August/msg00093.html
> as I couldn't find any information in the manuals about it.
> 
> In Isabelle 2016, you have to be more explicit about overloading -- see section 11.3 (ad hoc overloading for constants) in the reference manual:    http://isabelle.in.tum.de/doc/isar-ref.pdf
> 
> Your noncircular example should be written as follows: 
> 
> consts c :: 'a
> 
> typedef T = "{True}" by blast
> 
> overloading
>   c_bool    ≡ "c :: bool"   
> begin
> definition c_bool :: bool where
>   "c_bool = (if (EX (x::T). ALL y. x = y) then False else True)"
> end
> 
> By contrast, Ondra's circular example fails in Isabelle 2016: 
> 
> consts cc :: 'a
> 
> typedef (overloaded) TT = "{True,cc}" by blast
> 
> overloading
>   cc_bool    ≡ "cc :: bool"   
> begin
> definition cc_bool :: bool where
>   "cc_bool = (if (EX (x::TT). ALL y. x = y) then False else True)"
> end
> 
> The theory is also attached. 
> 
> Andrei 
> <Defs.thy>





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