Sorry, in previous mails I have wrongly copied the KLOP theorems for finite version. Below is the correct theorems for infinite version:
[Klop_0] Theorem
|- ∀a. Klop a 0 = ABS_graph ({0},∅)
[Klop_PROP0] Theorem
|- ∀a n N. n ≤ N ⇒ STABLE (lts n (Klop a N))
[Klop_PROP1] Theorem
|- ∀a n E N.
n ≤ N ⇒
(lts n (Klop a N) --label a--> E ⇔
∃m. m < n ∧ (E = lts m (Klop a N)))
[Klop_PROP2] Theorem
|- ∀a n m N. m < n ∧ n ≤ N ⇒ ¬(lts m (Klop a N) ∼ lts n (Klop a N))
[Klop_PROP2'] Theorem
|- ∀a n m N. m < n ∧ n ≤ N ⇒ ¬(lts m (Klop a N) ≈ lts n (Klop a N))
And all my proof scripts can be found at [1]. These’re new developments,
they’re not in HOL’s example/CCS folder.
[1] https://github.com/binghe/informatica-public/tree/master/thesis
> Il giorno 12 ott 2017, alle ore 11:51, Chun Tian <binghe.l...@gmail.com> ha
> scritto:
>
> Hi,
>
> This mail is long, it’s very important for me, and it's a continuation of my
> previous two big questions in 3 months ago, titled "On the use of new_axiom()
> in formal projects” and "How to define "infinite sums" of custom datatypes?”.
>
> The good thing is, I have resolved the previous difficulties in expressing
> infinite sums in process algebra, and have prevented using an axiom. I
> didn’t use the paper of Dr. Andrei Popescu, simply because it’s too hard for
> my current skills. I also didn’t use the idea from Michael Norrish, by
> introducing another larger Datatype:
>
> Datatype`CCS = … existing def … (* with or without finite/binary sums *)`
> Datatype`bigCCS = SUM (num -> CCS)`
>
> Because the "infinite sum” in my problem happens at infinite levels, but this
> “bigCCS” cannot further include itself.
>
> My solution is to embed LTS (labeled transition system) into CCS datatype:
>
> val _ = type_abbrev ("LTS", ``:('a ordinal, 'b Action) graph``);
>
> (* Define the type of (pure) CCS agent expressions. *)
> val _ = Datatype `CCS = nil
> | var 'a
> | prefix ('b Action) CCS
> | sum CCS CCS
> | par CCS CCS
> | restr (('b Label) set) CCS
> | relab CCS ('b Relabeling)
> | rec 'a CCS
> | lts ('a ordinal) (('a, 'b) LTS)`;
>
> here the type “:(‘a, ‘b) graph” is my creation in response of providing a
> general graph theory formalization [1], ‘a is the type of vertex, ‘b is the
> type of edge label. Currently it’s far from complete, with lots of possibly
> wrong definitions but no much supporting theorems. But it worked for my
> current needs. For my problem described in this mail, the structure of this
> graph doesn’t matter, you can safely think it’s a set (defined by
> pred_setTheory) with 'a ordinals as vertices.
>
> The “lts” constructor in above CCS datatype is my creation without knowing
> any similar work. the term ``lts r G`` means a rooted LTS, where “r” is a
> vertex in the graph G, as the root node. For this new constructor, I have
> defined a single transition rule:
>
> val (TRANS_rules, TRANS_ind, TRANS_cases) = Hol_reln `
> (!E u. TRANS (prefix u E) u E) /\
> (* PREFIX *)
> (!E u E1 E'. TRANS E u E1 ==> TRANS (sum E E') u E1) /\ (* SUM1
> *)
> (!E u E1 E'. TRANS E u E1 ==> TRANS (sum E' E) u E1) /\ (* SUM2
> *)
> ...
> (!E u E' G. (E, u, E') IN (TS G)
> ==> TRANS (lts E G) u (lts E' G)) `; (* LTS
> *)
>
> That is, TRANS (lts E G) u (lts E' G) is true if and only if there is a
> labeled edge E—u—>E’ in the graph G. The most surprising fact is, after
> introducing such a new constructor “lts” and its transition rule, all my
> previous proved theorems are still working. The only changes I have to do,
> is very few theorems in which the TRANS_cases theorem is used, but the
> additional sub-goal is trivial.
>
> So, all my definitions like Bisimulation, Weak bisimulation, etc. now also
> work in pure transition systems (as rooted directed graphs). I feel so happy
> for having LTS included in my formalization of CCS and prevented for
> re-defining almost everything again. And the mixing of LTS and CCS is now
> also meaningful: two graphs can be connected directly by algebraic
> operators, and the combined transition characteristics still make perfect
> sense.
>
> Now I have the following so-called Klop process, which is actually an set of
> “Arbitrary many non-bisimiar process”:
>
> Klop l n =
> ABS_graph ({m | m ≤ n},{{p} --label l--> {q} | p ≤ n ∧ q < p}):
>
> without any new axiom, now I can prove the following properties:
>
> [KLOP_PROP0] Theorem (all these processes are stable, i.e. has no
> tau-transition)
>
> |- ∀a n. STABLE (KLOP a n)
>
> [KLOP_PROP1] Theorem (any transition from such a process, leads to a
> smaller process by the same generator)
>
> |- ∀a n E. KLOP a n --label a--> E ⇔ ∃m. m < n ∧ (E = KLOP a m)
>
> [KLOP_PROP1'] Theorem (the same as above, but for weak transition, which
> is actually strong transition because there’s no tau at all)
>
> |- ∀a n E. KLOP a n ==label a=-> E ⇔ ∃m. m < n ∧ (E = KLOP a m)
>
> [KLOP_PROP2] Theorem (two different sized such processes are not strong
> bisimilar)
>
> |- ∀a n m. m < n ⇒ ¬(KLOP a m ∼ KLOP a n)
>
> [KLOP_PROP2'] Theorem (two different sized such processes are also not
> weak bisimilar)
>
> |- ∀a n m. m < n ⇒ ¬(KLOP a m ≈ KLOP a n)
>
> Again, I feel so happy for successfully proved and defined above function and
> its properties. Now it remains to use it for proving the ultimate “simple”
> theorem above process algebra:
>
> ``!p q. OBS_CONGR p q = !r. WEAK_EQUIV (sum p r) (sum q r)`` (observation
> congruence is the coarsest congruence contained in weak bisimulation)
>
> Now it’s touching my question and two difficulties:
>
> The proof of above theorem has been reduced to: finding a special process K,
> which is not (weak) bisimilar with any node in the transition graph of two
> given processes p and q. The informal proof [2] is like this:
>
> “Let c be the smallest infinite cardinal, such that NODES(p) and
> NODES(q) has less than c nodes. So there are less than c processes in
> NODES(p) and NODES(q). Then there’s a tau-free process K with NODES(K) < c,
> such that k is not bisimiar with any nodes in NODES(p) and NODES(q),
> BECAUSE: for each infinite cardinal c there are c ordinals smaller than c.”
>
> If I've learnt correctly, in standard set theory, all cardinals are ordinals,
> but the reverse is not true, because not every ordinals “has the same number
> (as itself) of smaller ordinals”. But in HOL’s currently formalization,
> cardinalTheory is depended by ordinalTheory, and ordinalTheory didn’t define
> “cardinal numbers” at all. Whenever an informal proof says "Let xxx be the
> smallest infinite cardinal, such that …”, I don’t know how to formalize it at
> all, because there’s no concept of “cardinal (number)” that I can use.
>
> Further more, my Klop function has the type: ‘a ordinal -> (‘a, ‘b) CCS.
> I have no way to change the first type variable to ‘c so that it’s
> independent with type variables used in CCS, because ordinal numbers were
> actually written as part of the CCS processes (as vertices in the lts graph).
> But this means I have no way to use my previous proved theorem:
>
> [ONE_ONE_IMP_NOTIN] Theorem
>
> |- ∀A f. ONE_ONE f ⇒ ∃n. f n ∉ A
>
> which is based on “univ_ord_greater_cardinal” in ordinalTheory. Because the
> type unification will fail: for any set of type ``(:’a, ‘b) CCS -> bool``, I
> have no way to say there’s always a bigger ‘a ordinal, which is “larger” than
> the “cardinality” of the set. Also please noticed that, now my CCS is at
> least as large as the “set" of all ‘a ordinals, because I do can inject each
> single ordinals into a CCS process, i.e. my Klop function defined above.
>
> I hope I’ve explained well for my two questions, let me summarize them again:
>
> 1. How to express the cardinality of a set as “cardinal numbers” in HOL?
> 2. How to find a larger ordinal for a set of custom-defined datatype, when
> their type variables are related?
>
> Best regards,
>
> Chun Tian
>
> [1]
> https://github.com/binghe/informatica-public/blob/master/thesis/GraphScript.sml
> [2] van Glabbeek, R.J.: A characterisation of weak bisimulation congruence.
> Lecture notes in computer science. 3838, 26–39 (2005).
>
>
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
