Re: [isabelle-dev] Shadowing of theorem names in locales
On Tue, 11 Feb 2014, Clemens Ballarin wrote: For the processing of locale expression, facts are not really required. Having all information related to syntax should be sufficient. I cannot tell, though, whether facts may contain syntax in disguise of certain attributes. In principle there could be arbitrary declarations disguised as declaration attributes of facts, but the general sanity assumption is that this is not done. The separate concept of syntax_declaration was introduced for that, when we sorted this out several years ago. On 10 February, 2014 16:14 CET, Makarius makar...@sketis.net wrote: There is a more general problem behind this: re-initializing a locale context is quite expensive, but we traditionally do this at certain important checkpoints when processing locale expressions. For example, in AFP/JinjaThreads the time for defining some huge locales is dominated by that re-init phase for the imports, and later only few facts are actually required. Several minutes (hours?) could probably be saved by maintaining facts within the context in a lazy manner: the name space is strict, but its values are only produced on demand. I have no clear idea, though, how that would impact practical realiablity of locale expressions. Or is that actually an answer to the problem above: assuming that re-init is fast, it could be done more often to check the name space, but its transformed results remain unchecked. I've done 1-2 rounds through the fact name spaces in the past few weeks, and will probably came back to it again soon. My present idea is to see if the application of notes could be made strict but asynchronous (using Execution.fork) like Goal.prove_future, but on the application of the composed chain of morphisms. By retaining strictness we have two potential advantages: (1) reliable information about failure at the end of the session, and (2) the interactive user can more readily access facts in find_theorems (otherwise there could be minutes to wait before all propositions of the facts space become available). This is a bit speculative at the moment, until I dive again into the sources again to explore the situation. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Shadowing of theorem names in locales
On 21 March, 2014 17:26 CET, Makarius makar...@sketis.net wrote: On Tue, 11 Feb 2014, Clemens Ballarin wrote: For the processing of locale expression, facts are not really required. Having all information related to syntax should be sufficient. I cannot tell, though, whether facts may contain syntax in disguise of certain attributes. In principle there could be arbitrary declarations disguised as declaration attributes of facts, but the general sanity assumption is that this is not done. The separate concept of syntax_declaration was introduced for that, when we sorted this out several years ago. To be more precise about what I had said above: I actually believe that syntax is only required when parsing a locale (i.e. reading it for the first time). When activating it later, everything should be set, and the syntax should no longer matter. Clemens ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Shadowing of theorem names in locales
This does not exhibit itself until the compromised locale context is (re-)entered, and I think this is not desirable. My first spontaneous thought is that strictness should not apply during the initialisation of a locale context. I wouldn't want to add special treatment for this. Currently we can only ensure that a locale is intact by visiting its context. It would be better if integrity checking could be done in an incremental fashion. But that would require much more sophistication. Or is that actually an answer to the problem above: assuming that re-init is fast, it could be done more often to check the name space, but its transformed results remain unchecked. My thought are also going in that direction of »early checking«, e.g. getting feedback when something is going to be compromised rather at a later (unrelated) re-entering of a locale context. 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] Shadowing of theorem names in locales
For the processing of locale expression, facts are not really required. Having all information related to syntax should be sufficient. I cannot tell, though, whether facts may contain syntax in disguise of certain attributes. Clemens On 10 February, 2014 16:14 CET, Makarius makar...@sketis.net wrote: On Fri, 10 Jan 2014, Clemens Ballarin wrote: This does not exhibit itself until the compromised locale context is (re-)entered, and I think this is not desirable. My first spontaneous thought is that strictness should not apply during the initialisation of a locale context. I wouldn't want to add special treatment for this. Currently we can only ensure that a locale is intact by visiting its context. It would be better if integrity checking could be done in an incremental fashion. But that would require much more sophistication. There is a more general problem behind this: re-initializing a locale context is quite expensive, but we traditionally do this at certain important checkpoints when processing locale expressions. For example, in AFP/JinjaThreads the time for defining some huge locales is dominated by that re-init phase for the imports, and later only few facts are actually required. Several minutes (hours?) could probably be saved by maintaining facts within the context in a lazy manner: the name space is strict, but its values are only produced on demand. I have no clear idea, though, how that would impact practical realiablity of locale expressions. Or is that actually an answer to the problem above: assuming that re-init is fast, it could be done more often to check the name space, but its transformed results remain unchecked. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Shadowing of theorem names in locales
On Fri, 10 Jan 2014, Clemens Ballarin wrote: This does not exhibit itself until the compromised locale context is (re-)entered, and I think this is not desirable. My first spontaneous thought is that strictness should not apply during the initialisation of a locale context. I wouldn't want to add special treatment for this. Currently we can only ensure that a locale is intact by visiting its context. It would be better if integrity checking could be done in an incremental fashion. But that would require much more sophistication. There is a more general problem behind this: re-initializing a locale context is quite expensive, but we traditionally do this at certain important checkpoints when processing locale expressions. For example, in AFP/JinjaThreads the time for defining some huge locales is dominated by that re-init phase for the imports, and later only few facts are actually required. Several minutes (hours?) could probably be saved by maintaining facts within the context in a lazy manner: the name space is strict, but its values are only produced on demand. I have no clear idea, though, how that would impact practical realiablity of locale expressions. Or is that actually an answer to the problem above: assuming that re-init is fast, it could be done more often to check the name space, but its transformed results remain unchecked. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Shadowing of theorem names in locales
On 28 December, 2013 19:53 CET, Florian Haftmann florian.haftm...@informatik.tu-muenchen.de wrote: HOL-Complex now builds with strict naming policy for facts (again). Thanks, that's cool. I have stumbled over something which needs some consideration: with strict naming policy, locales can be compromised by »injecting« duplicate facts to imported locales. That's not cool, but I would say that is a user error. There are other ways of compromising locales, for example with the sublocale command. This does not exhibit itself until the compromised locale context is (re-)entered, and I think this is not desirable. My first spontaneous thought is that strictness should not apply during the initialisation of a locale context. I wouldn't want to add special treatment for this. Currently we can only ensure that a locale is intact by visiting its context. It would be better if integrity checking could be done in an incremental fashion. But that would require much more sophistication. Clemens ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Shadowing of theorem names in locales
Quoting Florian Haftmann florian.haftm...@informatik.tu-muenchen.de:
If you point we to particular
occurences, I am willing to polish them accordingly.
There are several versions of bounded_iff in the locales of that
theory (and lattice locales from imported theories). To find all
problematic theorems, you probably want to apply Makarius' ch-strict
patch. I attach this and the other one from his original message.
The second patch no longer applies, though.
Clemens
# HG changeset patch
# User wenzelm
# Date 1349877701 -7200
# Node ID f1455859ff039bb15cb2ff451cc2eb91cb14116b
# Parent 28e37eab4e6fa7065d872ae8fcc5978a93ea0845
strict namespace policy for local facts, in correspondance with local terms
(cf. Variable.is_body);
diff -r 28e37eab4e6f -r f1455859ff03 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.MLWed Oct 10 15:39:01 2012 +0200
+++ b/src/Pure/Isar/proof_context.MLWed Oct 10 16:01:41 2012 +0200
@@ -952,7 +952,8 @@
val (res, ctxt') = fold_map app facts ctxt;
val thms = Global_Theory.name_thms false false name (flat res);
val Mode {stmt, ...} = get_mode ctxt;
- in ((name, thms), ctxt' | update_thms {strict = false, index = stmt} (b,
SOME thms)) end);
+val strict = not (Variable.is_body ctxt);
+ in ((name, thms), ctxt' | update_thms {strict = strict, index = stmt} (b,
SOME thms)) end);
fun put_thms index thms ctxt = ctxt
| map_naming (K Name_Space.local_naming)
# HG changeset patch
# User wenzelm
# Date 1349877725 -7200
# Node ID 9e0ea0b5bab5f5c7de77f135a21d76f763d22c47
# Parent f1455859ff039bb15cb2ff451cc2eb91cb14116b
some attempts to accomodate strict facts;
diff -r f1455859ff03 -r 9e0ea0b5bab5 src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy Wed Oct 10 16:01:41 2012 +0200
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy Wed Oct 10 16:02:05 2012 +0200
@@ -74,7 +74,7 @@
iter' m n f x =
(let f' = (\lambday. x \squnion f y) in iter_down f' n (iter_up f' m x))
-lemma iter'_pfp_above:
+lemma WN_iter'_pfp_above:
shows f(iter' m n f x0) \sqsubseteq iter' m n f x0
and x0 \sqsubseteq iter' m n f x0
using iter_up_pfp[of \lambdax. x0 \squnion f x] iter_down_pfp[of
\lambdax. x0 \squnion f x]
@@ -198,7 +198,7 @@
and bfilter_ivl' is bfilter
and AI_ivl' is AI
and aval_ivl' is aval'
-proof qed (auto simp: iter'_pfp_above)
+proof qed (auto simp: WN_iter'_pfp_above)
value [code] list_up(AI_ivl' test3_ivl Top)
value [code] list_up(AI_ivl' test4_ivl Top)
diff -r f1455859ff03 -r 9e0ea0b5bab5 src/HOL/Library/Code_Integer.thy
--- a/src/HOL/Library/Code_Integer.thy Wed Oct 10 16:01:41 2012 +0200
+++ b/src/HOL/Library/Code_Integer.thy Wed Oct 10 16:02:05 2012 +0200
@@ -31,7 +31,7 @@
done
qed
-lemma (in ring_1) of_int_code:
+lemma (in ring_1) of_int_code':
of_int k = (if k = 0 then 0
else if k 0 then - of_int (- k)
else let
@@ -45,7 +45,7 @@
of_int_add [symmetric]) (simp add: * mult_commute)
qed
-declare of_int_code [code]
+declare of_int_code' [code]
text {*
HOL numeral expressions are mapped to integer literals
diff -r f1455859ff03 -r 9e0ea0b5bab5 src/HOL/Library/Target_Numeral.thy
--- a/src/HOL/Library/Target_Numeral.thyWed Oct 10 16:01:41 2012 +0200
+++ b/src/HOL/Library/Target_Numeral.thyWed Oct 10 16:02:05 2012 +0200
@@ -605,7 +605,7 @@
k l \longleftrightarrow (of_int k :: Target_Numeral.int) of_int l
by (simp add: less_int_def)
-lemma (in ring_1) of_int_code:
+lemma (in ring_1) of_int_code':
of_int k = (if k = 0 then 0
else if k 0 then - of_int (- k)
else let
@@ -619,7 +619,7 @@
of_int_add [symmetric]) (simp add: * mult_commute)
qed
-declare of_int_code [code]
+declare of_int_code' [code]
subsection {* Implementation for @{typ nat} *}
@@ -707,7 +707,7 @@
num_of_nat = Target_Numeral.num_of_int \circ of_nat
by (simp add: fun_eq_iff num_of_int_def of_nat_def)
-lemma (in semiring_1) of_nat_code:
+lemma (in semiring_1) of_nat_code':
of_nat n = (if n = 0 then 0
else let
(m, q) = divmod_nat n 2;
@@ -721,7 +721,7 @@
(simp add: * mult_commute of_nat_mult add_commute)
qed
-declare of_nat_code [code]
+declare of_nat_code' [code]
text {* Conversions between @{typ nat} and @{typ int} *}
diff -r f1455859ff03 -r 9e0ea0b5bab5
src/HOL/Probability/Finite_Product_Measure.thy
--- a/src/HOL/Probability/Finite_Product_Measure.thyWed Oct 10 16:01:41
2012 +0200
+++ b/src/HOL/Probability/Finite_Product_Measure.thyWed Oct 10 16:02:05
2012 +0200
@@ -696,7 +696,7 @@
qed
qed
-sublocale finite_product_sigma_finite \subseteq sigma_finite_measure
Pi\^isubM I M
+sublocale finite_product_sigma_finite \subseteq Pi: sigma_finite_measure
Pi\^isubM I M
using sigma_finite[OF finite_index] .
lemma (in finite_product_sigma_finite) measure_times:
diff -r f1455859ff03 -r 9e0ea0b5bab5 src/HOL/Probability/Probability_Measure.thy
---
Re: [isabelle-dev] Shadowing of theorem names in locales
I recently tried to make HOL-Algebra compliant to this, but unfortunately got stuck in HOL already, where Big_Operators didn't comply either (but that's unlikely the only theory). Yet another unintentional coincidence. If you point we to particular occurences, I am willing to polish them accordingly. If we are serious about forbidding duplicate theorem names eventually we probably need to start by introducing a flag to enable/disable this, so that it doesn't get introduced by accident to theories where duplicate names had already been eliminated. We did similar things in the past and had some success with it. As other have noted before, this is not going to be a one-man effort. It is quite a bit of work, but more importantly, it involves design decisions (namely whether to rename theorems or introduce qualifiers) which is best done by a theory's author. Dito. 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] Shadowing of theorem names in locales
I recently tried to make HOL-Algebra compliant to this, but unfortunately got stuck in HOL already, where Big_Operators didn't comply either (but that's unlikely the only theory). If we are serious about forbidding duplicate theorem names eventually we probably need to start by introducing a flag to enable/disable this, so that it doesn't get introduced by accident to theories where duplicate names had already been eliminated. As other have noted before, this is not going to be a one-man effort. It is quite a bit of work, but more importantly, it involves design decisions (namely whether to rename theorems or introduce qualifiers) which is best done by a theory's author. Clemens Quoting Makarius makar...@sketis.net: On Tue, 9 Oct 2012, Makarius wrote: On Sun, 7 Oct 2012, Florian Haftmann wrote: After some pondering I would argue that this should be forbidden: * (Complete) shadowing is a constant source of confusion. * Global interpretations are impossible then, since they would result in two global theorems with the same name. I've started some experiments with this idea and will report the empirical results soon ... After some detours I am now back on Isabelle/28e37eab4e6f. In principle, the last big reform of locale + interpretation name space prefixes has addressed the situation already, where each locale scope is locally strict, but composing several of them in locale expressions etc. works by mandatory or non-mandatory prefixes. Actual strictness checking is part of the underlying name space policy, when bindings are applied and react with some naming. The local context of the locale construction is particularly important here. It was merely a historical left-over that fact bindings were not checked strictly: (1) in distant past facts were never strict and totally un-authentic (2) the Isar proof body mode allows to override 'notes' as it does for 'fixes'. So with the ch-strict changeset applied to the critical spot of local notes, the namespace policy enforces the concentual locale scopes. Applying this in practice leads to many surprises about situations found in existing theory libraries, though. Some of the changsets leading up to Isabelle/28e37eab4e6f already sort this out. Some other ad-hoc changes are attached as ch-test here. With Isabelle/28e37eab4e6f + ch-strict + ch-test and AFP/77f79b2076f1 the following sessions fail: BDD, Dijkstra_Shortest_Path, Free-Groups, Group-Ring-Module, HOL-Algebra, HOL-Number_Theory, HOL-ex, JinjaThreads, KBPs, Markov_Models, Ordinal, Ordinary_Differential_Equations, Pi_Calculus, Presburger-Automata, PseudoHoops, Psi_Calculi, Refine_Monadic, Simpl, Slicing, Topology, Transitive-Closure-II, Valuation So the question if ch-strict can be activated soon is mainly a matter of library space. It is up to emerging volunteers to sort it out further. (For me it was interesting to see how Isabell/jEdit works on the JinjaThreads monster session. See also AFP/77f79b2076f1 of the result of investing 3GB for poly, 4GB for java, and quite a bit of CPU time and elapsed time.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Shadowing of theorem names in locales
On Thu, 11 Oct 2012, Johannes Hölzl wrote: HOL-Probability (in Isabelle/bb5db3d1d6dd) and Ordinary_Differential_Equations (in AFP/e9fa38f86b76) work now with this patch. A surprising change is found in Markov_Models: We get an error when an assumption has the same name as a fact in the locale: locale loc begin lemma X: True .. lemma assumes X: X shows True ^- raises Duplicate fact declaration local.X vs. local.X Is this easily avoidable? I think this might confuse people and add a maintenance burden when one adds a fact to a locale with a popular name. It is a consequence of handling the local fact name space in a fully authentic way. In the conversions I had done earlier, there were a few situations with duplicate assumptions of a long statement, so I just renamed them apart. Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Shadowing of theorem names in locales
HOL-Probability (in Isabelle/bb5db3d1d6dd) and Ordinary_Differential_Equations (in AFP/e9fa38f86b76) work now with this patch. A surprising change is found in Markov_Models: We get an error when an assumption has the same name as a fact in the locale: locale loc begin lemma X: True .. lemma assumes X: X shows True ^- raises Duplicate fact declaration local.X vs. local.X Is this easily avoidable? I think this might confuse people and add a maintenance burden when one adds a fact to a locale with a popular name. - Johannes Am Mittwoch, den 10.10.2012, 16:51 +0200 schrieb Makarius: On Tue, 9 Oct 2012, Makarius wrote: On Sun, 7 Oct 2012, Florian Haftmann wrote: After some pondering I would argue that this should be forbidden: * (Complete) shadowing is a constant source of confusion. * Global interpretations are impossible then, since they would result in two global theorems with the same name. I've started some experiments with this idea and will report the empirical results soon ... After some detours I am now back on Isabelle/28e37eab4e6f. In principle, the last big reform of locale + interpretation name space prefixes has addressed the situation already, where each locale scope is locally strict, but composing several of them in locale expressions etc. works by mandatory or non-mandatory prefixes. Actual strictness checking is part of the underlying name space policy, when bindings are applied and react with some naming. The local context of the locale construction is particularly important here. It was merely a historical left-over that fact bindings were not checked strictly: (1) in distant past facts were never strict and totally un-authentic (2) the Isar proof body mode allows to override 'notes' as it does for 'fixes'. So with the ch-strict changeset applied to the critical spot of local notes, the namespace policy enforces the concentual locale scopes. Applying this in practice leads to many surprises about situations found in existing theory libraries, though. Some of the changsets leading up to Isabelle/28e37eab4e6f already sort this out. Some other ad-hoc changes are attached as ch-test here. With Isabelle/28e37eab4e6f + ch-strict + ch-test and AFP/77f79b2076f1 the following sessions fail: BDD, Dijkstra_Shortest_Path, Free-Groups, Group-Ring-Module, HOL-Algebra, HOL-Number_Theory, HOL-ex, JinjaThreads, KBPs, Markov_Models, Ordinal, Ordinary_Differential_Equations, Pi_Calculus, Presburger-Automata, PseudoHoops, Psi_Calculi, Refine_Monadic, Simpl, Slicing, Topology, Transitive-Closure-II, Valuation So the question if ch-strict can be activated soon is mainly a matter of library space. It is up to emerging volunteers to sort it out further. (For me it was interesting to see how Isabell/jEdit works on the JinjaThreads monster session. See also AFP/77f79b2076f1 of the result of investing 3GB for poly, 4GB for java, and quite a bit of CPU time and elapsed time.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Shadowing of theorem names in locales
Am Sonntag, den 07.10.2012, 18:06 +0200 schrieb Lars Noschinski: On 07.10.2012 09:37, Florian Haftmann wrote: Hi all, currently, theorem names in locales can be shadowed (given that declarations are in different theories, otherwise the foundation level would reject the declaration since the two foundation theorems would have the same name). After some pondering I would argue that this should be forbidden: * (Complete) shadowing is a constant source of confusion. * Global interpretations are impossible then, since they would result in two global theorems with the same name. Any comments? How would this interact with sublocale? If two (unrelated) locales contain a lemma with the same name, can I still establish a sublocale relation? -- Lars You are forced to give a name to the subplocale interpretation: sublocale L1 NAME!: L2 but then it should work. - Johannes ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Shadowing of theorem names in locales
On 07.10.2012 09:37, Florian Haftmann wrote: Hi all, currently, theorem names in locales can be shadowed (given that declarations are in different theories, otherwise the foundation level would reject the declaration since the two foundation theorems would have the same name). After some pondering I would argue that this should be forbidden: * (Complete) shadowing is a constant source of confusion. * Global interpretations are impossible then, since they would result in two global theorems with the same name. Any comments? How would this interact with sublocale? If two (unrelated) locales contain a lemma with the same name, can I still establish a sublocale relation? -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
