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

Attachment: CircularDefs.thy
Description: Binary data

theory CircularDefs imports Main

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" *)


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