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



Using the current Isabelle 2016, it is not possible for me to reproduce the problem.

If I understand Andrei Popescu and Makarius Wenzel correctly,
declarations of constants earlier than and separated from their definitions should be possible, 
but circular dependencies not anymore in the 2016 version of Isabelle.
Nevertheless, the error message reports a problem with the definition of the constant,
even if circularity is avoided by removing 'c' from tau ('T').

Could you please provide a working example (for the 2016 version of Isabelle)
by correcting my attempt (shown with the results below)?

Please note that line "consts c:Î" ("consts c:alpha") at
	http://www21.in.tum.de/~kuncar/kuncar-popescu-jar2016.pdf (p. 3)
still differs from line "consts c :: bool" in
	http://www21.in.tum.de/~kuncar/documents/False.tar.gz
available via
	http://www21.in.tum.de/~kuncar/documents/patch.html

Ken Kubota



(* using 'a, "(overloaded)", "definition", and c is removed from T  *)

consts c :: 'a

typedef (overloaded) T = "{True}" by blast

definition c_bool_def: 
  "c::bool â if (â(x::T) y. x = y) then False else True"
(*ERROR: Bad head of lhs: existing constant "c"*)


(* using 'a, "(overloaded)" and "definition" *)

consts c :: 'a

typedef (overloaded) T = "{True, c}" by blast

definition c_bool_def: 
  "c::bool â if (â(x::T) y. x = y) then False else True"
(*ERROR: Bad head of lhs: existing constant "c"*)


(* using "(overloaded)" and "definition" *)

consts c :: bool

typedef (overloaded) T = "{True, c}" by blast

definition c_bool_def: 
  "c::bool â if (â(x::T) y. x = y) then False else True"
(*ERROR: Bad head of lhs: existing constant "c"*)


(* original version by Ondrej Kuncar, with "defs" *)

consts c :: bool

typedef T = "{True, c}" by blast

defs c_bool_def: 
  "c::bool â if (â(x::T) y. x = y) then False else True"
(* several errors in current Isabelle 2016 *)



> Am 21.08.2016 um 21:17 schrieb OndÅej KunÄar <kuncar at in.tum.de>:
> 
> On 08/21/2016 07:35 PM, Ken Kubota wrote:
>> Dear Andrei,
>> 
>> Thank you for the quick answer, and also thanks to Larry Paulson and Makarius Wenzel.
>> 
>> I had read the abbreviated notation with the forall quantifier too quickly, but still the third restriction specified at
>>       http://sourceforge.net/projects/hol/files/hol/kananaskis-10/kananaskis-10-logic.pdf (p. 33) or at [Gordon/Melham, 1993, p. 220].
>> seems to be violated, as the type variable sigma occurs in the definiens, but not in (the type of) the definiendum.
> 
> That's a typo, that type should be tau, the type that was defined on the previous line. I've already uploaded an updated version of the draft.
> 
> Btw, we usually use alpha, beta, gamma for type variables, not sigma. But this is not mentioned until page 7.
> 
> Ondrej

____________________

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





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