From 201b9451bbb6cc11025a8c71b859f6249529084a Mon Sep 17 00:00:00 2001 From: Michael Norrish Date: Wed, 14 Aug 2024 20:39:41 +1000 Subject: [PATCH] Change addUDEdge to take set of nodes as edge argument Thanks to Chun Tian for the suggestion. This allows addition of hyperedges where that's permitted by the graph type. --- examples/generic_graphs/fsgraphScript.sml | 2 +- .../generic_graphs/genericGraphScript.sml | 100 +++++++++++------- 2 files changed, 62 insertions(+), 40 deletions(-) diff --git a/examples/generic_graphs/fsgraphScript.sml b/examples/generic_graphs/fsgraphScript.sml index 310f108a9d..a86919e71c 100644 --- a/examples/generic_graphs/fsgraphScript.sml +++ b/examples/generic_graphs/fsgraphScript.sml @@ -32,7 +32,7 @@ Definition fsgAddEdges_def: let es = { (m,n) | m ≠ n ∧ m ∈ nodes g ∧ n ∈ nodes g ∧ {m;n} ∈ es0 } in - ITSET (λ(m,n) g. addUDEdge m n () g) es g + ITSET (λ(m,n) g. addUDEdge {m; n} () g) es g End Definition valid_edges_def: diff --git a/examples/generic_graphs/genericGraphScript.sml b/examples/generic_graphs/genericGraphScript.sml index 61ccc2197b..a7cb64882e 100644 --- a/examples/generic_graphs/genericGraphScript.sml +++ b/examples/generic_graphs/genericGraphScript.sml @@ -1058,36 +1058,63 @@ Proof QED Definition addUDEdge0_def: - addUDEdge0 m n lab (G:('a,undirectedG,'ec,'el,'h,'nf,'nl,'sl)graphrep) = - if m = n ∧ ¬itself2bool(:'sl) then G + addUDEdge0 ns lab (G:('a,undirectedG,'ec,'el,'h,'nf,'nl,'sl)graphrep) = + if SING ns ∧ ¬itself2bool(:'sl) then G + else if INFINITE ns ∧ itself2bool(:'nf) then G + else if ¬itself2bool(:'h) ∧ (FINITE ns ⇒ 2 < CARD ns) then G + else if ns = ∅ then G else - G with <| nodes := {m;n} ∪ G.nodes ; - edges := udfilter_insertedge {m;n} lab (:'ec) G.edges + G with <| nodes := ns ∪ G.nodes ; + edges := udfilter_insertedge ns lab (:'ec) G.edges |> End +Theorem TWO_LECARD_I: + FINITE A ∧ ¬SING A ∧ A ≠ ∅ ⇒ 2 ≤ CARD A +Proof + simp[SING_DEF] >> rpt strip_tac >> + ‘∃a A0. A = a INSERT A0 ∧ a ∉ A0’ by metis_tac[SET_CASES] >> gvs[] >> + ‘A0 ≠ ∅’ by (strip_tac >> gvs[]) >> + ‘∃a2 A00. A0 = a2 INSERT A00 ∧ a2 ∉ A00’ by metis_tac[SET_CASES] >> gvs[] +QED + +Theorem CARD_LE2: + FINITE A ⇒ (CARD A ≤ 2 ⇔ A = ∅ ∨ SING A ∨ ∃m n. m ≠ n ∧ A = {m;n}) +Proof + strip_tac >> Cases_on ‘A = ∅’ >> simp[] >> + Cases_on ‘SING A’ + >- gvs[SING_DEF] >> + simp[EQ_IMP_THM, PULL_EXISTS] >> strip_tac >> + ‘CARD A = 0 ∨ CARD A = 1 ∨ CARD A = 2’ by DECIDE_TAC >> gvs[SING_IFF_CARD1] >> + metis_tac[CARDEQ2] +QED + Theorem addUDEdge_respects: - ((=) ===> (=) ===> (=) ===> ceq ===> ceq) addUDEdge0 addUDEdge0 + (((=) ===> (=)) ===> (=) ===> ceq ===> ceq) addUDEdge0 addUDEdge0 Proof - simp[FUN_REL_def, ceq_def] >> + simp[FUN_REL_def, ceq_def, GSYM FUN_EQ_THM] >> simp[addUDEdge0_def, wfgraph_def, ITSELF_UNIQUE] >> - Cases_on ‘m = n’ >> rw[finite_cst_UNION] >>~- - ([‘BAG_IN e $ udfilter_insertedge _ _ _ _’], - drule_then strip_assume_tac BAG_IN_udfilter_insertedge >> simp[] >> - first_x_assum drule >> simp[SUBSET_DEF]) >>~- - ([‘edge_cst _ _’, ‘edge_cst _ (udfilter_insertedge _ _ _ _)’], - qpat_x_assum ‘edge_cst _ _’ mp_tac >> - simp[edge_cst_def] >> - rename [‘itself2_ecv ecst’] >> - Cases_on ‘itself2_ecv ecst’ >> - gvs[finite_edges_per_nodeset_udfilter_insertedge, - only_one_edge_per_label_udfilter_insertedge, - only_one_edge_udfilter_insertedge, ITSELF_UNIQUE]) >> + rw[finite_cst_UNION] >~ + [‘BAG_IN e $ udfilter_insertedge _ _ _ _’] + >- (drule_then strip_assume_tac BAG_IN_udfilter_insertedge >> simp[] >> + first_x_assum drule >> simp[SUBSET_DEF]) >~ + [‘finite_cst _ (A ∪ g.nodes)’] + >- gvs[finite_cst_def, itself2bool_def] >~ + [‘edge_cst _ g.edges’, ‘edge_cst _ (udfilter_insertedge _ _ _ _)’] + >- (qpat_x_assum ‘edge_cst _ _’ mp_tac >> + simp[edge_cst_def] >> + rename [‘itself2_ecv ecst’] >> + Cases_on ‘itself2_ecv ecst’ >> + gvs[finite_edges_per_nodeset_udfilter_insertedge, + only_one_edge_per_label_udfilter_insertedge, + only_one_edge_udfilter_insertedge, ITSELF_UNIQUE]) >> gvs[dirhypcst_def] >> rw[] >> drule_then strip_assume_tac BAG_IN_udfilter_insertedge >>~- ([‘BAG_IN e g.edges (* a *)’], metis_tac[]) >>~- - ([‘core_incident e = {m;n}’], - Cases_on ‘e’ >> gvs[] >> irule_at Any EQ_REFL >> simp[]) + ([‘core_incident e = _’], + Cases_on ‘e’ >> + gvs[TWO_LECARD_I, arithmeticTheory.NOT_LESS, CARD_LE2, INSERT2_lemma] >> + dsimp[] >> gvs[SING_DEF]) QED val (aud1,aud2) = liftdef addUDEdge_respects "addUDEdge" @@ -1294,23 +1321,18 @@ fun F th = seq.hd $ resolve_relhyps [] cleftp rdb th fpow F 4 base *) -Theorem addUDEdge_COMM: - addUDEdge m n lab G = addUDEdge n m lab G -Proof - Cases_on ‘m = n’ >> simp[] >> - time (xfer_back_tac []) >> simp[addUDEdge0_def, INSERT_COMM] -QED Theorem nodes_addUDEdge[simp]: ∀m n lab G. - nodes (addUDEdge m n lab G) = - (if m ≠ n ∨ selfloops_ok G then {m; n} else ∅) ∪ nodes G + nodes (addUDEdge {m;n} lab G) = + (if (m ≠ n ∨ selfloops_ok G) then {m;n} else ∅) ∪ nodes G Proof - simp[] >> xfer_back_tac[] >> simp[addUDEdge0_def] >> rw[] >> gvs[] + simp[] >> xfer_back_tac[] >> simp[addUDEdge0_def] >> rw[] >> gvs[] >> + Cases_on ‘m = n’ >> gvs[] QED Theorem udedges_addUDEdge: - udedges (addUDEdge m n lab G) = + udedges (addUDEdge {m; n} lab G) = if m ≠ n ∨ selfloops_ok G then if oneEdge_max G then {undirected {m;n} lab} ∪ { ude | ude ∈ udedges G ∧ udenodes ude ≠ {m;n} } @@ -1319,16 +1341,16 @@ Theorem udedges_addUDEdge: else udedges G Proof simp[udedges_def, oneEdge_max_def] >> - map_every qid_spec_tac [‘m’, ‘n’, ‘G’, ‘lab’] >> - xfer_back_tac[] >> simp[addUDEdge0_def] >> rw[] >> rw[] >> gvs[] - >- (simp[udfilter_insertedge_def, Once EXTENSION] >> metis_tac[]) >> + xfer_back_tac[] >> simp[addUDEdge0_def] >> rw[] >> rw[] >> gvs[] >> + Cases_on ‘m = n’ >> gvs[] >> + simp[udfilter_insertedge_def, GSPEC_OR, AC CONJ_COMM CONJ_ASSOC] >> rename [‘itself2_ecv x’] >> Cases_on ‘itself2_ecv x’ >> gvs[] >> - simp[udfilter_insertedge_def] >> simp[Once EXTENSION] >> rw[] >> + simp[Once EXTENSION] >> rw[] >> metis_tac[] QED Theorem adjacent_addUDEdge[simp]: - adjacent (addUDEdge m n lab G : ('a,'b,'c,'d,'e,'f)udgraph) a b ⇔ + adjacent (addUDEdge {m; n} lab G : ('a,'b,'c,'d,'e,'f)udgraph) a b ⇔ (m ≠ n ∨ selfloops_ok G) ∧ {a;b} = {m;n} ∨ adjacent G a b Proof simp[adjacent_undirected, udedges_addUDEdge] >> rw[] >> @@ -1352,7 +1374,7 @@ QED (* adding undirected self-edge from n to n in a no-selfloop graph is an identity operation *) Theorem addUDEdge_addNode[simp]: - addUDEdge n n lab (G:(α,'ec,'el,'nf,'nl,noSL) udgraph) = G + addUDEdge {n} lab (G:(α,'ec,'el,'nf,'nl,noSL) udgraph) = G Proof xfer_back_tac [] >> rw[addUDEdge0_def] QED @@ -2732,8 +2754,8 @@ Proof QED Theorem addUDEdge_udul_LCOMM: - addUDEdge m n l1 (addUDEdge a b l2 g : (α,ν,σ)udulgraph) = - addUDEdge a b l2 (addUDEdge m n l1 g) + addUDEdge {m; n} l1 (addUDEdge {a; b} l2 g : (α,ν,σ)udulgraph) = + addUDEdge {a; b} l2 (addUDEdge {m; n} l1 g) Proof simp[gengraph_component_equality] >> rw[] >- SET_TAC[] @@ -2747,7 +2769,7 @@ Theorem edges_ITSET_addUDEdge_udul: FINITE A ∧ (∀m n. (m,n) ∈ A ⇒ m ∈ nodes g ∧ n ∈ nodes g) ∧ (¬selfloops_ok g ⇒ ∀m n. (m,n) ∈ A ⇒ m ≠ n) ⇒ - udedges (ITSET (λ(m,n) g. addUDEdge m n () g) A g) = + udedges (ITSET (λ(m,n) g. addUDEdge {m; n} () g) A g) = { undirected {m;n} () | (m,n) ∈ A } ∪ udedges g Proof Induct_on ‘FINITE’ >>