Re: [isabelle-dev] Example for global interpretation into instantiation [was: Future of permanent_interpretation]

[Florian Haftmann]

Hi Clemens,

> I didn't have time to look at your patches, and since I only have
superficial knowledge of instantiation contexts I didn't fully
understand the example either.  I guess though that the purpose of these
global interpretations is to propagate some constant declarations into
the surrounding theory.  If this is useful we should certainly have such
a command.

thanks for looking into that.

> What I still fail to understand is why you want to use 'global_interpretation'
as keyword if the command occurs directly in a theory.  This is
redundant.  I now take this as a temporary solution until there is some
better terminology for distinguishing kinds of interpretations, and I
very much hope that we will not get into another debate about renaming
'interpretation' to 'global_interpretation' or similar after the 2016
release.

I am personally very comfortable with the situation »as it is« by now
and I am convinced there is now much time to breathe before we have to
make any final decisions on that matter.

Enjoy your time,
Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] Example for global interpretation into instantiation [was: Future of permanent_interpretation]

[Clemens Ballarin]

Hi Florian,

I didn't have time to look at your patches, and since I only have superficial 
knowledge of instantiation contexts I didn't fully understand the example 
either.  I guess though that the purpose of these global interpretations is to 
propagate some constant declarations into the surrounding theory.  If this is 
useful we should certainly have such a command.

What I still fail to understand is why you want to use 'global_interpretation' 
as keyword if the command occurs directly in a theory.  This is redundant.  I 
now take this as a temporary solution until there is some better terminology 
for distinguishing kinds of interpretations, and I very much hope that we will 
not get into another debate about renaming 'interpretation' to 
'global_interpretation' or similar after the 2016 release.

Clemens


On 17 December, 2015 17:49 CET, Florian Haftmann 
 wrote: 
 
> Hi Clemens,
> 
> I have found a potential example for global interpretation into
> instantiation in the existing Isabelle sources.
> 
> The example is presented in the attached patches, which can be applied
> in alphabetical order on top of 32a530a5c54c.
> 
> The first patch experimentally introduces a global_interpretation
> keyword, which is then used in theory src/HOL/Library/Saturated.thy:
> 
> instantiation sat :: (len) "{Inf, Sup}"
> begin
> 
> global_interpretation Inf_sat: semilattice_neutr_set min "top :: 'a sat"
>   defines Inf_sat = Inf_sat.F
>   by standard (simp add: min_def)
> 
> global_interpretation Sup_sat: semilattice_neutr_set max "bot :: 'a sat"
>   defines Sup_sat = Sup_sat.F
>   by standard (simp add: max_def bot.extremum_unique)
> 
> end
> 
> Here we have a clear distinction between interpretation, which would
> only last until the closing end, and the explicitly permanent global
> interpretation which provides the necessary instance definitions.
> 
> This pattern, which uses interpretation as a kind of simple definitional
> package, is very common nowadays, as can be seen in theories like
> src/HOL/Groups_Big.thy, src/HOL/Groups_List.thy,
> src/HOL/Lattices_Big.thy or src/HOL/Library/Multiset.thy.
> 
> I have prepared this to give some evidence that my insistence on proper
> distinction between (confined) interpretation and (permanent) global
> interpretation has significant practical implications (although the
> experimental nature of the patches exhibits some issues in the internal
> machinery which would have to worked out properly first).  So, it is
> really a good idea to have a separate keyword »global_interpretation«.
> 
> Hence, before letting »permanent_interpretation« stand as it is, I would
> really prefer to replace the existing occurrences by
> »global_interpretation«, to avoid confusion in the long run.
> 
> So, my minimal plan for the upcoming release would be:
> * Provide »global_interpretation« as separate keyword.
> * Discontinue »permanent_interpretation« entirely – remaining
> occurrences are suitable for »global_interpretation«.
> * »interpretation« retains its current traditional semantics.  No
> systematic replacement by »global_interpretation«.
> * Polish the documentation accordingly.
> 
> I have no idea whether you have a time slot to consider and give
> feedback on this; anyway this plan is quite minimal invasive wrt.
> existing sources, so I am confident that it is appropriate for the
> upcoming release.
> 
> All the best,
> Florian
> 
> -- 
> 
> PGP available:
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
 
 
 
 


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

[isabelle-dev] Example for global interpretation into instantiation [was: Future of permanent_interpretation]

[Florian Haftmann]

Hi Clemens,

I have found a potential example for global interpretation into
instantiation in the existing Isabelle sources.

The example is presented in the attached patches, which can be applied
in alphabetical order on top of 32a530a5c54c.

The first patch experimentally introduces a global_interpretation
keyword, which is then used in theory src/HOL/Library/Saturated.thy:

instantiation sat :: (len) "{Inf, Sup}"
begin

global_interpretation Inf_sat: semilattice_neutr_set min "top :: 'a sat"
  defines Inf_sat = Inf_sat.F
  by standard (simp add: min_def)

global_interpretation Sup_sat: semilattice_neutr_set max "bot :: 'a sat"
  defines Sup_sat = Sup_sat.F
  by standard (simp add: max_def bot.extremum_unique)

end

Here we have a clear distinction between interpretation, which would
only last until the closing end, and the explicitly permanent global
interpretation which provides the necessary instance definitions.

This pattern, which uses interpretation as a kind of simple definitional
package, is very common nowadays, as can be seen in theories like
src/HOL/Groups_Big.thy, src/HOL/Groups_List.thy,
src/HOL/Lattices_Big.thy or src/HOL/Library/Multiset.thy.

I have prepared this to give some evidence that my insistence on proper
distinction between (confined) interpretation and (permanent) global
interpretation has significant practical implications (although the
experimental nature of the patches exhibits some issues in the internal
machinery which would have to worked out properly first).  So, it is
really a good idea to have a separate keyword »global_interpretation«.

Hence, before letting »permanent_interpretation« stand as it is, I would
really prefer to replace the existing occurrences by
»global_interpretation«, to avoid confusion in the long run.

So, my minimal plan for the upcoming release would be:
* Provide »global_interpretation« as separate keyword.
* Discontinue »permanent_interpretation« entirely – remaining
occurrences are suitable for »global_interpretation«.
* »interpretation« retains its current traditional semantics.  No
systematic replacement by »global_interpretation«.
* Polish the documentation accordingly.

I have no idea whether you have a time slot to consider and give
feedback on this; anyway this plan is quite minimal invasive wrt.
existing sources, so I am confident that it is appropriate for the
upcoming release.

All the best,
Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
# HG changeset patch
# Parent 32a530a5c54cfa3bd5263600e3bdfae87153627e

diff -r 32a530a5c54c src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thyWed Dec 16 17:30:30 2015 +0100
+++ b/src/HOL/Finite_Set.thyThu Dec 17 17:34:35 2015 +0100
@@ -1209,7 +1209,7 @@
   But now that we have @{const fold} things are easy:
 \
 
-permanent_interpretation card: folding "\_. Suc" 0
+global_interpretation card: folding "\_. Suc" 0
   defines card = "folding.F (\_. Suc) 0"
   by standard rule
 
diff -r 32a530a5c54c src/HOL/IMP/Abs_Int1_const.thy
--- a/src/HOL/IMP/Abs_Int1_const.thyWed Dec 16 17:30:30 2015 +0100
+++ b/src/HOL/IMP/Abs_Int1_const.thyThu Dec 17 17:34:35 2015 +0100
@@ -53,7 +53,7 @@
 end
 
 
-permanent_interpretation Val_semilattice
+global_interpretation Val_semilattice
 where \ = \_const and num' = Const and plus' = plus_const
 proof (standard, goal_cases)
   case (1 a b) thus ?case
@@ -66,7 +66,7 @@
   case 4 thus ?case by(auto simp: plus_const_cases split: const.split)
 qed
 
-permanent_interpretation Abs_Int
+global_interpretation Abs_Int
 where \ = \_const and num' = Const and plus' = plus_const
 defines AI_const = AI and step_const = step' and aval'_const = aval'
 ..
@@ -120,7 +120,7 @@
 
 text{* Monotonicity: *}
 
-permanent_interpretation Abs_Int_mono
+global_interpretation Abs_Int_mono
 where \ = \_const and num' = Const and plus' = plus_const
 proof (standard, goal_cases)
   case 1 thus ?case by(auto simp: plus_const_cases split: const.split)
@@ -131,7 +131,7 @@
 definition m_const :: "const \ nat" where
 "m_const x = (if x = Any then 0 else 1)"
 
-permanent_interpretation Abs_Int_measure
+global_interpretation Abs_Int_measure
 where \ = \_const and num' = Const and plus' = plus_const
 and m = m_const and h = "1"
 proof (standard, goal_cases)
diff -r 32a530a5c54c src/HOL/IMP/Abs_Int1_parity.thy
--- a/src/HOL/IMP/Abs_Int1_parity.thy   Wed Dec 16 17:30:30 2015 +0100
+++ b/src/HOL/IMP/Abs_Int1_parity.thy   Thu Dec 17 17:34:35 2015 +0100
@@ -102,7 +102,7 @@
 text{* First we instantiate the abstract value interface and prove that the
 functions on type @{typ parity} have all the necessary properties: *}
 
-permanent_interpretation Val_semilattice
+global_interpretation Val_semilattice
 where \ = \_parity and num' = num_parity and plus' = plus_parity
 proof (standard, goal_cases) txt{* subgoals are the locale axioms *}
   case 1 thus ?case by(auto simp: less_eq_parity_def)
@@ -124,7 +124,7 @@
 proofs (they