Email Gateway (Aug 22 2022 at 12:40): Email Gateway (Aug 22 2022 at 12:40):From: Jonathan Woodgate via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hello,
I have a simple question: Let
f :: N => Nf k = {n:N. predicate(k) }
typedef T1 = "f 1"
typedef T2 = "f 2"
...
instance T1::cpo //assume the predicate is such that they are indeed cpo'sinstance T2::cpo
...
So for 100 type definitions i have to prove the instantiation 100 times by hand.
My question is, how can I automatize this, by defining a lemma as follows:
lemma " ∀T. OFCLASS(f T, pcpo_class) "
PS: I know that this is syntactically wrong, since f T is a set and it should instead be a type.
Thank You!
Email Gateway (Aug 22 2022 at 12:40):From: Jonathan Woodgate via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hello,
small correction:
f :: nat => nat set where
f k = {n:N. predicate(k) }
typedef T1 = "f 1"
typedef T2 = "f 2"
...
instance T1::cpo //assume the predicate is such that they are indeed cpo'sinstance T2::cpo
...
So for 100 type definitions i have to prove the instantiation 100 times by hand.
My question is, how can I automatize this, by defining a lemma as follows:
lemma " ∀T. OFCLASS(f T, cpo_class) "
Thank you very much! Jonathan Woodgate via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk> schrieb am 18:16 Mittwoch, 17.Februar 2016:
Hello,
I have a simple question: Let
f :: N => Nf k = {n:N. predicate(k) }
typedef T1 = "f 1"
typedef T2 = "f 2"
...
instance T1::cpo //assume the predicate is such that they are indeed cpo'sinstance T2::cpo
...
So for 100 type definitions i have to prove the instantiation 100 times by hand.
My question is, how can I automatize this, by defining a lemma as follows:
lemma " ∀T. OFCLASS(f T, pcpo_class) "
PS: I know that this is syntactically wrong, since f T is a set and it should instead be a type.
Thank You!
Email Gateway (Aug 22 2022 at 12:40):From: Johannes Hölzl <hoelzl@in.tum.de>
You can use the usual trick to use the cardinality of a type parameter:
typedef 'a T = "f (card (UNIV :: 'a set))"
Then you can use the Numeral_Type library to write:
1 T, 2 T, ...
Last updated: Apr 25 2024 at 20:15 UTC