-(* It is now clear that we can build a DFA D_e for e by taking pre as states,
-and move as transition function; the initial state is •(e) and a state 〈i,b〉 is
-final if and only if b is true. The fact that states in D_e are finite is obvious:
-in fact, their cardinality is at most 2^{n+1} where n is the number of symbols in
-e. This is one of the advantages of pointed regular expressions w.r.t. derivatives,
-whose finite nature only holds after a suitable quotient.
-
-Let us discuss a couple of examples.
-
-Example.
-Below is the DFA associated with the regular expression (ac+bc)*.
-
-DFA for (ac+bc)
-
-The graphical description of the automaton is the traditional one, with nodes for
-states and labelled arcs for transitions. Unreachable states are not shown.
-Final states are emphasized by a double circle: since a state 〈e,b〉 is final if and
-only if b is true, we may just label nodes with the item.
-The automaton is not minimal: it is easy to see that the two states corresponding to
-the items (a•c +bc)* and (ac+b•c)* are equivalent (a way to prove it is to observe
-that they define the same language!). In fact, an important property of pres e is that
-each state has a clear semantics, given in terms of the specification e and not of the
-behaviour of the automaton. As a consequence, the construction of the automaton is not
-only direct, but also extremely intuitive and locally verifiable.
-
-Let us consider a more complex case.
-
-Example.
-Starting form the regular expression (a+ϵ)(b*a + b)b, we obtain the following automaton.
-
-DFA for (a+ϵ)(b*a + b)b
-
-Remarkably, this DFA is minimal, testifying the small number of states produced by our
-technique (the pair of states 6-8 and 7-9 differ for the fact that 6 and 7
-are final, while 8 and 9 are not).
-
-
-Move to pit
-.
-
-We conclude this chapter with a few properties of the move opertions in relation
-with the pit state. *)
-
-definition pit_pre ≝ λS.λi.〈blank S (|i|), false〉.
-
-(* The following function compute the list of characters occurring in a given
-item i. *)
-
-let rec occur (S: DeqSet) (i: re S) on i ≝
- match i with
- [ z ⇒ [ ]
- | e ⇒ [ ]
- | s y ⇒ y::[]
- | o e1 e2 ⇒ unique_append ? (occur S e1) (occur S e2)
- | c e1 e2 ⇒ unique_append ? (occur S e1) (occur S e2)
- | k e ⇒ occur S e].
-
-(* If a symbol a does not occur in i, then move(i,a) gets to the
-pit state. *)
-
-lemma not_occur_to_pit: ∀S,a.∀i:pitem S. memb S a (occur S (|i|)) ≠ true →
- move S a i = pit_pre S i.
-#S #a #i elim i //
- [#x normalize cases (a==x) normalize // #H @False_ind /2/
- |#i1 #i2 #Hind1 #Hind2 #H >move_cat
- >Hind1 [2:@(not_to_not … H) #H1 @sublist_unique_append_l1 //]
- >Hind2 [2:@(not_to_not … H) #H1 @sublist_unique_append_l2 //] //
- |#i1 #i2 #Hind1 #Hind2 #H >move_plus
- >Hind1 [2:@(not_to_not … H) #H1 @sublist_unique_append_l1 //]
- >Hind2 [2:@(not_to_not … H) #H1 @sublist_unique_append_l2 //] //
- |#i #Hind #H >move_star >Hind //
+(*
+Lifted Operators
+
+
+Plus and bullet have been already lifted from items to pres. We can now
+do a similar job for concatenation ⊙ and Kleene's star ⊛.*)
+
+definition lifted_cat ≝ λS:DeqSet.λe:pre S.
+ lift S (pre_concat_l S eclose e).
+
+notation "e1 ⊙ e2" left associative with precedence 70 for @{'odot $e1 $e2}.
+
+interpretation "lifted cat" 'odot e1 e2 = (lifted_cat ? e1 e2).
+
+lemma odot_true_b : ∀S.∀i1,i2:pitem S.∀b.
+ 〈i1,true〉 ⊙ 〈i2,b〉 = 〈i1 · (fst \dots (•i2)),snd \dots (•i2) ∨ b〉.
+#S #i1 #i2 #b normalize in ⊢ (??%?); cases (•i2) //
+qed.
+
+lemma odot_false_b : ∀S.∀i1,i2:pitem S.∀b.
+ 〈i1,false〉 ⊙ 〈i2,b〉 = 〈i1 · i2 ,b〉.
+//
+qed.
+
+lemma erase_odot:∀S.∀e1,e2:pre S.
+ |fst \dots (e1 ⊙ e2)| = |fst \dots e1| · (|fst \dots e2|).
+#S * #i1 * * #i2 #b2 // >odot_true_b >erase_dot
+whd in match (fst ???) in ⊢ (???%); whd in match (fst ???) in ⊢ (???%);//
+qed.
+
+(* Let us come to the star operation: *)
+
+definition lk ≝ λS:DeqSet.λe:pre S.
+ match e with
+ [ pair i1 b1 ⇒
+ match b1 with
+ [true ⇒ 〈(fst \dots (eclose ? i1))^*, true〉
+ |false ⇒ 〈i1^*,false〉
+ ]
+ ].
+
+(* notation < "a \sup ⊛" non associative with precedence 90 for @{'lk $a}.*)
+interpretation "lk" 'lk a = (lk ? a).
+notation "a^⊛" non associative with precedence 90 for @{'lk $a}.
+
+lemma ostar_true: ∀S.∀i:pitem S.
+ 〈i,true〉^⊛ = 〈(fst \dots (•i))^*, true〉.
+// qed.
+
+lemma ostar_false: ∀S.∀i:pitem S.
+ 〈i,false〉^⊛ = 〈i^*, false〉.
+// qed.
+
+lemma erase_ostar: ∀S.∀e:pre S.
+ |fst \dots (e^⊛)| = |fst \dots e|^*.
+#S * #i * whd in match (fst ???) in ⊢ (???%); // qed.
+
+lemma sem_odot_true: ∀S:DeqSet.∀e1:pre S.∀i.
+ \sem{e1 ⊙ 〈i,true〉} ≐ \sem{e1 ▹ i} ∪ { [ ] }.
+#S #e1 #i
+cut (e1 ⊙ 〈i,true〉 = 〈fst \dots (e1 ▹ i), snd \dots(e1 ▹ i) ∨ true〉) [//]
+#H >H cases (e1 ▹ i) #i1 #b1 cases b1
+ [>sem_pre_true @eqP_trans [||@eqP_sym @union_assoc]
+ @eqP_union_l #w normalize % [/2/|* //]
+ |/2/