search

SKolodynski / IsarMathLib

IsarMathLib is a library of formalized mathematics for Isabelle/ZF.
https://isarmathlib.org
Other
16 stars 2 forks source link

Add interpretation to the parser #26

Closed dan323 closed 1 year ago

dan323 commented 1 year ago

It will be interesting to add the possibility to interpret locales with the interpretation key word as follows:

definition comp2 ("_{_ O _}") where
  "X{f O g} ≡ Composition(X)`⟨f,g⟩" 

interpretation comp_monoid:monoid0 "X→X" "Composition(X)" "comp2(X)"
  unfolding monoid0_def comp2_def using Group_ZF_2_5_L2(1) by auto
SKolodynski commented 1 year ago

I thought interpretation is supported, but indeed it's not. I will add it. Can you tell me what is the difference between sublocale and interpretation? Both seem to make theorems proven in one locale available in another one.

dan323 commented 1 year ago

Sublocale interprets a locale within another locale; but interpretation instances a locale without another locale in context.

SKolodynski commented 1 year ago

I have added support for interpretation, tested on the above example, please check.

dan323 commented 1 year ago

Seems fine to me

dan323 commented 1 year ago

It was added in commit 147624f44caf8cd8dbfb22812b6392ab34b65456