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
