I just repaired Akra_Bazzi.
In the process of doing so, I noticed two things:
1. Due to the new definition of ‘real’, the theorem Real.of_nat_nat,
which is stated as ‘0 ≤ x ⟹ real (nat x) = real x’ now essentially means
‘0 ≤ x ⟹ real (nat (int x)) = real x’, which is rather silly.
Moreover, Real.of_nat_nat shadows Int.ring_1_class.of_nat_nat, which
even implies Real.of_nat_nat. I therefore suggest we just remove
Real.of_nat_nat completely.
2. Goals like ‘real (floor x) ≤ x’ used to be solvable by ‘simp’,
whereas the now equivalent ‘of_int (floor x) ≤ x’ is not. (I don't know
if simp used to do that with a simp rule or a solver)
It would probably nice to have ‘simp’ do this sort of thing again, but
in all instances that I encountered, ‘linarith’ did the trick as well.
I'm a bit busy right now, but I am, in general, willing to help out with
fixing the AFP. Which entries would you want me to look at?
Cheers,
Manuel
On 11/11/15 22:09, Johannes Hölzl wrote:
It looks like the setup for blast changed, in the following entries is a
non-terminating blast call. They do not seam to be related to the change
at all:
Graph_Theory
ShortestPath
Rank_Nullity_Theorem
Echelon_Form
Gauss_Jordan
Interestingly in
Jordan_Normal_Form
QR_Decomposition
a real :: 'a => real is required! Both introduce a type class with
group/vector-space homomorphism.
I did _not_ look yet into:
JinjaThreads
Ordinary_Differential_Equations
Affine_Arithmetic
Akra_Bazzi
- Johannes
Am Mittwoch, den 11.11.2015, 18:29 +0100 schrieb Johannes Hölzl:
Okay, I look at the AFP entries.
I assume Affine_Arithmetic is just slow, but I can ask Fabian tomorrow
if this is unusual.
- Johannes
Am Mittwoch, den 11.11.2015, 17:19 +0000 schrieb Lawrence Paulson:
It would be great if you could help. I have just committed some
corrections to a number of AFP theories, including that one I think.
Affine_Arithmetic comes with some examples that run extremely slowly;
I’m not sure whether there is a problem or whether it is always like
that. If you want to take over with those, I can do some more tidying
up with the main libraries.
Larry
On 11 Nov 2015, at 17:17, Johannes Hölzl <hoe...@in.tum.de> wrote:
Hi Larry,
this is a huge change and after I adapted Markov_Models I see that it
simplifies some proofs.
If you want I can adapt all AFP entries for which I'm the maintainer, or
which are related to Probability theory:
Density_Compiler
Integration
Lower_Semicontinuous
Markov_Models
Ordinary_Differential_Equations
Possibilistic_Noninterference
Probabilistic_Noninterference
UpDown_Scheme
Girth_Chromatic
Probabilistic_System_Zoo
Random_Graph_Subgraph_Threshold
pGCL
Just tell me which of these you are already working on, so we can merge
without conflicts.
- Johannes
Am Mittwoch, den 11.11.2015, 12:28 +0000 schrieb Lawrence Paulson:
I’m glad to have your support. It’s just possible that I might ask your help in
getting some things working in the AFP.
Larry
On 10 Nov 2015, at 17:53, Manuel Eberl <ebe...@in.tum.de> wrote:
This is very nice to hear. ‘real’ has plagued me for some time now and I am
glad to see it gone.
Thanks for the good work!
On 10/11/15 17:45, Lawrence Paulson wrote:
The first phase of this project is finished: the function “real” now has the
monomorphic type nat => real and is simply an abbreviation for the generic
function, of_nat. In addition, the function “real_of_int” abbreviates the generic
function of_int.
It took about a week to convert all the theories in the main Isabelle/HOL
directory. Most of them needed little or no attention, the big exceptions being
Probability (which frequently used “real” with the type ereal => real) and
Decision_Procs, which contained many thousands of instances of “real” on integers
and floats.
The main priority at the moment is to fix the decision procedure mir, which
isn’t working but appears to be entirely unused. Then there is still a lot of
cleaning up to do, especially in Real.thy and its ancestors. Two or three dozen
theorems existed in duplicate forms, with versions for “real” separate from
versions for the other coercions; occasionally these variants were named
systematically, but often their names were unrelated from the originals, and
the names of variables in the theorems were almost always different. The
simplification status of the two variants generally differed as well. Thus the
behaviour of the simplifier on a formula depended on which coercion had been
used, and in 150 cases, the simplification itself included the mapping of one
coercion to another (there were two equivalent theorems for doing this).
Innumerable type constraints have now become redundant (things such as
real_of_int (i::int)), but I intend to leave them as they are. I have a lot of
AFP entries to fix.
Larry
_______________________________________________
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
_______________________________________________
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
