Re: [isabelle-dev] Problem in the AFP

[Thiemann, Rene]

Dear Peter,

>> It's the operation identification phase of Autoref,
>> quite difficult to debug ... I have not yet looked at it due to
>> ITP-deadline. 
> 
> I found the culprit:
> 
> summary: adapting entries to new Deriving mechanism
> 
> in LTL_to_GBA-theory, this removes a linorder-constraint on
> create_name_igba, which causes the breakdown, because later,
> autoref is only given rules to refine create_name_igba for 
> 'a::linorder, but the respective lemmas do not repeat the
> linorder-constraint. 
> 
> I fixed it by adding the linorder-constraint to the refinement, leaving
> the abstract version general.

sorry, for this problem. I first locally tried to replace the linorder 
class-constraint
by some compare class-constraint, since the new derive-generator produces 
class-constraints
of the form mytype :: (compare,...,compare)compare. However, for lack of time I 
did not manage
to fully adapt your entry from linorder to compare before ITP submission. To 
this end, I 
manually adapted in 88dc498667ff the generation of linear orders in 
LTL_to_GBA_impl. 
Since also other entries prefer the mytype :: (linorder, ..., linorder)linorder 
constraint,
I adding support for it in derive in 470b9d92f174 and then integrate it in 
LTL_to_GBA_impl in
8afc741ecb48, so that the adaptation of LTL_to_GBA_impl in total only was a 
change of a single
line, namely the import statement from the old to the new derive.

However, the problem was that I overlooked in 88dc498667ff that it also 
contained a change in 
LTL_to_GBA which removed the linorder constraint, and which shouldn't have been 
checked in.

Anyway, thanks for fixing the problem,
René
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] [isabelle] Semirings in HOL/Algebra/Ring

[Thiemann, Rene]

Dear all,

can someone please integrate the attached patch which introduces a locale for 
semirings.

I tested the patch by running all sessions of the AFP though without 
ISABELLE_FULL_TEST:
there have been no problems.

Isabelle: db0b87085c16
AFP:  55e04ff27c52

Thanks,
René



>
>> Looks like a good idea to me. Are there any drawbacks?
>
> None of which I'm aware of. I just tested my changes against three 
> AFP-entries which are based on HOL-Algebra
> and they all compile without problems. (Jordan_Hoelder Secondary_Sylow 
> VectorSpace)
>
> However, I really just adapted Ring.thy by adding semiring as intermediate 
> locale. I did not make further
> changes at this point, e.g., by also having commutative semirings, 
> homomorphisms on semirings, etc.



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

[isabelle-dev] Isabelle2016-RC0: potential changes

[Thiemann, Rene]

Dear all,

there are some changes I would like to add for the upcoming release. It would 
be nice, if someone can integrate them:

- improved code equations for binomial coefficients and certain 
divmod-algorithms.

  (cf. 
http://afp.sourceforge.net/browser_info/devel/AFP/Algebraic_Numbers/Improved_Code_Equations.html)

- change type in definition and lemmas about pderiv from real to arbitrary 
fields, or even more general, cf. lines starting with
  (* TODO: inform Isabelle developers *) in 
http://afp.sourceforge.net/browser_info/devel/AFP/Algebraic_Numbers/Square_Free_Factorization.html

- change type of divides_degree from complex to 'a :: idom, cf beginning of
  
http://afp.sourceforge.net/browser_info/devel/AFP/Jordan_Normal_Form/Missing_Polynomial.html

Moreover, everything of

http://afp.sourceforge.net/browser_info/devel/AFP/Jordan_Normal_Form/Missing_*
http://afp.sourceforge.net/browser_info/devel/AFP/Algebraic_Numbers/Missing_*

can freely be moved from the AFP into the distribution, where I ask the 
developers to judge which parts
belong in the distribution and which are too specific, etc.


With best regards,
René
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Isabelle2016-RC0: potential changes

[Thiemann, Rene]

Hi Manuel,

> I already moved a few small lemmas.

Thanks.

> I also defined the notion of an algebraic number; as soon as your AFP entry 
> works with the development version of Isabelle again (is that already the 
> case?),

Yes, it should work. (At least, on Friday afternoon, it worked)

> I will prove equivalence of my definition in Poly_Deriv.thy to your 
> definition in Algebraic_Numbers and adapt the AFP entry accordingly.

I’m puzzled. In ~~/src/HOL/Library/Poly_Deriv.thy I found no notion of 
algebraic number.

> As for the binomial numbers: that looks a bit suboptimal to me.
> I would have expected something like "listprod [k+1..n] div fact (n - k)" 
> plus an additional check if "2*k >= n", reducing "n choose k" to "n choose (n 
> - k)" if appropriate.
> (Not sure what code generation makes of "listprod [k+1..n]", a code_unfold 
> rule to compute this efficiently with an accumulator and without constructing 
> the list explicitly might be required. Same for "fact“.)

Its definitely not optimal, and you’re right that one can improve it by using 
an inline-version of listprod [k+1..n], 
but even the version that is mentioned in 
Algebraic_Numbers/Improved_Code_Equations.html is by far better than the 
current setup, since that just uses the recursive direct definition of 
binomial. (I noticed this since I got timeouts in my experiments with algebraic 
numbers and one of the culprits was binomial!)

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

Re: [isabelle-dev] Isabelle2016-RC0: potential changes

[Thiemann, Rene]

>> I’m puzzled. In ~~/src/HOL/Library/Poly_Deriv.thy I found no notion of 
>> algebraic number.
> Oh, yes, you're right. It's in 
> https://bitbucket.org/isa-afp/afp-devel/src/363fdbc2f28c2503095a245f00db3d2805ed3ff9/thys/Liouville_Numbers/Liouville_Numbers_Misc.thy
>  .

Ah, I see. Indeed: definitely equivalent.

> 
>> Its definitely not optimal, and you’re right that one can improve it by 
>> using an inline-version of listprod [k+1..n], but even the version that is 
>> mentioned in Algebraic_Numbers/Improved_Code_Equations.html is by far better 
>> than the current setup, since that just uses the recursive direct definition 
>> of binomial. (I noticed this since I got timeouts in my experiments with 
>> algebraic numbers and one of the culprits was binomial!)
> 
> I suggest this:
> 
> 
> function fold_atLeastAtMost_nat where
>  [simp del]: "fold_atLeastAtMost_nat f a (b::nat) acc =
> (if a > b then acc else fold_atLeastAtMost_nat f (a+1) b (f a 
> acc))"
> by pat_completeness auto
> termination by (relation "measure (λ(_,a,b,_). Suc b - a)") auto
> ...

Looks good from my viewpoint.

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

Re: [isabelle-dev] Isabelle2016-RC0: potential changes

[Thiemann, Rene]

Hi Manuel,

> I added the efficient code equations for fact and binomial, and similar ones 
> for pochhammer and gbinomial.
> 
> I also adapted everything from Square_Free_Factorization and 
> Missing_Polynomial that seemed to be of general interest to me (especially 
> the generalisation of the type of pderiv).

thanks a lot; in the meantime, I deleted this material from the AFP-entries.

> 
> I also noticed the ring_gcd instance for polynomials. Finalising the changes 
> to the GCD class hierarchy and updating the AFP entries that rely on 
> half-finished versions of this change (such as Echelon_Form) is something 
> that I should probably take care of soon, but definitely not before the 2016 
> release – hopefully before the 2017 one.

The absence of the ring_gcd instance for polynomials is strange from my 
perspective: In Isabelle 2015 we had

  instantiation poly :: (field) gcd

where the gcd-class contained the important properties of a gcd.

In Isabelle 2016-RC0 there also is  

  instantiation poly :: (field) gcd

but now the gcd-class is purely syntactic. Here, to get the same properties of 
a gcd (and more), the corresponding instance would be

  instantiation poly :: (field) semiring_gcd   (or ring_gcd) 

So why should the small proof below be not integrated for the 2016 release? 
Otherwise, there
is no class-based gcd for polynomials available for 2016, in contrast to 2015.

instance poly :: (field) ring_gcd
proof 
  fix a b :: "'a poly"
  show "normalize (gcd a b) = gcd a b" by (simp add: normalize_poly_def 
poly_gcd_monic)
  show "lcm a b = normalize (a * b) div gcd a b" 
  proof (cases "a * b = 0") 
case False
show ?thesis unfolding lcm_poly_def normalize_poly_def
by (subst div_smult_right, insert False, auto simp: div_smult_left)
   (metis coeff_degree_mult divide_divide_eq_left divide_inverse_commute 
inverse_eq_divide)
  next
case True
thus ?thesis by (metis div_0 lcm_poly_def normalize_0)
  qed
qed auto


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

Re: [isabelle-dev] Isabelle2016-RC0: potential changes

[Thiemann, Rene]

Dear all,

> 
> I have already some post-release patches in the pipeline which would add
> this instance anyway.  So, there is no demand for action here at the moment.
> 
> Note that the classes (semi)ring_gcd in Isabelle2015 had no lemmas and
> thus very hardly different from syntactic classes, so there is no loss
> of generality here.

I disagree with this second item: the classes (semi)ring_gcd in Isabelle2015 
have
the three essential lemmas:

gcd_dvd1, gcd_dvd2, and gcd_greatest.

And since you want to include the patch anyway, why not include at least the 
instance now?

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

Re: [isabelle-dev] Isabelle2016-RC0: potential changes

[Thiemann, Rene]

> Am 14.01.2016 um 15:36 schrieb Makarius :
> 
> On Thu, 14 Jan 2016, Florian Haftmann wrote:
> 
 Note that the classes (semi)ring_gcd in Isabelle2015 had no lemmas and
 thus very hardly different from syntactic classes, so there is no loss
 of generality here.
>>> 
>>> I disagree with this second item: the classes (semi)ring_gcd in 
>>> Isabelle2015 have
>>> the three essential lemmas:
>>> 
>>> gcd_dvd1, gcd_dvd2, and gcd_greatest.
>> 
>> indeed, but these are exactly the assumptions of the type class.
>> 
>>> And since you want to include the patch anyway, why not include at least 
>>> the instance now?
>> 
>> It sits on top of a couple of other patches definitely not suitable for
>> inclusion by now.
> 
> Does it mean this thread is closed concerning Isabelle2016?

If Florian has a post-release patch available and wants to insert exactly that 
patch, 
then that’s fine for me. 

Then Isabelle users (including myself) can just load the proposed instance 
declaration from the AFP to
uniformly access the gcd-properties via the semiring-class(-axioms) in Isabelle 
2016.

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

Re: [isabelle-dev] semiring_gcd [was: Isabelle2016-RC0: potential changes]

[Thiemann, Rene]

Dear Florian,

thanks for the info.

Concerning the factorial semiring, we also made some development in that 
direction which we required
for the algebraic numbers. To be more precise, we have an instance of

poly :: (ufd) ufd

where ufd is a unique factorization domain, cf.

http://afp.sourceforge.net/browser_info/current/AFP/Algebraic_Numbers/Unique_Factorization_Domain.html
and
http://afp.sourceforge.net/browser_info/current/AFP/Algebraic_Numbers/Unique_Factorization_Poly.html

Perhaps we should share efforts on this topic (but please after the ITP 
deadline).

Cheers,
René

> Am 18.02.2016 um 17:00 schrieb Florian Haftmann 
> :
> 
> Hi Rene,
> 
> see now fd049b54ad68 for an abstract semiring_gcd with a corresponding
> poly :: (field) semiring_gcd instance.
> 
> Btw. in my pipeline there is an abstract factorial ring with
> 
>   subclass (in factorial_semiring) semiring_gcd
> 
> and hence the possibility to formulate also the other prominent instance
> 
>   poly :: (factorial_semiring) factorial_semiring
> 
> This will still take some time however.
> 
> Cheers,
>   Florian
> 
> Am 15.01.2016 um 12:12 schrieb Thiemann, Rene:
>> 
>>> Am 14.01.2016 um 15:36 schrieb Makarius :
>>> 
>>> On Thu, 14 Jan 2016, Florian Haftmann wrote:
>>> 
>>>>>> Note that the classes (semi)ring_gcd in Isabelle2015 had no lemmas and
>>>>>> thus very hardly different from syntactic classes, so there is no loss
>>>>>> of generality here.
>>>>> 
>>>>> I disagree with this second item: the classes (semi)ring_gcd in 
>>>>> Isabelle2015 have
>>>>> the three essential lemmas:
>>>>> 
>>>>> gcd_dvd1, gcd_dvd2, and gcd_greatest.
>>>> 
>>>> indeed, but these are exactly the assumptions of the type class.
>>>> 
>>>>> And since you want to include the patch anyway, why not include at least 
>>>>> the instance now?
>>>> 
>>>> It sits on top of a couple of other patches definitely not suitable for
>>>> inclusion by now.
>>> 
>>> Does it mean this thread is closed concerning Isabelle2016?
>> 
>> If Florian has a post-release patch available and wants to insert exactly 
>> that patch,
>> then that’s fine for me.
>> 
>> Then Isabelle users (including myself) can just load the proposed instance 
>> declaration from the AFP to
>> uniformly access the gcd-properties via the semiring-class(-axioms) in 
>> Isabelle 2016.
>> 
>> Cheers,
>> René
>> ___
>> isabelle-dev mailing list
>> isabelle-...@in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>> 
> 
> --
> 
> PGP available:
> http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
> 



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

[isabelle-dev] Problem with factorial-ring in combination with containers

[Thiemann, Rene]

Dear all,

in the following theory, the export-code fails:

(Isabelle 957ba35d1338, AFP 618f04bf906f)

theory Problem
  imports 
  "~~/src/HOL/Library/Polynomial_Factorial"
  "$AFP/thys/Containers/Set_Impl"
begin

definition foo :: "'a :: factorial_semiring_gcd ⇒ 'a ⇒ 'a" where
  "foo x y = gcd y x" 
  
definition bar :: "int ⇒ int" where
  "bar x = foo x (x - 1)" 
  
export_code bar in Haskell 
end


The problem arises from two issues:
- factorial_semiring_gcd requires code for 
  Gcd :: “Set ‘a => ‘a”, not only for the binary “gcd :: ‘a => ‘a => ‘a”!
- the code-equation for Gcd is Gcd_eucl_set: "Gcd_eucl (set xs) = foldl 
gcd_eucl 0 xs”
  where “set” is only a constructor if one does not load the container-library.

It would be nice, if one can either alter factorial_semiring_gcd so that it 
does not
require “Gcd” anymore, or if the code-equation is modified in a way that permits
co-existence with containers. (Of course, similarly for Lcm).


With best regards,
Akihisa, Sebastiaan, and René

PS: We currently solve the problem by disabling Gcd and Lcm as follows:

lemma [code]: "(Gcd_eucl :: rat set ⇒ rat) = Code.abort (STR ''no Gcd on 
sets'') (λ _. Gcd_eucl)"  by simp
lemma [code]: "(Lcm_eucl :: rat set ⇒ rat) = Code.abort (STR ''no Lcm on 
sets'') (λ _. Lcm_eucl)"  by simp
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Theory for discrete log etc.

[Thiemann, Rene]

Dear all,

thanks Manuel and Florian for pointing to other variants of discrete 
logarithms. 

I would like to mention a fairly recent one in
AFP/Sqrt_Babylonian/Log_Impl.thy.

It defines log_floor and log_ceiling :: “int => int => nat”.

The advantage of these functions are improved code equations which
work like repeated squaring for exponentiation algorithms. 

The efficiency has been crucial when computing logarithms of numbers x with 
more than 100,000 digits, i.e., where log2 x >= 300,000.
(These numbers arose during the factorization of large integer polynomials.)

Cheers,
René


> Am 13.08.2016 um 17:02 schrieb Manuel Eberl :
> 
> There's also natlog2 in src/HOL/Analysis/Summation_Tests.thy, which I 
> introduced because I didn't know about the other ones.
> 
> Manuel
> 
> 
> On 13/08/16 15:09, Florian Haftmann wrote:
>> Hi all,
>> 
>> after studying 28d1deca302e I realized that we have now two theories
>> dealing with discrete functions (with one having been hidden in
>> Float.thy for years):
>> 
>>  Log_Nat.floorlog :: "nat ⇒ nat ⇒ nat"
>>  Discrete.log :: "nat ⇒ nat"
>>  Log_Nat.bitlen :: "int ⇒ int"
>>  Discrete.sqrt :: "nat ⇒ nat"
>> 
>> »Discrete.log« seems to be »Log_Nat.floorlog 2« and »Log_Nat.bitlen« is
>> just a variant with different types.
>> 
>> Just to place a memo for future consolidation.
>> 
>> Cheers,
>>  Florian
>> 
>> 
>> 
>> ___
>> 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

Re: [isabelle-dev] Efficient code for Discrete.log

[Thiemann, Rene]

Hi Manual,

thanks for your efforts, but I believe there is already a more efficient way to 
compute log2.

In your implementation, consider your intlog2_aux which roughly requires y 
iterations if log2(x) = y,
since you always just add 1 to the accumulator.

For some of my applications this implementation is not efficient enough, 
which was the reason to develop Sqrt_Babylonian/Log_Impl.thy,
which is much faster since it only needs log2(y) iterations: 
in log_main the accumulator is roughly doubled in every iteration.

To test, try to compute "log_2 (3 ^ n)” for some reasonably large n.

Cheers,
René

PS: Unfortunately, Sqrt_Babylonian.log_floor and log_ceiling are not connected 
to Discrete.log.

> Am 29.06.2017 um 15:29 schrieb Manuel Eberl :
> 
> Hallo,
> 
> I'm considering adding efficient code for Discrete.log (the dual logarithm on 
> natural numbers). PolyML does provide an IntInf.log2 function that seems 
> reasonably efficient so that one can set up code printing. However, I am 
> struggling with one detail:
> 
> Where would the code that does this actually reside? I cannot really put it 
> into Discrete.thy, because then that would have to import 
> Code_Target_Numeral. I could put it into Code_Target_Integer.thy, but then 
> that would have to import Discrete, which does not sound right to me either.
> 
> I attached what I have so far.
> 
> Manuel
> 
> ___
> 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] Towards the Isabelle2017 release

[Thiemann, Rene]

Dear all,

let me share my opinions after porting IsaFoR to yesterdays development version:

- In total the transition from our 2016-1 source went quite smooth 
  (~ 14 hours for whole of IsaFoR)

- Most changes have been caused by integrating session-qualified theory imports.
  This will also require a reform of the splitting of sessions, which previously
  was structured towards a fast build-process, but now should be structured 
more 
  towards logical structure (which is currently reflected in the 
directory-structure).

- In the NEWS I read about freeing short constant names like the
  “Renamed ii to imaginary_unit in order to free up ii as a variable”.
  I definitely support this kind of change, but at the same time found
  quite the opposite in HOL-Algebra:
  If one imports HOL-Algebra.Multiplicative_Group (which we actually do
  via some transitive import), then \mu (LFP), \nu (GFP) and 
  \phi (Euler’s totient function) become constants.
  This was a bit annoying.

- There have been some changes w.r.t. code-generation which now lead
  to runtime exception in the generated code. For instance, now
  I get code like
  “f x = Code.abort …” 
  whereas in 2016-1 there was a proper code like
  “f x = some ordinary right-hand side” 
  We did not yet isolate the problem and will report later.

Cheers,
René  


> Am 21.08.2017 um 20:24 schrieb Makarius :
> 
> Dear Isabelle contributors,
> 
> we are now definitely heading towards the Isabelle2017 release.
> 
> The first official release candidate Isabelle2017-RC1 is anticipated for
> 2/3-Sep-2017, that is a bit less than 2 weeks from now.
> 
> That is also the deadline for any significant additions.
> 
> 
> I have already updated the important files NEWS, CONTRIBUTORS, ANNOUNCE
> in Isabelle/5c0a3f63057d, but it seems that many potential entries are
> still missing.
> 
> Please provide entries in NEWS and CONTRIBUTORS for all relevant things
> you have done since the last release.
> 
> 
>   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] Towards the Isabelle2017 release

[Thiemann, Rene]

Dear Florian,

>> - There have been some changes w.r.t. code-generation which now lead
>>  to runtime exception in the generated code. For instance, now
>>  I get code like
>>  “f x = Code.abort …”
>>  whereas in 2016-1 there was a proper code like
>>  “f x = some ordinary right-hand side”
>>  We did not yet isolate the problem and will report later.
> 
> OK, I will dig into this after you have isolated it.  Might be well that
> this only occurs on certain theory merges.

The problem seems to be a change wrt. locale interpretations.

Consider the following code:

=
locale foo = fixes f :: "nat => nat"
  assumes f_mono[termination_simp]: "f x <= x"
begin

fun bar :: "nat => nat" where
  "bar 0 = 0"
| "bar (Suc x) = Suc (bar (f x))"

end

definition com where
  [code del]: "com = foo.bar id"

interpretation foo id
  rewrites "foo.bar id = com"
  unfolding com_def by (unfold_locales, auto)

lemma "com 5 = 5" by eval
export_code com in Haskell
=


This works perfectly fine in Isabelle 2016-1, and especially
the [code del] is required to make the final export_code and eval succeed.

In contrast, in a recent development version, the [code del] still is accepted,
but the export_code will deliver “com _ = error …” and the “eval” will fail.

The solution is easy: remove the previously required [code del].

Cheers,
René


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

Re: [isabelle-dev] Towards the Isabelle2017 release

[Thiemann, Rene]

Dear Florian,

thanks for the explanation and the hint on style.

The below pattern works perfectly in our formalization.

Cheers,
René

> Am 31.08.2017 um 14:03 schrieb Florian Haftmann 
> :
> 
> Note that the pattern above is avoided nowadays by an interpretation
> with mixin definitions:
> 
> locale foo = fixes f :: "nat => nat"
>  assumes ...
> begin
> 
> fun bar :: "nat => nat” where ...
> 
> end
> 
> global_interpretation foo id
>  defines com = bar
>  by standard simp

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

Re: [isabelle-dev] Fwd: [isabelle] Matrix-Vector operation

[Thiemann, Rene]

Dear all,

with HMA_Connect you have a bidirectional connection between “‘a^’n’^m” and “‘a 
mat”.
However, when you transfer something from “‘a^’n^’m” to “‘a mat”, then you get 
the additional
constraint that the dimensions of the matrix must be non-zero.

To be more precise, assume the following two lemmas (where I omit 
sort-constraints):

lemma one: 
  fixes A B :: “‘a^’n^’m”
  shows “A + B = B + A” 

lemma two: 
  fixes A B :: “‘a mat”
  shows “A : carrier_mat n m ==> B : carrier_mat n m ==> A + B = B + A” 

From “two” and HMA_Connect you can easily get “one”.
But from “one” and HMA_Connect you only get “three” via transfer:  

lemma three: 
  fixes A B :: “‘a mat”
  shows “n ~= 0 ==> m ~= 0 ==> A : carrier_mat n m ==> B : carrier_mat n m ==> 
A + B = B + A” 

To obtain “two” from “three", one would have to manually proof the result for 
the corner cases “n = 0 \/ m = 0”.


But indeed, Fabian is completely right that lemmas for determinants, etc. are 
duplicates. Actually, the JNF-matrices “‘a mat” 
have been developed from scratch (without HMA_Connect), by manually copying and 
adapting several proofs from the distribution.

Cheers,
René

> Am 26.02.2018 um 18:28 schrieb Fabian Immler :
> 
> 
>> Am 26.02.2018 um 16:12 schrieb Lawrence Paulson :
>> 
>> I was at the meeting in Logroño and my impression was that we had to live 
>> with these different formalisations. There was no way to unify them and the 
>> best one could hope to transfer certain results from one formalisation to 
>> another using local types in some incredibly complicated way.
> HMA_Connect shows a way to unify (at least parts of) them: it makes explicit 
> that 'a^'n^'m can be seen as a subtype of 'a mat.
> 
> This makes it possible to avoid duplications: for example, results about 
> eigenvalues are only proved once for 'a mat and are transferred to the 
> "subtype" 'a^'n^'m.
> In contrast to that, we do have duplicate developments for determinants, 
> multiplication etc. in isabelle and the AFP. We should be able to get rid of 
> those.
> 
> Ideally, one would do the developments for 'a^'n^'m, but I am not sure how 
> well theorems can be transferred in that direction...
> 
> Fabian
> 
> 
>> If there really is a common basis for formalising linear algebra than I 
>> would be thrilled to see it, and I'm sure we could figure out a way to 
>> implement this.
>> 
>> Larry
>> 
>>> On 26 Feb 2018, at 14:57, Fabian Immler >> > wrote:
>>> 
>>> We do have the problem that AFP/Jordan_Normal_Form/Matrix and 
>>> Analysis/Finite_Cartesian_Product both formalize vectors and matrices and 
>>> that there are formalizations of (aspects of) linear algebra for both of 
>>> them. Last year in Logrono, there was the proposal to put all linear 
>>> algebra on the common foundation of a locale for modules, but apparently 
>>> nobody has found the time and motivation to push this much further.
>>> 
>>> Perhaps a more humble first step towards unifying the existing theories 
>>> would be to move AFP/Jordan_Normal_Form/Matrix to the distribution and do 
>>> the construction of Finite_Cartesian_Product.vec as a subtype of Matrix.vec.
>>> 
>>> Any opinions on that?
>> 
> 
> ___
> 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