Julin Shaji (Feb 11 2025 at 06:58): Julin Shaji (Feb 11 2025 at 06:58):Hi.
I was looking at this page:
https://isabelle.in.tum.de/library/HOL/HOL-Matrix_LP/Matrix.html
What does the nat ⇒ nat ⇒ 'a::zero in the following lines mean?
definition nonzero_positions :: "(nat ⇒ nat ⇒ 'a::zero) ⇒ (nat × nat) set" where
"nonzero_positions A = {pos. A (fst pos) (snd pos) ~= 0}"
It looks like the type of a function that accepts two nat and then returns a list?
But maybe :: doesn't mean cons of list? I suppose that's #?
zero is like the identity element of a group?
https://isabelle.in.tum.de/library/HOL/HOL/Groups.html#Groups.zero|class
I'm new to isabelle but am familiar with sml.
Jan van Brügge (Feb 11 2025 at 10:44):That is a kind type class constraint. It means that 'a must have an instance of the class zero.
John Hughes (Feb 11 2025 at 16:17):Learning that "::" doesn't mean "cons" is a tough battle for those who (like me) come from ML. I feel your pain, Julin. :)
I also had no idea that it had this additional "type class constraint" meaning.
Julin Shaji (Feb 12 2025 at 04:27):Jan van Brügge said:
That is a kind type class constraint. It means that
'amust have an instance of the classzero.
Ah.. So (nat ⇒ nat ⇒ 'a::zero) ⇒ (nat × nat) set is like Zero a => (nat -> nat -> a) -> Set (nat, nat) in Haskell, I guess.
Jan van Brügge (Feb 12 2025 at 09:16):precisely
Julin Shaji (Feb 12 2025 at 09:26):Also, what does pos in {pos. A (fst pos) (snd pos) ~= 0} mean?
~= means not-equal, right?
Julin Shaji (Feb 12 2025 at 09:26):Is it like an anonymous function?
Jan van Brügge (Feb 12 2025 at 10:29):similar, it is syntax sugar for Collect (λpos. A (fst pos) (snd pos) ~= 0), which denotes the set of all pos such that A (fst pos) (snd pos) ~= 0
Julin Shaji (Feb 13 2025 at 06:06):Thanks.
I suppose Collect is this one:
https://isabelle.in.tum.de/library/HOL/HOL/Set.html#Set.Collect|const
Jan van Brügge (Feb 13 2025 at 09:59):yes
Julin Shaji (Feb 17 2025 at 13:02):In the definition of Collect:
axiomatization Collect :: "('a ⇒ bool) ⇒ 'a set" ― ‹comprehension›
and member :: "'a ⇒ 'a set ⇒ bool" ― ‹membership›
where mem_Collect_eq [iff, code_unfold]: "member a (Collect P) = P a"
and Collect_mem_eq [simp]: "Collect (λx. member x A) = A"
what does the part within square brackets mean?
Like [iff, code_unfold] in mem_Collect_eq [iff, code_unfold].
Christian Pardillo Laursen (Feb 17 2025 at 13:49):It gives the theorem attributes to the theorems, which transforms them in some way or makes them accessible to automation tools. So, for example, [simp] will mean that simp will use that theorem as a simplification rule, and code_unfold (I think) means that the rule is available during code generation
Christian Pardillo Laursen (Feb 17 2025 at 13:49):https://isabelle.systems/conventions/theorem_attributes.html
Last updated: Mar 09 2025 at 12:28 UTC