Re: [isabelle-dev] Global constant names in inductive

[Lars Hupel]

> Your proposed change
> https://isabelle.in.tum.de/repos/testboard/rev/20d5e446aa10 looks
> formally OK.

See now Isabelle/3c628937899d and AFP/a7160ffc25f1.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Global constant names in inductive

[Makarius]

On 06/04/17 13:08, Lars Hupel wrote:
>> Did you encounter an actual problem from that situation?
>>
>> Formally, a comment is not a problem. "Fixing" such things prematurely
>> is likely to break it.
> 
> Yes, there is an actual problem. I define a function via
> "Function.add_function" and inspect the resulting info. As per usual
> discipline this looks as follows:

> That is, I inspect the relation as generated by the function package.
> The termination proof needs to get some information about that relation
> from the inductive package. However, "#R" is a term, not a const name
> string. Before I close the target, it will be a free variable.

OK, that is a better motivation.

Your proposed change
https://isabelle.in.tum.de/repos/testboard/rev/20d5e446aa10 looks
formally OK.


My old comment from 10-years ago stems from:

changeset:   25380:03201004c77e
user:wenzelm
date:Sat Nov 10 18:36:08 2007 +0100
files:   src/HOL/Tools/inductive_package.ML
description:
put_inductives: be permissive about multiple versions
  (target names are not necessarily unique);
add_inductive: store info under global (!) name -- very rough
approximation of the real thing;


That historical context is important. Isabelle development means to
study sources + history carefully and to make empiric explorations
against current applications (notably AFP).

The date above reminds me of chaotic times in 2006/2007 when far too
many things were changed without clear principles.


Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Global constant names in inductive

[Lars Hupel]

> Did you encounter an actual problem from that situation?
> 
> Formally, a comment is not a problem. "Fixing" such things prematurely
> is likely to break it.

Yes, there is an actual problem. I define a function via
"Function.add_function" and inspect the resulting info. As per usual
discipline this looks as follows:

val (info, (lthy', lthy)) = lthy'
  |> tap print_info
  |> Local_Theory.open_target |> snd
  |> Function.add_function bindings specs fun_config
   pat_completeness_auto
  |> (fn (info, lthy) => prove_termination lthy (#R info))
  ||> `Local_Theory.close_target

That is, I inspect the relation as generated by the function package.
The termination proof needs to get some information about that relation
from the inductive package. However, "#R" is a term, not a const name
string. Before I close the target, it will be a free variable.

With my change, I can lookup the inductive based on the term. Otherwise,
I'd need to construct the constant name and look it up using that.

Cheers
Lars
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Global constant names in inductive

[Makarius]

On 06/04/17 09:29, Lars Hupel wrote:
> while poking around in the function package (to store more information
> in "info"), I also realized that I need a little bit more information
> from the inductive package.
> 
> Reading its sources, I stumbled upon 10-year-old comments by Makarius
> that remind the reader of (what I assume is) non-canonical use of global
> constant names in a "Generic_Data" slot.
> 
> I took a stab at changing this to use item nets (as it is done in the
> function package). The draft patch is here:

Did you encounter an actual problem from that situation?

Formally, a comment is not a problem. "Fixing" such things prematurely
is likely to break it.


Makarius


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Global constant names in inductive

[Lars Hupel]

Dear list,

while poking around in the function package (to store more information
in "info"), I also realized that I need a little bit more information
from the inductive package.

Reading its sources, I stumbled upon 10-year-old comments by Makarius
that remind the reader of (what I assume is) non-canonical use of global
constant names in a "Generic_Data" slot.

I took a stab at changing this to use item nets (as it is done in the
function package). The draft patch is here:

  

Unfortunately, this breaks HOL-Proofs-Lambda with a rather mysterious

  exception THM 1 raised (line 741 of "thm.ML"): assume: variables

I'm at a loss for an explanation. Does anybody have any idea what is
going on there?

Cheers
Lars
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev