Hi Ramana, Thanks for explanation and hints. Now it’s clear to me that, I *must* remove the new_axiom() from the project, even if this means I have to bring some “ugly” solutions.
Now I see ord_RECURSION is a universal tool for defining recursive functions on
ordinals, for this part I have no doubts any more. But my datatype is discrete,
no order, no accumulation, currently I can’t see a function (lf :’a ordinal ->
‘b set -> ‘b) which can be supplied to ord_RECURSION ..
Currently I’m trying to something else in the datatype, and I have to replay
all theorems in the project to see the side effects. Meanwhile I would like to
hear from other HOL users for possible solutions on the infinite sum problem
which looks quite a common need ..
Regards,
Chun
> Il giorno 13 lug 2017, alle ore 14:35, Ramana Kumar
> <ramana.ku...@cl.cam.ac.uk> ha scritto:
>
> Some very quick answers. Others will probably go into more detail.
>
> 1. If you use new_axiom, it becomes your responsibility to ensure that your
> axiom is consistent. If it is not consistent, the principle of explosion
> makes any subsequent formalisation vacuous. (If you don't use new_axiom, it
> can be shown that any formalisation is consistent as long as set theory is
> consistent.)
>
> 2. Yes. But you should probably detail why you claim that the axiom is
> consistent and that you wrote it down correctly. It also makes it less
> appealing for others to build on your work subsequently.
>
> 3. Yes. Prove the existence of functions defined on ordinals, specialise that
> existence theorem with your desired definition, then use new_specification.
> Maybe the required theorem exists already? Does ord_RECURSION do it? See how
> ordADD is defined. (I haven't looked at this in detail.)
>
> On 13 July 2017 at 21:10, Chun Tian (binghe) <binghe.l...@gmail.com> wrote:
> Hi,
>
> (Thank you for your patience for reading this long mail with the question at
> the end)
>
> Recently I kept working on the formal proof of an important (and elegant)
> theorem in CCS, in which the proof requires the construction of a recursive
> function defined on ordinals (returning infinite sums of CCS processes). Here
> is the informal definition:
>
> 1. Klop a 0o := nil
> 2. Klop a (ordSUC n) := Klop a n + (prefix a (Klop a n))
> 3. islimit n ==>
> Klop a n := SUM (Klop a m) for all ordinals m < n
>
> (here the "+" operator is overloaded, it's the "sum" of an custom datatype
> (CCS) defined by HOL's Define command. "prefix" is another operator, both are
> 2-ary)
>
> I think it's a well-defined function, because the ordinal arguments strictly
> becomes smaller in each recursive call. But I don't know how to formall prove
> it, and of course HOL's Define package doesn't support ordinals at all.
>
> On the other side, my datatype doesn't support infinite sums at all, and it
> seems no hope for me to successfully defined it, after Michael has replied my
> easier email and explained the cardinality issues for such nested types.
>
> So I got two issues here: 1) no way to define infinite sums, 2) no way to
> define resursive functions on ordinals. But I found a "solution" to bypass
> both issues: instead of trying to express infinite sums, I turn to focus on
> the behavior of the infinite sums and define the behavior directly as an
> axiom. In CCS, if a process p transits to p', then p + q + ... (infinite
> other process) still transit to p'. Thus I wrote the following "cases"
> theorem (which looks quite like the 3rd return values by Hol_reln) talking
> about a new constant "Klop"
>
> val _ = new_constant ("Klop", ``:'b Label -> 'c ordinal -> ('a, 'b) CCS``);
>
> |- (!a. Klop a 0o = nil) ∧
> (!a n u E.
> Klop a n⁺ --u-> E <==>
> u = label a ∧ E = Klop a n ∨ Klop a n --u-> E) ∧
> !a n u E.
> islimit n ==> (Klop a n --u-> E <==> !m. m < n ∧ Klop a m --u-> E)
>
> I used new_axiom() to make above definion accepted by HOL. I don't know how
> to "prove" it, don't even know what to prove, because it's just a definition
> on a new logical constant (acts as a black-box function), while it's
> behaviour is exactly the same as if I have infinite sums in my datatype and
> HOL has the ability to define recursive function on ordinals.
>
> From now on, I need no other axioms at all. Then I can prove the following
> "rules" theorems which looks like the first return value of Hol_reln:
>
> |- (!a n. Klop a n⁺ --label a-> Klop a n) ∧
> !a n m u E. islimit n ∧ m < n ∧ Klop a m --u-> E ==> Klop a n --u-> E
>
> Then I can use transfinite inductino to prove a lot of other properties of
> the function ``Klop a``. And with a lot of work, finally I have proved the
> following elegant theorem in Concurrent Theory:
>
> Thm. (Coarsest congruence contained in weak equivalence)
> |- !g h. g ≈ʳ h <==> !r. g + r ≈ h + r
>
> ("≈ʳ" is observation congruence, or rooted weak bisimulation equivalence. "≈"
> is weak bisimulation equivalence)
>
> Every lemma or proof step corresponds to the original paper [1] with
> improvements or simplification. And if you let me to write down the informal
> proof (from the formal proof) using strict Math notations and theorems from
> related theories, I have full confidence to convince people that it's a
> correct proof.
>
> But I do have used new_axiom() in my proof script. My questions:
>
> 1. What's the risk for a new_axiom() used on a new constant to break the
> consistency of entire HOL Logic?
> 2. With new_axiom() used, can I still claim that, I have correctly formalized
> the proof of that theorem?
> 3. (optionall) is there any hope to prevent using new_axiom() in my case?
>
> Best regards,
>
> Chun Tian
>
> [1] van Glabbeek, Rob J. "A characterisation of weak bisimulation
> congruence." Lecture notes in computer science 3838 (2005): 26.
>
> --
> Chun Tian (binghe)
> University of Bologna (Italy)
>
>
> ------------------------------------------------------------------------------
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
signature.asc
Description: Message signed with OpenPGP using GPGMail
------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
