tphols-2011

By xingyuan

January 24, 2011

Contents

1 Preliminary definitions  1
2 The direction regular language ⇒finite partition (easier direction) 4
2.1 Basic notions needed for this direction . . . . . . . . . . . . . 4
2.2 Some lemmas for basic cases . . . . . . . . . . . . . . . . . . . 5
2.3 The case for SEQ . . . . . . . . . . . . . . . . . . . . . . . . . 6

theory Myhill imports Main List-Prefix begin

1 Preliminary definitions

Sequential composition of two languages L1 and L2

definition Seq :: string set ⇒ string set ⇒ string set (- ;; - [100 ,100 ] 100 ) where L1 ;; L2 = {s1 @ s2 | s1 s2 . s1 ∈ L1 ∧ s2 ∈ L2 }

Transitive closure of language L.

inductive-set Star :: string set ⇒ string set (-⋆ [101 ] 102 ) for L :: string set where start[intro]: [] ∈ L⋆ | step[intro]: [[s1 ∈ L; s2 ∈ L⋆]] ⟹ s1 @s2 ∈ L⋆

Some properties of operator ;;.

lemma seq-union-distrib: (A ∪ B) ;; C = (A ;; C ) ∪ (B ;; C ) by (auto simp:Seq-def )

lemma seq-intro: [[x ∈ A; y ∈ B]] ⟹ x @ y ∈ A ;; B by (auto simp:Seq-def ) lemma seq-assoc: (A ;; B) ;; C = A ;; (B ;; C ) apply(auto simp:Seq-def ) apply blast by (metis append-assoc)

lemma star-intro1 [rule-format]: x ∈ lang⋆ ⟹ ∀ y. y ∈ lang⋆ ⟶ x @ y ∈ lang⋆ by (erule Star.induct, auto)

lemma star-intro2 : y ∈ lang ⟹ y ∈ lang⋆ by (drule step[of y lang []], auto simp:start)

lemma star-intro3 [rule-format]: x ∈ lang⋆ ⟹ ∀ y . y ∈ lang ⟶ x @ y ∈ lang⋆ by (erule Star.induct, auto intro:star-intro2 )

lemma star-decom: [[x ∈ lang⋆; x ≠ []]] ⟹(∃ a b. x = a @ b ∧ a ≠ [] ∧ a ∈ lang ∧ b ∈ lang⋆) by (induct x rule: Star.induct, simp, blast)

lemma star-decom′: [[x ∈ lang⋆; x ≠ []]] ⟹ ∃ a b. x = a @ b ∧ a ∈ lang⋆ ∧ b ∈ lang apply (induct x rule:Star.induct, simp) apply (case-tac s2 = []) apply (rule-tac x = [] in exI , rule-tac x = s1 in exI , simp add:start) apply (simp, (erule exE | erule conjE)+) by (rule-tac x = s1 @ a in exI , rule-tac x = b in exI , simp add:step)

Ardens lemma expressed at the level of language, rather than the level of regular expression.

axioms ardens-revised: [] ∉ A ⟹ (X = X ;; A ∪ B) = (X = B ;; A⋆)

The syntax of regular expressions is defined by the datatype rexp.

datatype rexp = NULL | EMPTY | CHAR char | SEQ rexp rexp | ALT rexp rexp | STAR rexp

The following L is an overloaded operator, where L(x) evaluates to the language represented by the syntactic object x.

consts L:: ′a ⇒ string set

The L(rexp) for regular expression rexp is defined by the following overloading function L-rexp.

overloading L-rexp ≡ L:: rexp ⇒ string set begin fun L-rexp :: rexp ⇒ string set where

L-rexp (NULL) = {} | L-rexp (EMPTY ) = {[]} | L-rexp (CHAR c) = {[c]} | L-rexp (SEQ r1 r2 ) = (L-rexp r1 ) ;; (L-rexp r2 ) | L-rexp (ALT r1 r2 ) = (L-rexp r1 ) ∪ (L-rexp r2 ) | L-rexp (STAR r) = (L-rexp r)⋆ end

To obtain equational system out of finite set of equivalent classes, a fold operation on finite set folds is defined. The use of SOME makes fold more robust than the fold in Isabelle library. The expression folds f makes sense when f is not associative and commutitive, while fold f does not.

definition folds :: (′a ⇒ ′b ⇒ ′b) ⇒ ′b ⇒ ′a set ⇒ ′b where folds f z S ≡ SOME x. fold-graph f z S x

The following lemma assures that the arbitrary choice made by the SOME in folds does not affect the L-value of the resultant regular expression.

lemma folds-alt-simp [simp]: finite rs ⟹ L (folds ALT NULL rs) = ⋃ (L ‘ rs) apply (rule set-ext, simp add:folds-def ) apply (rule someI2-ex, erule finite-imp-fold-graph) by (erule fold-graph.induct, auto)

lemma [simp]: shows (x, y) ∈ {(x, y). P x y} ⟷ P x y by simp

≈L is an equivalent class defined by language Lang.

definition str-eq-rel (≈-) where ≈Lang ≡ {(x, y). (∀ z. x @ z ∈ Lang ⟷ y @ z ∈ Lang)}

Among equivlant clases of ≈Lang, the set finals(Lang) singles out those which contains strings from Lang.

definition finals Lang ≡ {≈Lang ‘‘ {x} | x . x ∈ Lang}

The following lemma show the relationshipt between finals(Lang) and Lang.

lemma lang-is-union-of-finals:

Lang = ⋃ finals(Lang) proof show Lang ⊆ ⋃ (finals Lang) proof fix x assume x ∈ Lang thus x ∈ ⋃ (finals Lang) apply (simp add:finals-def , rule-tac x = (≈Lang) ‘‘ {x} in exI ) by (auto simp:Image-def str-eq-rel-def )

qed next show ⋃ (finals Lang) ⊆ Lang apply (clarsimp simp:finals-def str-eq-rel-def ) by (drule-tac x = [] in spec, auto)

qed

2 The direction regular language ⇒finite partition (easier direction)

2.1 Basic notions needed for this direction

definition str-eq (- ≈- -) where x ≈Lang y ≡ (x, y) ∈ (≈Lang)

lemma finite-tag-imageI : finite (range tag) ⟹ finite (((op ‘) tag) ‘ S) apply (rule-tac B = Pow (tag ‘ UNIV ) in finite-subset) by (auto simp add:image-def Pow-def )

lemma eq-class-equalI : [[X ∈ UNIV // ≈lang; Y ∈ UNIV // ≈lang; x ∈ X ; y ∈ Y ; x ≈lang y]] ⟹ X = Y by (auto simp:quotient-def str-eq-rel-def str-eq-def )

lemma tag-image-injI : assumes str-inj : ⋀ x y. tag x = tag (y::string) ⟹ x ≈lang y shows inj-on ((op ‘) tag) (UNIV // ≈lang) proof− { fix X Y assume X-in: X ∈ UNIV // ≈lang and Y-in: Y ∈ UNIV // ≈lang and tag-eq: tag ‘ X = tag ‘ Y then obtain x y where x ∈ X and y ∈ Y and tag x = tag y unfolding quotient-def Image-def str-eq-rel-def str-eq-def image-def apply simp by blast with X-in Y-in str-inj have X = Y by (rule-tac eq-class-equalI , simp+)

} thus ?thesis unfolding inj-on-def by auto qed

2.2 Some lemmas for basic cases

lemma quot-empty-subset: UNIV // (≈{[]}) ⊆ {{[]}, UNIV − {[]}} proof fix x assume x ∈ UNIV // ≈{[]} then obtain y where h: x = {z. (y, z) ∈ ≈{[]}} unfolding quotient-def

Image-def by blast show x ∈ {{[]}, UNIV − {[]}} proof (cases y = []) case True with h have x = {[]} by (auto simp:str-eq-rel-def ) thus ?thesis by simp next case False with h have x = UNIV − {[]} by (auto simp:str-eq-rel-def ) thus ?thesis by simp qed qed

lemma quot-char-subset: UNIV // (≈{[c]}) ⊆ {{[]},{[c]}, UNIV − {[], [c]}} proof fix x assume x ∈ UNIV // ≈{[c]} then obtain y where h: x = {z. (y, z) ∈ ≈{[c]}} unfolding quotient-def

Image-def by blast show x ∈ {{[]},{[c]}, UNIV − {[], [c]}} proof − { assume y = [] hence x = {[]} using h by (auto simp:str-eq-rel-def ) } moreover { assume y = [c] hence x = {[c]} using h by (auto dest!:spec[where x = []] simp:str-eq-rel-def )

} moreover {

assume y ≠ [] and y ≠ [c]

hence ∀ z. (y @ z) ≠ [c] by (case-tac y, auto)

moreover have ⋀ p. (p ≠ [] ∧ p ≠ [c]) = (∀ q. p @ q ≠ [c]) by (case-tac p, auto)

ultimately have x = UNIV − {[],[c]} using h by (auto simp add:str-eq-rel-def )

} ultimately show ?thesis by blast qed qed

2.3 The case for SEQ

end