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



Dear Andrei,

Thank you very much for your kind support at
	https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-August/msg00099.html
which I really appreciate.

I was wondering whether it would be possible to create declarations separated 
from definitions without (!) overloading in the current Isabelle version 
(2016). Such attempts were rejected by the current Isabelle version (see 
attached theory CircularDefs). So it seems that overall your approach is 
successful in preventing the kind of inconsistency described in your article.

Also, I tried to express your (OndÅej's) definitions in the R0 implementation 
and obtained interesting results on the methods preventing such paradoxes. I 
shall write more about it in a separate e-mail soon.

Kind regards,

Ken Kubota

____________________

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


Attachment: CircularDefs.thy
Description: Binary data



theory CircularDefs imports Main
begin

consts c1_bool :: bool
consts c2_bool :: bool

definition c1_bool where
  "c1_bool = (if c2_bool then False else True)"
(* ERROR: Duplicate constant declaration "CircularDefs.c1_bool" vs. "CircularDefs.c1_bool" *)

definition c2_bool where
  "c2_bool = (if c1_bool then True else False)"
(* ERROR: Duplicate constant declaration "CircularDefs.c2_bool" vs. "CircularDefs.c2_bool" *)

end



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