# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1502479741 -3600
# Node ID 32b222d77fa0303012e2f41a42a81de6f207fb5e
# Parent  fff2e1b40dfc11de30c8cc687b3286abf030c3d3
updated

diff -r fff2e1b40dfc -r 32b222d77fa0 thys/Journal/Paper.thy
--- a/thys/Journal/Paper.thy	Wed Jul 19 14:55:46 2017 +0100
+++ b/thys/Journal/Paper.thy	Fri Aug 11 20:29:01 2017 +0100
@@ -15,6 +15,11 @@
 
 declare [[show_question_marks = false]]
 
+syntax (latex output)
+  "_Collect" :: "pttrn => bool => 'a set"              ("(1{_ \<^raw:\mbox{\boldmath$\mid$}> _})")
+  "_CollectIn" :: "pttrn => 'a set => bool => 'a set"   ("(1{_ \<in> _ |e _})")
+
+
 abbreviation 
   "der_syn r c \<equiv> der c r"
 
@@ -26,12 +31,14 @@
   "nprec v1 v2 \<equiv> \<not>(v1 :\<sqsubset>val v2)"
 
 
+
+
 notation (latex output)
   If  ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and
   Cons ("_\<^raw:\mbox{$\,$}>::\<^raw:\mbox{$\,$}>_" [75,73] 73) and  
 
   ZERO ("\<^bold>0" 78) and 
-  ONE ("\<^bold>1" 78) and 
+  ONE ("\<^bold>1" 1000) and 
   CHAR ("_" [1000] 80) and
   ALT ("_ + _" [77,77] 78) and
   SEQ ("_ \<cdot> _" [77,77] 78) and
@@ -53,8 +60,10 @@
   mkeps ("mkeps _" [79] 76) and 
   length ("len _" [73] 73) and
   intlen ("len _" [73] 73) and
+  set ("_" [73] 73) and
  
-  Prf ("_ : _" [75,75] 75) and  
+  Prf ("_ : _" [75,75] 75) and
+  CPrf ("_ \<^raw:\mbox{\textbf{\textlengthmark}}> _" [75,75] 75) and
   Posix ("'(_, _') \<rightarrow> _" [63,75,75] 75) and
  
   lexer ("lexer _ _" [78,78] 77) and 
@@ -84,6 +93,13 @@
 definition 
   "match r s \<equiv> nullable (ders s r)"
 
+
+lemma CV_STAR_ONE_empty: 
+  shows "CV (STAR ONE) [] = {Stars []}"
+by(auto simp add: CV_def elim: CPrf.cases intro: CPrf.intros)
+
+
+
 (*
 comments not implemented
 
@@ -94,6 +110,8 @@
 
 (*>*)
 
+
+
 section {* Introduction *}
 
 
@@ -153,7 +171,7 @@
 not match an empty string unless this is the only match for the repetition.\smallskip
 
 \item[$\bullet$] \emph{Empty String Rule:} An empty string shall be considered to 
-be longer than no match at all.
+be longer than no match at all.\marginpar{Explain its purpose}
 \end{itemize}
 
 \noindent Consider for example a regular expression @{text "r\<^bsub>key\<^esub>"} for recognising keywords
@@ -165,7 +183,9 @@
 by the Longest Match Rule a single identifier token, not a keyword
 followed by an identifier. For @{text "if"} we obtain by the Priority
 Rule a keyword token, not an identifier token---even if @{text "r\<^bsub>id\<^esub>"}
-matches also.
+matches also. By the Star Rule we know @{text "(r\<^bsub>key\<^esub> + r\<^bsub>id\<^esub>)\<^sup>\<star>"} matches @{text "iffoo"}, respectively @{text "if"}, in exactly one
+`iteration' of the star.
+
 
 One limitation of Brzozowski's matcher is that it only generates a
 YES/NO answer for whether a string is being matched by a regular
@@ -185,7 +205,8 @@
 algorithm. This proof idea is inspired by work of Frisch and Cardelli
 \cite{Frisch2004} on a GREEDY regular expression matching
 algorithm. However, we were not able to establish transitivity and
-totality for the ``order relation'' by Sulzmann and Lu. ??In Section
+totality for the ``order relation'' by Sulzmann and Lu. \marginpar{We probably drop this section} 
+??In Section
 \ref{argu} we identify some inherent problems with their approach (of
 which some of the proofs are not published in \cite{Sulzmann2014});
 perhaps more importantly, we give a simple inductive (and
@@ -230,6 +251,8 @@
 informal proof contains gaps, and possible fixes are not fully worked out.}
 Our specification of a POSIX value consists of a simple inductive definition
 that given a string and a regular expression uniquely determines this value.
+We also show that our definition is equivalent to an ordering 
+of values based on positions by Okui and Suzuki \cite{OkuiSuzuki2013}.
 Derivatives as calculated by Brzozowski's method are usually more complex
 regular expressions than the initial one; various optimisations are
 possible. We prove the correctness when simplifications of @{term "ALT ZERO
@@ -267,13 +290,10 @@
   recursive function @{term L} with the six clauses:
 
   \begin{center}
-  \begin{tabular}{l@ {\hspace{3mm}}rcl}
+  \begin{tabular}{l@ {\hspace{4mm}}rcl}
   (1) & @{thm (lhs) L.simps(1)} & $\dn$ & @{thm (rhs) L.simps(1)}\\
   (2) & @{thm (lhs) L.simps(2)} & $\dn$ & @{thm (rhs) L.simps(2)}\\
   (3) & @{thm (lhs) L.simps(3)} & $\dn$ & @{thm (rhs) L.simps(3)}\\
-  \end{tabular}
-  \hspace{14mm}
-  \begin{tabular}{l@ {\hspace{3mm}}rcl}
   (4) & @{thm (lhs) L.simps(4)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) L.simps(4)[of "r\<^sub>1" "r\<^sub>2"]}\\
   (5) & @{thm (lhs) L.simps(5)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) L.simps(5)[of "r\<^sub>1" "r\<^sub>2"]}\\
   (6) & @{thm (lhs) L.simps(6)} & $\dn$ & @{thm (rhs) L.simps(6)}\\
@@ -325,14 +345,12 @@
   @{thm (lhs) nullable.simps(3)} & $\dn$ & @{thm (rhs) nullable.simps(3)}\\
   @{thm (lhs) nullable.simps(4)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) nullable.simps(4)[of "r\<^sub>1" "r\<^sub>2"]}\\
   @{thm (lhs) nullable.simps(5)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) nullable.simps(5)[of "r\<^sub>1" "r\<^sub>2"]}\\
-  @{thm (lhs) nullable.simps(6)} & $\dn$ & @{thm (rhs) nullable.simps(6)}\medskip\\
-  
-  %\end{tabular}
-  %\end{center}
+  @{thm (lhs) nullable.simps(6)} & $\dn$ & @{thm (rhs) nullable.simps(6)}%\medskip\\
+  \end{tabular}
+  \end{center}
 
-  %\begin{center}
-  %\begin{tabular}{lcl}
-  
+  \begin{center}
+  \begin{tabular}{lcl}
   @{thm (lhs) der.simps(1)} & $\dn$ & @{thm (rhs) der.simps(1)}\\
   @{thm (lhs) der.simps(2)} & $\dn$ & @{thm (rhs) der.simps(2)}\\
   @{thm (lhs) der.simps(3)} & $\dn$ & @{thm (rhs) der.simps(3)}\\
@@ -384,7 +402,7 @@
 
 text {* 
 
-  The clever idea by Sulzmann and Lu \cite{Sulzmann2014} is to define
+  The clever idea by Sulzmann and Lu \cite{Sulzmann2014} is to use
   values for encoding \emph{how} a regular expression matches a string
   and then define a function on values that mirrors (but inverts) the
   construction of the derivative on regular expressions. \emph{Values}
@@ -422,7 +440,7 @@
   \end{center}
 
   \noindent Sulzmann and Lu also define inductively an inhabitation relation
-  that associates values to regular expressions:
+  that associates values to regular expressions
 
   \begin{center}
   \begin{tabular}{c}
@@ -436,7 +454,10 @@
   \end{tabular}
   \end{center}
 
-  \noindent Note that no values are associated with the regular expression
+  \noindent 
+  where in the clause for @{const "Stars"} we use the notation @{term "v \<in> set vs"}
+  for indicating that @{text v} is a member in the list @{text vs}.
+  Note that no values are associated with the regular expression
   @{term ZERO}, and that the only value associated with the regular
   expression @{term ONE} is @{term Void}, pronounced (if one must) as @{text
   "Void"}. It is routine to establish how values ``inhabiting'' a regular
@@ -446,10 +467,58 @@
   @{thm L_flat_Prf}
   \end{proposition}
 
-  In general there is more than one value associated with a regular
-  expression. In case of POSIX matching the problem is to calculate the
-  unique value that satisfies the (informal) POSIX rules from the
-  Introduction. Graphically the POSIX value calculation algorithm by
+  \noindent
+  Given a regular expression @{text r} and a string @{text s}, we can define the 
+  set of all \emph{Lexical Values} inhabited by @{text r} with the underlying string 
+  being @{text s} by
+  
+  \begin{center}
+  @{thm LV_def}
+  \end{center}
+
+  \noindent However, later on it will sometimes be necessary to
+  restrict the set of lexical values to a subset called
+  \emph{Canonical Values}. The idea of canonical values is that they
+  satisfy the Star Rule (see Introduction) where the $^\star$ does not
+  match the empty string unless this is the only match for the
+  repetition.  One way to define canonical values formally is to use a
+  stronger inhabitation relation, written @{term "\<Turnstile> DUMMY : DUMMY"}, which has the same rules as @{term
+  "\<turnstile> DUMMY : DUMMY"} shown above, except that the rule for 
+  @{term Stars} has
+  the additional side-condition of flattened values not being the
+  empty string, namely
+
+  \begin{center}
+  @{thm [mode=Rule] CPrf.intros(6)}
+  \end{center}
+
+  \noindent
+  With this we can define
+  
+  \begin{center}
+  @{thm CV_def}
+  \end{center}
+
+  \noindent
+  Clearly we have @{thm LV_CV_subset}.
+  The main point of canonical values is that for every regular expression @{text r} and every
+  string @{text s}, the set @{term "CV r s"} is finite.
+
+  \begin{lemma}
+  @{thm CV_finite}
+  \end{lemma}
+
+  \noindent This finiteness property does not generally hold for lexical values where
+  for example @{term "LV (STAR ONE) []"} contains infinitely many
+  values, but @{thm CV_STAR_ONE_empty}. However, if a regular
+  expression @{text r} matches a string @{text s}, then in general the
+  set @{term "CV r s"} is not just a
+  singleton set.  In case of POSIX matching the problem is to
+  calculate the unique value that satisfies the (informal) POSIX rules
+  from the Introduction. It will turn out that this POSIX value is in fact a
+  canonical value.
+
+  Graphically the POSIX value calculation algorithm by
   Sulzmann and Lu can be illustrated by the picture in Figure~\ref{Sulz}
   where the path from the left to the right involving @{term derivatives}/@{const
   nullable} is the first phase of the algorithm (calculating successive
@@ -614,7 +683,7 @@
   \end{proof}
 
   Having defined the @{const mkeps} and @{text inj} function we can extend
-  \Brz's matcher so that a [lexical] value is constructed (assuming the
+  \Brz's matcher so that a value is constructed (assuming the
   regular expression matches the string). The clauses of the Sulzmann and Lu lexer are
 
   \begin{center}
@@ -633,19 +702,25 @@
   functional programming language and also in Isabelle/HOL. In the remaining
   part of this section we prove that this algorithm is correct.
 
-  The well-known idea of POSIX matching is informally defined by the longest
-  match and priority rule (see Introduction); as correctly argued in \cite{Sulzmann2014}, this
+  The well-known idea of POSIX matching is informally defined by some
+  rules such as the longest match and priority rule (see
+  Introduction); as correctly argued in \cite{Sulzmann2014}, this
   needs formal specification. Sulzmann and Lu define an ``ordering
-  relation'' between values and argue
-  that there is a maximum value, as given by the derivative-based algorithm.
-  In contrast, we shall introduce a simple inductive definition that
-  specifies directly what a \emph{POSIX value} is, incorporating the
-  POSIX-specific choices into the side-conditions of our rules. Our
-  definition is inspired by the matching relation given by Vansummeren
-  \cite{Vansummeren2006}. The relation we define is ternary and written as
-  \mbox{@{term "s \<in> r \<rightarrow> v"}}, relating strings, regular expressions and
-  values.
+  relation'' between values and argue that there is a maximum value,
+  as given by the derivative-based algorithm.  In contrast, we shall
+  introduce a simple inductive definition that specifies directly what
+  a \emph{POSIX value} is, incorporating the POSIX-specific choices
+  into the side-conditions of our rules. Our definition is inspired by
+  the matching relation given by Vansummeren
+  \cite{Vansummeren2006}. The relation we define is ternary and
+  written as \mbox{@{term "s \<in> r \<rightarrow> v"}}, relating
+  strings, regular expressions and values; the inductive rules are given in 
+  Figure~\ref{POSIXrules}.
+  We can prove that given a string @{term s} and regular expression @{term
+   r}, the POSIX value @{term v} is uniquely determined by @{term "s \<in> r \<rightarrow> v"}.
+
   %
+  \begin{figure}[t]
   \begin{center}
   \begin{tabular}{c}
   @{thm[mode=Axiom] Posix.intros(1)}@{text "P"}@{term "ONE"} \qquad
@@ -668,10 +743,10 @@
    {@{thm (concl) Posix.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]}}$@{text "P\<star>"}
   \end{tabular}
   \end{center}
+  \caption{Our inductive definition of POSIX values.}\label{POSIXrules}
+  \end{figure}
 
-   \noindent
-   We can prove that given a string @{term s} and regular expression @{term
-   r}, the POSIX value @{term v} is uniquely determined by @{term "s \<in> r \<rightarrow> v"}.
+   
 
   \begin{theorem}\mbox{}\smallskip\\\label{posixdeterm}
   \begin{tabular}{ll}
@@ -687,7 +762,7 @@
   \end{proof}
 
   \noindent
-  We claim that our @{term "s \<in> r \<rightarrow> v"} relation captures the idea behind the two
+  We claim that our @{term "s \<in> r \<rightarrow> v"} relation captures the idea behind the four
   informal POSIX rules shown in the Introduction: Consider for example the
   rules @{text "P+L"} and @{text "P+R"} where the POSIX value for a string
   and an alternative regular expression, that is @{term "(s, ALT r\<^sub>1 r\<^sub>2)"},
@@ -718,8 +793,19 @@
   @{term v} cannot be flattened to the empty string. In effect, we require
   that in each ``iteration'' of the star, some non-empty substring needs to
   be ``chipped'' away; only in case of the empty string we accept @{term
-  "Stars []"} as the POSIX value.
+  "Stars []"} as the POSIX value. Indeed we can show that our POSIX value
+  is a canonical value which excludes those @{text Stars} containing values 
+  that flatten to the empty string.
 
+  \begin{lemma}
+  @{thm [mode=IfThen] Posix_CV}
+  \end{lemma}
+
+  \begin{proof}
+  By routine induction on @{thm (prem 1) Posix_CV}.\qed 
+  \end{proof}
+
+  \noindent
   Next is the lemma that shows the function @{term "mkeps"} calculates
   the POSIX value for the empty string and a nullable regular expression.
 
@@ -1117,17 +1203,11 @@
 
 text {*
 
- Theorems:
-
- @{thm [mode=IfThen] Posix_CPT}
+ Theorem 1:
 
  @{thm [mode=IfThen] Posix_PosOrd[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]}
 
- Corrollary from the last one
-
- @{thm [mode=IfThen] Posix_PosOrd_stronger[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]}
-
- Theorem
+ Theorem 2:
 
  @{thm [mode=IfThen] PosOrd_Posix[where ?v1.0="v\<^sub>1"]}
 *}
diff -r fff2e1b40dfc -r 32b222d77fa0 thys/Journal/document/root.tex
--- a/thys/Journal/document/root.tex	Wed Jul 19 14:55:46 2017 +0100
+++ b/thys/Journal/document/root.tex	Fri Aug 11 20:29:01 2017 +0100
@@ -12,6 +12,9 @@
 %%\usepackage{stmaryrd}
 \usepackage{url}
 \usepackage{color}
+\usepackage[safe]{tipa}
+
+
 
 \titlerunning{POSIX Lexing with Derivatives of Regular Expressions}
 
@@ -26,6 +29,8 @@
 \renewcommand{\isasymemptyset}{$\varnothing$}
 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
 \renewcommand{\isasymiota}{\makebox[0mm]{${}^{\prime}$}}
+\renewcommand{\isasymin}{\ensuremath{\,\in\,}}
+
 
 \def\Brz{Brzozowski}
 \def\der{\backslash}
@@ -36,8 +41,10 @@
 \renewcommand{\thefootnote}{$\star$} \footnotetext[1]{This paper is a
   revised and expanded version of \cite{AusafDyckhoffUrban2016}.
   Compared with that paper we give a second definition for POSIX
-  values and prove that it is equivalent to the original one. This
-  definition is based on an ordering of values and very similar to the
+  values introduced by Okui Suzuki \cite{OkuiSuzuki2013} and prove that it is
+  equivalent to our original one. This
+  second definition is based on an ordering of values and very similar to,
+  but not equivalent with, the
   definition given by Sulzmann and Lu~\cite{Sulzmann2014}. We also
   extend our results to additional constructors of regular
   expressions.}  \renewcommand{\thefootnote}{\arabic{footnote}}
@@ -54,7 +61,6 @@
 \maketitle
 
 \begin{abstract}
-
 Brzozowski introduced the notion of derivatives for regular
 expressions. They can be used for a very simple regular expression
 matching algorithm.  Sulzmann and Lu cleverly extended this algorithm
@@ -68,10 +74,10 @@
 of an optimised version of the POSIX matching algorithm.  In the
 second part we show that $(iii)$ our inductive definition of a POSIX
 value is equivalent to an alternative definition by Okui and Suzuki
-which identifies a POSIX value as least element according to an
+which identifies POSIX values as least elements according to an
 ordering of values. The advantage of the definition based on the
-ordering is that it implements more directly the POSIX
-longest-leftmost matching semantics.\smallskip
+ordering is that it implements more directly the informal rules from the
+POSIX standard.\smallskip
 
 {\bf Keywords:} POSIX matching, Derivatives of Regular Expressions,
 Isabelle/HOL
diff -r fff2e1b40dfc -r 32b222d77fa0 thys/Paper/document/root.tex
--- a/thys/Paper/document/root.tex	Wed Jul 19 14:55:46 2017 +0100
+++ b/thys/Paper/document/root.tex	Fri Aug 11 20:29:01 2017 +0100
@@ -1,4 +1,5 @@
 \documentclass[runningheads]{llncs}
+\usepackage{stix}
 \usepackage{times}
 \usepackage{isabelle}
 \usepackage{isabellesym}
@@ -13,6 +14,8 @@
 \usepackage{url}
 \usepackage{color}
 
+
+
 \titlerunning{POSIX Lexing with Derivatives of Regular Expressions}
 
 \urlstyle{rm}
diff -r fff2e1b40dfc -r 32b222d77fa0 thys/Positions.thy
--- a/thys/Positions.thy	Wed Jul 19 14:55:46 2017 +0100
+++ b/thys/Positions.thy	Fri Aug 11 20:29:01 2017 +0100
@@ -31,10 +31,8 @@
 lemma Pos_stars:
   "Pos (Stars vs) = {[]} \<union> (\<Union>n < length vs. {n#ps | ps. ps \<in> Pos (vs ! n)})"
 apply(induct vs)
-apply(simp) 
-apply(simp add: insert_ident)
-apply(rule subset_antisym)
-using less_Suc_eq_0_disj by auto
+apply(auto simp add: insert_ident less_Suc_eq_0_disj)
+done
 
 lemma Pos_empty:
   shows "[] \<in> Pos v"
@@ -45,31 +43,25 @@
   "intlen [] = 0"
 | "intlen (x # xs) = 1 + intlen xs"
 
+lemma intlen_int:
+  shows "intlen xs = int (length xs)"
+by (induct xs)(simp_all)
+
 lemma intlen_bigger:
   shows "0 \<le> intlen xs"
 by (induct xs)(auto)
 
 lemma intlen_append:
   shows "intlen (xs @ ys) = intlen xs + intlen ys"
-by (induct xs arbitrary: ys) (auto)
+by (simp add: intlen_int)
 
 lemma intlen_length:
   shows "intlen xs < intlen ys \<longleftrightarrow> length xs < length ys"
-apply(induct xs arbitrary: ys)
-apply (auto simp add: intlen_bigger not_less)
-apply (metis intlen.elims intlen_bigger le_imp_0_less)
-apply (smt Suc_lessI intlen.simps(2) length_Suc_conv nat_neq_iff)
-by (smt Suc_lessE intlen.simps(2) length_Suc_conv)
+by (simp add: intlen_int)
 
 lemma intlen_length_eq:
   shows "intlen xs = intlen ys \<longleftrightarrow> length xs = length ys"
-apply(induct xs arbitrary: ys)
-apply (auto simp add: intlen_bigger not_less)
-apply(case_tac ys)
-apply(simp_all)
-apply (smt intlen_bigger)
-apply (smt intlen.elims intlen_bigger length_Suc_conv)
-by (metis intlen.simps(2) length_Suc_conv)
+by (simp add: intlen_int)
 
 definition pflat_len :: "val \<Rightarrow> nat list => int"
 where
@@ -90,7 +82,7 @@
 lemma pflat_len_Stars_simps:
   assumes "n < length vs"
   shows "pflat_len (Stars vs) (n#p) = pflat_len (vs!n) p"
-using assms 
+using assms
 apply(induct vs arbitrary: n p)
 apply(auto simp add: less_Suc_eq_0_disj pflat_len_simps)
 done
@@ -98,7 +90,8 @@
 lemma pflat_len_outside:
   assumes "p \<notin> Pos v1"
   shows "pflat_len v1 p = -1 "
-using assms by (auto simp add: pflat_len_def)
+using assms by (simp add: pflat_len_def)
+
 
 
 section {* Orderings *}
@@ -175,15 +168,10 @@
 lemma PosOrd_shorterE:
   assumes "v1 :\<sqsubset>val v2" 
   shows "length (flat v2) \<le> length (flat v1)"
-using assms
-apply(auto simp add: pflat_len_simps PosOrd_ex_def PosOrd_def)
-apply(case_tac p)
-apply(simp add: pflat_len_simps intlen_length)
-apply(simp)
-apply(drule_tac x="[]" in bspec)
-apply(simp add: Pos_empty)
-apply(simp add: pflat_len_simps le_less intlen_length_eq)
-done
+using assms unfolding PosOrd_ex_def PosOrd_def
+apply(auto simp add: pflat_len_def intlen_int split: if_splits)
+apply (metis Pos_empty Un_iff at.simps(1) eq_iff lex_simps(1) nat_less_le)
+by (metis Pos_empty UnI2 at.simps(1) lex_simps(2) lex_trichotomous linear)
 
 lemma PosOrd_shorterI:
   assumes "length (flat v2) < length (flat v1)"
@@ -206,8 +194,7 @@
 unfolding PosOrd_ex_def
 apply(rule_tac x="[0]" in exI)
 using assms 
-apply(auto simp add: PosOrd_def pflat_len_simps)
-apply(smt intlen_bigger)
+apply(auto simp add: PosOrd_def pflat_len_simps intlen_int)
 done
 
 lemma PosOrd_Left_eq:
@@ -547,34 +534,35 @@
 by (metis PosOrd_SeqI1 PosOrd_shorterI WW1 antisym_conv3 append_eq_append_conv assms(2))
 
 
+
 section {* The Posix Value is smaller than any other Value *}
 
 
 lemma Posix_PosOrd:
-  assumes "s \<in> r \<rightarrow> v1" "v2 \<in> CPT r s" 
+  assumes "s \<in> r \<rightarrow> v1" "v2 \<in> CV r s" 
   shows "v1 :\<sqsubseteq>val v2"
 using assms
 proof (induct arbitrary: v2 rule: Posix.induct)
   case (Posix_ONE v)
-  have "v \<in> CPT ONE []" by fact
+  have "v \<in> CV ONE []" by fact
   then have "v = Void"
-    by (simp add: CPT_simps)
+    by (simp add: CV_simps)
   then show "Void :\<sqsubseteq>val v"
     by (simp add: PosOrd_ex_eq_def)
 next
   case (Posix_CHAR c v)
-  have "v \<in> CPT (CHAR c) [c]" by fact
+  have "v \<in> CV (CHAR c) [c]" by fact
   then have "v = Char c"
-    by (simp add: CPT_simps)
+    by (simp add: CV_simps)
   then show "Char c :\<sqsubseteq>val v"
     by (simp add: PosOrd_ex_eq_def)
 next
   case (Posix_ALT1 s r1 v r2 v2)
   have as1: "s \<in> r1 \<rightarrow> v" by fact
-  have IH: "\<And>v2. v2 \<in> CPT r1 s \<Longrightarrow> v :\<sqsubseteq>val v2" by fact
-  have "v2 \<in> CPT (ALT r1 r2) s" by fact
+  have IH: "\<And>v2. v2 \<in> CV r1 s \<Longrightarrow> v :\<sqsubseteq>val v2" by fact
+  have "v2 \<in> CV (ALT r1 r2) s" by fact
   then have "\<Turnstile> v2 : ALT r1 r2" "flat v2 = s"
-    by(auto simp add: CPT_def prefix_list_def)
+    by(auto simp add: CV_def prefix_list_def)
   then consider
     (Left) v3 where "v2 = Left v3" "\<Turnstile> v3 : r1" "flat v3 = s" 
   | (Right) v3 where "v2 = Right v3" "\<Turnstile> v3 : r2" "flat v3 = s"
@@ -582,8 +570,8 @@
   then show "Left v :\<sqsubseteq>val v2"
   proof(cases)
      case (Left v3)
-     have "v3 \<in> CPT r1 s" using Left(2,3) 
-       by (auto simp add: CPT_def prefix_list_def)
+     have "v3 \<in> CV r1 s" using Left(2,3) 
+       by (auto simp add: CV_def prefix_list_def)
      with IH have "v :\<sqsubseteq>val v3" by simp
      moreover
      have "flat v3 = flat v" using as1 Left(3)
@@ -603,10 +591,10 @@
   case (Posix_ALT2 s r2 v r1 v2)
   have as1: "s \<in> r2 \<rightarrow> v" by fact
   have as2: "s \<notin> L r1" by fact
-  have IH: "\<And>v2. v2 \<in> CPT r2 s \<Longrightarrow> v :\<sqsubseteq>val v2" by fact
-  have "v2 \<in> CPT (ALT r1 r2) s" by fact
+  have IH: "\<And>v2. v2 \<in> CV r2 s \<Longrightarrow> v :\<sqsubseteq>val v2" by fact
+  have "v2 \<in> CV (ALT r1 r2) s" by fact
   then have "\<Turnstile> v2 : ALT r1 r2" "flat v2 = s"
-    by(auto simp add: CPT_def prefix_list_def)
+    by(auto simp add: CV_def prefix_list_def)
   then consider
     (Left) v3 where "v2 = Left v3" "\<Turnstile> v3 : r1" "flat v3 = s" 
   | (Right) v3 where "v2 = Right v3" "\<Turnstile> v3 : r2" "flat v3 = s"
@@ -614,8 +602,8 @@
   then show "Right v :\<sqsubseteq>val v2"
   proof (cases)
     case (Right v3)
-     have "v3 \<in> CPT r2 s" using Right(2,3) 
-       by (auto simp add: CPT_def prefix_list_def)
+     have "v3 \<in> CV r2 s" using Right(2,3) 
+       by (auto simp add: CV_def prefix_list_def)
      with IH have "v :\<sqsubseteq>val v3" by simp
      moreover
      have "flat v3 = flat v" using as1 Right(3)
@@ -625,10 +613,10 @@
      then show "Right v :\<sqsubseteq>val v2" unfolding Right .
   next
      case (Left v3)
-     have "v3 \<in> CPT r1 s" using Left(2,3) as2  
-       by (auto simp add: CPT_def prefix_list_def)
+     have "v3 \<in> CV r1 s" using Left(2,3) as2  
+       by (auto simp add: CV_def prefix_list_def)
      then have "flat v3 = flat v \<and> \<Turnstile> v3 : r1" using as1 Left(3)
-       by (simp add: Posix1(2) CPT_def) 
+       by (simp add: Posix1(2) CV_def) 
      then have "False" using as1 as2 Left
        by (auto simp add: Posix1(2) L_flat_Prf1 Prf_CPrf)
      then show "Right v :\<sqsubseteq>val v2" by simp
@@ -637,22 +625,22 @@
   case (Posix_SEQ s1 r1 v1 s2 r2 v2 v3)
   have "s1 \<in> r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" by fact+
   then have as1: "s1 = flat v1" "s2 = flat v2" by (simp_all add: Posix1(2))
-  have IH1: "\<And>v3. v3 \<in> CPT r1 s1 \<Longrightarrow> v1 :\<sqsubseteq>val v3" by fact
-  have IH2: "\<And>v3. v3 \<in> CPT r2 s2 \<Longrightarrow> v2 :\<sqsubseteq>val v3" by fact
+  have IH1: "\<And>v3. v3 \<in> CV r1 s1 \<Longrightarrow> v1 :\<sqsubseteq>val v3" by fact
+  have IH2: "\<And>v3. v3 \<in> CV r2 s2 \<Longrightarrow> v2 :\<sqsubseteq>val v3" by fact
   have cond: "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" by fact
-  have "v3 \<in> CPT (SEQ r1 r2) (s1 @ s2)" by fact
+  have "v3 \<in> CV (SEQ r1 r2) (s1 @ s2)" by fact
   then obtain v3a v3b where eqs:
     "v3 = Seq v3a v3b" "\<Turnstile> v3a : r1" "\<Turnstile> v3b : r2"
     "flat v3a @ flat v3b = s1 @ s2" 
-    by (force simp add: prefix_list_def CPT_def elim: CPrf.cases)
+    by (force simp add: prefix_list_def CV_def elim: CPrf.cases)
   with cond have "flat v3a \<sqsubseteq>pre s1" unfolding prefix_list_def
     by (smt L_flat_Prf1 Prf_CPrf append_eq_append_conv2 append_self_conv)
   then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat v3b = s2)" using eqs
     by (simp add: sprefix_list_def append_eq_conv_conj)
   then have q2: "v1 :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat v3b = s2)" 
     using PosOrd_spreI as1(1) eqs by blast
-  then have "v1 :\<sqsubset>val v3a \<or> (v3a \<in> CPT r1 s1 \<and> v3b \<in> CPT r2 s2)" using eqs(2,3)
-    by (auto simp add: CPT_def)
+  then have "v1 :\<sqsubset>val v3a \<or> (v3a \<in> CV r1 s1 \<and> v3b \<in> CV r2 s2)" using eqs(2,3)
+    by (auto simp add: CV_def)
   then have "v1 :\<sqsubset>val v3a \<or> (v1 :\<sqsubseteq>val v3a \<and> v2 :\<sqsubseteq>val v3b)" using IH1 IH2 by blast         
   then have "Seq v1 v2 :\<sqsubseteq>val Seq v3a v3b" using eqs q2 as1
     unfolding  PosOrd_ex_eq_def by (auto simp add: PosOrd_SeqI1 PosOrd_SeqI2) 
@@ -661,17 +649,17 @@
   case (Posix_STAR1 s1 r v s2 vs v3) 
   have "s1 \<in> r \<rightarrow> v" "s2 \<in> STAR r \<rightarrow> Stars vs" by fact+
   then have as1: "s1 = flat v" "s2 = flat (Stars vs)" by (auto dest: Posix1(2))
-  have IH1: "\<And>v3. v3 \<in> CPT r s1 \<Longrightarrow> v :\<sqsubseteq>val v3" by fact
-  have IH2: "\<And>v3. v3 \<in> CPT (STAR r) s2 \<Longrightarrow> Stars vs :\<sqsubseteq>val v3" by fact
+  have IH1: "\<And>v3. v3 \<in> CV r s1 \<Longrightarrow> v :\<sqsubseteq>val v3" by fact
+  have IH2: "\<And>v3. v3 \<in> CV (STAR r) s2 \<Longrightarrow> Stars vs :\<sqsubseteq>val v3" by fact
   have cond: "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))" by fact
   have cond2: "flat v \<noteq> []" by fact
-  have "v3 \<in> CPT (STAR r) (s1 @ s2)" by fact
+  have "v3 \<in> CV (STAR r) (s1 @ s2)" by fact
   then consider 
     (NonEmpty) v3a vs3 where "v3 = Stars (v3a # vs3)" 
     "\<Turnstile> v3a : r" "\<Turnstile> Stars vs3 : STAR r"
     "flat (Stars (v3a # vs3)) = s1 @ s2"
   | (Empty) "v3 = Stars []"
-  unfolding CPT_def
+  unfolding CV_def
   apply(auto)
   apply(erule CPrf.cases)
   apply(simp_all)
@@ -690,8 +678,8 @@
         by (simp add: sprefix_list_def append_eq_conv_conj)
       then have q2: "v :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" 
         using PosOrd_spreI as1(1) NonEmpty(4) by blast
-      then have "v :\<sqsubset>val v3a \<or> (v3a \<in> CPT r s1 \<and> Stars vs3 \<in> CPT (STAR r) s2)" 
-        using NonEmpty(2,3) by (auto simp add: CPT_def)
+      then have "v :\<sqsubset>val v3a \<or> (v3a \<in> CV r s1 \<and> Stars vs3 \<in> CV (STAR r) s2)" 
+        using NonEmpty(2,3) by (auto simp add: CV_def)
       then have "v :\<sqsubset>val v3a \<or> (v :\<sqsubseteq>val v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" using IH1 IH2 by blast
       then have "v :\<sqsubset>val v3a \<or> (v = v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" 
          unfolding PosOrd_ex_eq_def by auto     
@@ -708,58 +696,26 @@
     qed      
 next 
   case (Posix_STAR2 r v2)
-  have "v2 \<in> CPT (STAR r) []" by fact
+  have "v2 \<in> CV (STAR r) []" by fact
   then have "v2 = Stars []" 
-    unfolding CPT_def by (auto elim: CPrf.cases) 
+    unfolding CV_def by (auto elim: CPrf.cases) 
   then show "Stars [] :\<sqsubseteq>val v2"
   by (simp add: PosOrd_ex_eq_def)
 qed
 
-lemma Posix_PosOrd_stronger:
-  assumes "s \<in> r \<rightarrow> v1" "v2 \<in> CPTpre r s" 
-  shows "v1 :\<sqsubseteq>val v2"
-proof -
-  from assms(2) have "v2 \<in> CPT r s \<or> flat v2 \<sqsubset>spre s"
-  unfolding CPTpre_def CPT_def sprefix_list_def prefix_list_def by auto
-  moreover
-    { assume "v2 \<in> CPT r s" 
-      with assms(1) 
-      have "v1 :\<sqsubseteq>val v2" by (rule Posix_PosOrd)
-    }
-  moreover
-    { assume "flat v2 \<sqsubset>spre s"
-      then have "flat v2 \<sqsubset>spre flat v1" using assms(1)
-        using Posix1(2) by blast
-      then have "v1 :\<sqsubseteq>val v2"
-        by (simp add: PosOrd_ex_eq_def PosOrd_spreI) 
-    }
-  ultimately show "v1 :\<sqsubseteq>val v2" by blast
-qed
 
 lemma Posix_PosOrd_reverse:
   assumes "s \<in> r \<rightarrow> v1" 
-  shows "\<not>(\<exists>v2 \<in> CPTpre r s. v2 :\<sqsubset>val v1)"
+  shows "\<not>(\<exists>v2 \<in> CV r s. v2 :\<sqsubset>val v1)"
 using assms
-by (metis Posix_PosOrd_stronger less_irrefl PosOrd_def 
+by (metis Posix_PosOrd less_irrefl PosOrd_def 
     PosOrd_ex_eq_def PosOrd_ex_def PosOrd_trans)
 
 
-lemma test2: 
-  assumes "\<forall>v \<in> set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []"
-  shows "(Stars vs) \<in> CPT (STAR r) (flat (Stars vs))" 
-using assms
-apply(induct vs)
-apply(auto simp add: CPT_def)
-apply(rule CPrf.intros)
-apply(simp)
-apply(rule CPrf.intros)
-apply(simp_all)
-by (metis (no_types, lifting) CPT_def Posix_CPT mem_Collect_eq)
-
 
 lemma PosOrd_Posix_Stars:
   assumes "\<forall>v \<in> set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []"
-  and "\<not>(\<exists>vs2 \<in> PT (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val (Stars vs))"
+  and "\<not>(\<exists>vs2 \<in> LV (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val (Stars vs))"
   shows "(flat (Stars vs)) \<in> (STAR r) \<rightarrow> Stars vs" 
 using assms
 proof(induct vs)
@@ -769,24 +725,24 @@
 next
   case (Cons v vs)
   have IH: "\<lbrakk>\<forall>v\<in>set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []; 
-             \<not> (\<exists>vs2\<in>PT (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs)\<rbrakk>
+             \<not> (\<exists>vs2\<in>LV (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs)\<rbrakk>
              \<Longrightarrow> flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs" by fact
   have as2: "\<forall>v\<in>set (v # vs). flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" by fact
-  have as3: "\<not> (\<exists>vs2\<in>PT (STAR r) (flat (Stars (v # vs))). vs2 :\<sqsubset>val Stars (v # vs))" by fact
+  have as3: "\<not> (\<exists>vs2\<in>LV (STAR r) (flat (Stars (v # vs))). vs2 :\<sqsubset>val Stars (v # vs))" by fact
   have "flat v \<in> r \<rightarrow> v" using as2 by simp
   moreover
   have  "flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs" 
     proof (rule IH)
       show "\<forall>v\<in>set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" using as2 by simp
     next 
-      show "\<not> (\<exists>vs2\<in>PT (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs)" using as3
+      show "\<not> (\<exists>vs2\<in>LV (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs)" using as3
         apply(auto)
-        apply(subst (asm) (2) PT_def)
+        apply(subst (asm) (2) LV_def)
         apply(auto)
         apply(erule Prf.cases)
         apply(simp_all)
         apply(drule_tac x="Stars (v # vs)" in bspec)
-        apply(simp add: PT_def CPT_def)
+        apply(simp add: LV_def CV_def)
         using Posix_Prf Prf.intros(6) calculation
         apply(rule_tac Prf.intros)
         apply(simp add:)
@@ -810,7 +766,7 @@
    apply(simp_all)
    apply(clarify)
    apply(drule_tac x="Stars (va#vs)" in bspec)
-   apply(auto simp add: PT_def)[1]   
+   apply(auto simp add: LV_def)[1]   
    apply(rule Prf.intros)
    apply(simp)
    by (simp add: PosOrd_StarsI PosOrd_shorterI)
@@ -823,69 +779,69 @@
 section {* The Smallest Value is indeed the Posix Value *}
 
 text {*
-  The next lemma seems to require PT instead of CPT in the Star-case.
+  The next lemma seems to require LV instead of CV in the Star-case.
 *}
 
 lemma PosOrd_Posix:
-  assumes "v1 \<in> CPT r s" "\<forall>v\<^sub>2 \<in> PT r s. \<not> v\<^sub>2 :\<sqsubset>val v1"
+  assumes "v1 \<in> CV r s" "\<forall>v\<^sub>2 \<in> LV r s. \<not> v\<^sub>2 :\<sqsubset>val v1"
   shows "s \<in> r \<rightarrow> v1" 
 using assms
 proof(induct r arbitrary: s v1)
   case (ZERO s v1)
-  have "v1 \<in> CPT ZERO s" by fact
-  then show "s \<in> ZERO \<rightarrow> v1" unfolding CPT_def
+  have "v1 \<in> CV ZERO s" by fact
+  then show "s \<in> ZERO \<rightarrow> v1" unfolding CV_def
     by (auto elim: CPrf.cases)
 next 
   case (ONE s v1)
-  have "v1 \<in> CPT ONE s" by fact
-  then show "s \<in> ONE \<rightarrow> v1" unfolding CPT_def
+  have "v1 \<in> CV ONE s" by fact
+  then show "s \<in> ONE \<rightarrow> v1" unfolding CV_def
     by(auto elim!: CPrf.cases intro: Posix.intros)
 next 
   case (CHAR c s v1)
-  have "v1 \<in> CPT (CHAR c) s" by fact
-  then show "s \<in> CHAR c \<rightarrow> v1" unfolding CPT_def
+  have "v1 \<in> CV (CHAR c) s" by fact
+  then show "s \<in> CHAR c \<rightarrow> v1" unfolding CV_def
     by (auto elim!: CPrf.cases intro: Posix.intros)
 next
   case (ALT r1 r2 s v1)
-  have IH1: "\<And>s v1. \<lbrakk>v1 \<in> CPT r1 s; \<forall>v2 \<in> PT r1 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r1 \<rightarrow> v1" by fact
-  have IH2: "\<And>s v1. \<lbrakk>v1 \<in> CPT r2 s; \<forall>v2 \<in> PT r2 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r2 \<rightarrow> v1" by fact
-  have as1: "\<forall>v2\<in>PT (ALT r1 r2) s. \<not> v2 :\<sqsubset>val v1" by fact
-  have as2: "v1 \<in> CPT (ALT r1 r2) s" by fact
+  have IH1: "\<And>s v1. \<lbrakk>v1 \<in> CV r1 s; \<forall>v2 \<in> LV r1 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r1 \<rightarrow> v1" by fact
+  have IH2: "\<And>s v1. \<lbrakk>v1 \<in> CV r2 s; \<forall>v2 \<in> LV r2 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r2 \<rightarrow> v1" by fact
+  have as1: "\<forall>v2\<in>LV (ALT r1 r2) s. \<not> v2 :\<sqsubset>val v1" by fact
+  have as2: "v1 \<in> CV (ALT r1 r2) s" by fact
   then consider 
      (Left) v1' where
         "v1 = Left v1'" "s = flat v1'"
-        "v1' \<in> CPT r1 s"
+        "v1' \<in> CV r1 s"
   |  (Right) v1' where
         "v1 = Right v1'" "s = flat v1'"
-        "v1' \<in> CPT r2 s"
-  unfolding CPT_def by (auto elim: CPrf.cases)
+        "v1' \<in> CV r2 s"
+  unfolding CV_def by (auto elim: CPrf.cases)
   then show "s \<in> ALT r1 r2 \<rightarrow> v1"
    proof (cases)
      case (Left v1')
-     have "v1' \<in> CPT r1 s" using as2
-       unfolding CPT_def Left by (auto elim: CPrf.cases)
+     have "v1' \<in> CV r1 s" using as2
+       unfolding CV_def Left by (auto elim: CPrf.cases)
      moreover
-     have "\<forall>v2 \<in> PT r1 s. \<not> v2 :\<sqsubset>val v1'" using as1
-       unfolding PT_def Left using Prf.intros(2) PosOrd_Left_eq by force  
+     have "\<forall>v2 \<in> LV r1 s. \<not> v2 :\<sqsubset>val v1'" using as1
+       unfolding LV_def Left using Prf.intros(2) PosOrd_Left_eq by force  
      ultimately have "s \<in> r1 \<rightarrow> v1'" using IH1 by simp
      then have "s \<in> ALT r1 r2 \<rightarrow> Left v1'" by (rule Posix.intros)
      then show "s \<in> ALT r1 r2 \<rightarrow> v1" using Left by simp
    next
      case (Right v1')
-     have "v1' \<in> CPT r2 s" using as2
-       unfolding CPT_def Right by (auto elim: CPrf.cases)
+     have "v1' \<in> CV r2 s" using as2
+       unfolding CV_def Right by (auto elim: CPrf.cases)
      moreover
-     have "\<forall>v2 \<in> PT r2 s. \<not> v2 :\<sqsubset>val v1'" using as1
-       unfolding PT_def Right using Prf.intros(3) PosOrd_RightI by force   
+     have "\<forall>v2 \<in> LV r2 s. \<not> v2 :\<sqsubset>val v1'" using as1
+       unfolding LV_def Right using Prf.intros(3) PosOrd_RightI by force   
      ultimately have "s \<in> r2 \<rightarrow> v1'" using IH2 by simp
      moreover 
        { assume "s \<in> L r1"
-         then obtain v' where "v' \<in>  PT r1 s"
-            unfolding PT_def using L_flat_Prf2 by blast
-         then have "Left v' \<in>  PT (ALT r1 r2) s" 
-            unfolding PT_def by (auto intro: Prf.intros)
+         then obtain v' where "v' \<in>  LV r1 s"
+            unfolding LV_def using L_flat_Prf2 by blast
+         then have "Left v' \<in>  LV (ALT r1 r2) s" 
+            unfolding LV_def by (auto intro: Prf.intros)
          with as1 have "\<not> (Left v' :\<sqsubset>val Right v1') \<and> (flat v' = s)" 
-            unfolding PT_def Right by (auto)
+            unfolding LV_def Right by (auto)
          then have False using PosOrd_Left_Right Right by blast  
        }
      then have "s \<notin> L r1" by rule 
@@ -894,36 +850,36 @@
   qed
 next 
   case (SEQ r1 r2 s v1)
-  have IH1: "\<And>s v1. \<lbrakk>v1 \<in> CPT r1 s; \<forall>v2 \<in> PT r1 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r1 \<rightarrow> v1" by fact
-  have IH2: "\<And>s v1. \<lbrakk>v1 \<in> CPT r2 s; \<forall>v2 \<in> PT r2 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r2 \<rightarrow> v1" by fact
-  have as1: "\<forall>v2\<in>PT (SEQ r1 r2) s. \<not> v2 :\<sqsubset>val v1" by fact
-  have as2: "v1 \<in> CPT (SEQ r1 r2) s" by fact
+  have IH1: "\<And>s v1. \<lbrakk>v1 \<in> CV r1 s; \<forall>v2 \<in> LV r1 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r1 \<rightarrow> v1" by fact
+  have IH2: "\<And>s v1. \<lbrakk>v1 \<in> CV r2 s; \<forall>v2 \<in> LV r2 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r2 \<rightarrow> v1" by fact
+  have as1: "\<forall>v2\<in>LV (SEQ r1 r2) s. \<not> v2 :\<sqsubset>val v1" by fact
+  have as2: "v1 \<in> CV (SEQ r1 r2) s" by fact
   then obtain 
     v1a v1b where eqs:
         "v1 = Seq v1a v1b" "s = flat v1a @ flat v1b"
-        "v1a \<in> CPT r1 (flat v1a)" "v1b \<in> CPT r2 (flat v1b)" 
-  unfolding CPT_def by(auto elim: CPrf.cases)
-  have "\<forall>v2 \<in> PT r1 (flat v1a). \<not> v2 :\<sqsubset>val v1a"
+        "v1a \<in> CV r1 (flat v1a)" "v1b \<in> CV r2 (flat v1b)" 
+  unfolding CV_def by(auto elim: CPrf.cases)
+  have "\<forall>v2 \<in> LV r1 (flat v1a). \<not> v2 :\<sqsubset>val v1a"
     proof
       fix v2
-      assume "v2 \<in> PT r1 (flat v1a)"
-      with eqs(2,4) have "Seq v2 v1b \<in> PT (SEQ r1 r2) s"
-         by (simp add: CPT_def PT_def Prf.intros(1) Prf_CPrf)
+      assume "v2 \<in> LV r1 (flat v1a)"
+      with eqs(2,4) have "Seq v2 v1b \<in> LV (SEQ r1 r2) s"
+         by (simp add: CV_def LV_def Prf.intros(1) Prf_CPrf)
       with as1 have "\<not> Seq v2 v1b :\<sqsubset>val Seq v1a v1b \<and> flat (Seq v2 v1b) = flat (Seq v1a v1b)" 
-         using eqs by (simp add: PT_def) 
+         using eqs by (simp add: LV_def) 
       then show "\<not> v2 :\<sqsubset>val v1a"
          using PosOrd_SeqI1 by blast
     qed     
   then have "flat v1a \<in> r1 \<rightarrow> v1a" using IH1 eqs by simp
   moreover
-  have "\<forall>v2 \<in> PT r2 (flat v1b). \<not> v2 :\<sqsubset>val v1b"
+  have "\<forall>v2 \<in> LV r2 (flat v1b). \<not> v2 :\<sqsubset>val v1b"
     proof 
       fix v2
-      assume "v2 \<in> PT r2 (flat v1b)"
-      with eqs(2,3,4) have "Seq v1a v2 \<in> PT (SEQ r1 r2) s"
-         by (simp add: CPT_def PT_def Prf.intros Prf_CPrf)
+      assume "v2 \<in> LV r2 (flat v1b)"
+      with eqs(2,3,4) have "Seq v1a v2 \<in> LV (SEQ r1 r2) s"
+         by (simp add: CV_def LV_def Prf.intros Prf_CPrf)
       with as1 have "\<not> Seq v1a v2 :\<sqsubset>val Seq v1a v1b \<and> flat v2 = flat v1b" 
-         using eqs by (simp add: PT_def) 
+         using eqs by (simp add: LV_def) 
       then show "\<not> v2 :\<sqsubset>val v1b"
          using PosOrd_SeqI2 by auto
     qed     
@@ -935,8 +891,8 @@
      then obtain s3 s4 where q1: "s3 \<noteq> [] \<and> s3 @ s4 = flat v1b \<and> flat v1a @ s3 \<in> L r1 \<and> s4 \<in> L r2" by blast
      then obtain vA vB where q2: "flat vA = flat v1a @ s3" "\<turnstile> vA : r1" "flat vB = s4" "\<turnstile> vB : r2"
         using L_flat_Prf2 by blast
-     then have "Seq vA vB \<in> PT (SEQ r1 r2) s" unfolding eqs using q1
-       by (auto simp add: PT_def intro: Prf.intros)
+     then have "Seq vA vB \<in> LV (SEQ r1 r2) s" unfolding eqs using q1
+       by (auto simp add: LV_def intro: Prf.intros)
      with as1 have "\<not> Seq vA vB :\<sqsubset>val Seq v1a v1b" unfolding eqs by auto
      then have "\<not> vA :\<sqsubset>val v1a \<and> length (flat vA) > length (flat v1a)" using q1 q2 PosOrd_SeqI1 by auto 
      then show "False"
@@ -947,57 +903,57 @@
     by (rule Posix.intros)
 next
    case (STAR r s v1)
-   have IH: "\<And>s v1. \<lbrakk>v1 \<in> CPT r s; \<forall>v2\<in>PT r s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r \<rightarrow> v1" by fact
-   have as1: "\<forall>v2\<in>PT (STAR r) s. \<not> v2 :\<sqsubset>val v1" by fact
-   have as2: "v1 \<in> CPT (STAR r) s" by fact
+   have IH: "\<And>s v1. \<lbrakk>v1 \<in> CV r s; \<forall>v2\<in>LV r s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r \<rightarrow> v1" by fact
+   have as1: "\<forall>v2\<in>LV (STAR r) s. \<not> v2 :\<sqsubset>val v1" by fact
+   have as2: "v1 \<in> CV (STAR r) s" by fact
    then obtain 
     vs where eqs:
         "v1 = Stars vs" "s = flat (Stars vs)"
-        "\<forall>v \<in> set vs. v \<in> CPT r (flat v)"
-        unfolding CPT_def by (auto elim: CPrf.cases dest!: CPrf_stars)
+        "\<forall>v \<in> set vs. v \<in> CV r (flat v)"
+        unfolding CV_def by (auto elim: CPrf.cases)
    have "\<forall>v\<in>set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" 
      proof 
         fix v
         assume a: "v \<in> set vs"
         then obtain pre post where e: "vs = pre @ [v] @ post"
           by (metis append_Cons append_Nil in_set_conv_decomp_first)
-        then have q: "\<forall>v2\<in>PT (STAR r) s. \<not> v2 :\<sqsubset>val Stars (pre @ [v] @ post)" 
+        then have q: "\<forall>v2\<in>LV (STAR r) s. \<not> v2 :\<sqsubset>val Stars (pre @ [v] @ post)" 
           using as1 unfolding eqs by simp
-        have "\<forall>v2\<in>PT r (flat v). \<not> v2 :\<sqsubset>val v" unfolding eqs 
+        have "\<forall>v2\<in>LV r (flat v). \<not> v2 :\<sqsubset>val v" unfolding eqs 
           proof (rule ballI, rule notI) 
              fix v2
              assume w: "v2 :\<sqsubset>val v"
-             assume "v2 \<in> PT r (flat v)"
-             then have "Stars (pre @ [v2] @ post) \<in> PT (STAR r) s" 
+             assume "v2 \<in> LV r (flat v)"
+             then have "Stars (pre @ [v2] @ post) \<in> LV (STAR r) s" 
                  using as2 unfolding e eqs
-                 apply(auto simp add: CPT_def PT_def intro!: Prf.intros)[1]
-                 using CPrf_Stars_appendE CPrf_stars Prf_CPrf apply blast
-                 by (meson CPrf_Stars_appendE CPrf_stars Prf_CPrf list.set_intros(2))
+                 apply(auto simp add: CV_def LV_def intro!: Prf.intros)[1]
+                 using CPrf_Stars_appendE Prf_CPrf Prf_elims(6) list.set_intros apply blast
+                 by (metis CPrf_Stars_appendE Prf_CPrf Prf_elims(6) list.set_intros(2) val.inject(5))
              then have  "\<not> Stars (pre @ [v2] @ post) :\<sqsubset>val Stars (pre @ [v] @ post)"
                 using q by simp     
              with w show "False"
-                using PT_def \<open>v2 \<in> PT r (flat v)\<close> append_Cons flat.simps(7) mem_Collect_eq 
+                using LV_def \<open>v2 \<in> LV r (flat v)\<close> append_Cons flat.simps(7) mem_Collect_eq 
                 PosOrd_StarsI PosOrd_Stars_appendI by auto
           qed     
         with IH
-        show "flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" using a as2 unfolding eqs
-          using eqs(3) by (smt CPT_def CPrf_stars mem_Collect_eq) 
+        show "flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" using a as2 unfolding eqs CV_def
+        by (auto elim: CPrf.cases)
      qed
    moreover
-   have "\<not> (\<exists>vs2\<in>PT (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs)" 
+   have "\<not> (\<exists>vs2\<in>LV (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs)" 
      proof 
-       assume "\<exists>vs2 \<in> PT (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs"
+       assume "\<exists>vs2 \<in> LV (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs"
        then obtain vs2 where "\<turnstile> Stars vs2 : STAR r" "flat (Stars vs2) = flat (Stars vs)"
                              "Stars vs2 :\<sqsubset>val Stars vs" 
-         unfolding PT_def
-         apply(auto elim: Prf.cases)
+         unfolding LV_def
+         apply(auto)
          apply(erule Prf.cases)
          apply(auto intro: Prf.intros)
          done
        then show "False" using as1 unfolding eqs
          apply -
          apply(drule_tac x="Stars vs2" in bspec)
-         apply(auto simp add: PT_def)
+         apply(auto simp add: LV_def)
          done
      qed
    ultimately have "flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs"
diff -r fff2e1b40dfc -r 32b222d77fa0 thys/Spec.thy
--- a/thys/Spec.thy	Wed Jul 19 14:55:46 2017 +0100
+++ b/thys/Spec.thy	Fri Aug 11 20:29:01 2017 +0100
@@ -1,9 +1,8 @@
    
 theory Spec
-  imports Main 
+  imports Main "~~/src/HOL/Library/Sublist"
 begin
 
-
 section {* Sequential Composition of Languages *}
 
 definition
@@ -172,13 +171,15 @@
 
 lemma ders_correctness:
   shows "L (ders s r) = Ders s (L r)"
-apply(induct s arbitrary: r)
-apply(simp_all add: Ders_def der_correctness Der_def)
-done
+by (induct s arbitrary: r)
+   (simp_all add: Ders_def der_correctness Der_def)
+
 
 
 section {* Lemmas about ders *}
 
+(* not really needed *)
+
 lemma ders_ZERO:
   shows "ders s (ZERO) = ZERO"
 apply(induct s)
@@ -201,9 +202,8 @@
 
 lemma  ders_ALT:
   shows "ders s (ALT r1 r2) = ALT (ders s r1) (ders s r2)"
-apply(induct s arbitrary: r1 r2)
-apply(simp_all)
-done
+by (induct s arbitrary: r1 r2)(simp_all)
+
 
 section {* Values *}
 
@@ -229,8 +229,11 @@
 | "flat (Stars []) = []"
 | "flat (Stars (v#vs)) = (flat v) @ (flat (Stars vs))" 
 
+abbreviation
+  "flats vs \<equiv> concat (map flat vs)"
+
 lemma flat_Stars [simp]:
- "flat (Stars vs) = concat (map flat vs)"
+ "flat (Stars vs) = flats vs"
 by (induct vs) (auto)
 
 
@@ -273,7 +276,7 @@
 
 lemma Star_val:
   assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<turnstile> v : r"
-  shows "\<exists>vs. concat (map flat vs) = concat ss \<and> (\<forall>v\<in>set vs. \<turnstile> v : r)"
+  shows "\<exists>vs. flats vs = concat ss \<and> (\<forall>v\<in>set vs. \<turnstile> v : r)"
 using assms
 apply(induct ss)
 apply(auto)
@@ -313,7 +316,7 @@
   have "s \<in> L (STAR r)" by fact
   then obtain ss where "concat ss = s" "\<forall>s \<in> set ss. s \<in> L r"
   using Star_string by auto
-  then obtain vs where "concat (map flat vs) = s" "\<forall>v\<in>set vs. \<turnstile> v : r"
+  then obtain vs where "flats vs = s" "\<forall>v\<in>set vs. \<turnstile> v : r"
   using IH Star_val by blast
   then show "\<exists>v. \<turnstile> v : STAR r \<and> flat v = s"
   using Prf.intros(6) flat_Stars by blast
@@ -331,8 +334,8 @@
   shows "L(r) = {flat v | v. \<turnstile> v : r}"
 using L_flat_Prf1 L_flat_Prf2 by blast
 
-section {* CPT and CPTpre *}
 
+section {* Canonical Values *}
 
 inductive 
   CPrf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<Turnstile> _ : _" [100, 100] 100)
@@ -350,71 +353,153 @@
 using assms
 by (induct)(auto intro: Prf.intros)
 
-lemma CPrf_stars:
-  assumes "\<Turnstile> Stars vs : STAR r"
-  shows "\<forall>v \<in> set vs. flat v \<noteq> [] \<and> \<Turnstile> v : r"
-using assms
-apply(erule_tac CPrf.cases)
-apply(simp_all)
-done
-
 lemma CPrf_Stars_appendE:
   assumes "\<Turnstile> Stars (vs1 @ vs2) : STAR r"
   shows "\<Turnstile> Stars vs1 : STAR r \<and> \<Turnstile> Stars vs2 : STAR r" 
 using assms
 apply(erule_tac CPrf.cases)
-apply(auto intro: CPrf.intros elim: Prf.cases)
+apply(auto intro: CPrf.intros)
 done
 
-definition PT :: "rexp \<Rightarrow> string \<Rightarrow> val set"
-where "PT r s \<equiv> {v. flat v = s \<and> \<turnstile> v : r}"
+
+section {* Sets of Lexical and Canonical Values *}
 
-definition
-  "CPT r s = {v. flat v = s \<and> \<Turnstile> v : r}"
+definition 
+  LV :: "rexp \<Rightarrow> string \<Rightarrow> val set"
+where "LV r s \<equiv> {v.  \<turnstile> v : r \<and> flat v = s}"
 
 definition
-  "CPTpre r s = {v. \<exists>s'. flat v @ s' = s \<and> \<Turnstile> v : r}"
+  CV :: "rexp \<Rightarrow> string \<Rightarrow> val set"
+where  "CV r s \<equiv> {v. \<Turnstile> v : r \<and> flat v = s}"
+
+lemma LV_CV_subset:
+  shows "CV r s \<subseteq> LV r s"
+unfolding CV_def LV_def by(auto simp add: Prf_CPrf)
+
+abbreviation
+  "Prefixes s \<equiv> {s'. prefixeq s' s}"
+
+abbreviation
+  "Suffixes s \<equiv> {s'. suffixeq s' s}"
+
+abbreviation
+  "SSuffixes s \<equiv> {s'. suffix s' s}"
 
-lemma CPT_CPTpre_subset:
-  shows "CPT r s \<subseteq> CPTpre r s"
-by(auto simp add: CPT_def CPTpre_def)
+lemma Suffixes_cons [simp]:
+  shows "Suffixes (c # s) = Suffixes s \<union> {c # s}"
+by (auto simp add: suffixeq_def Cons_eq_append_conv)
+
+lemma CV_simps:
+  shows "CV ZERO s = {}"
+  and   "CV ONE s = (if s = [] then {Void} else {})"
+  and   "CV (CHAR c) s = (if s = [c] then {Char c} else {})"
+  and   "CV (ALT r1 r2) s = Left ` CV r1 s \<union> Right ` CV r2 s"
+unfolding CV_def
+by (auto intro: CPrf.intros elim: CPrf.cases)
+
+lemma finite_Suffixes: 
+  shows "finite (Suffixes s)"
+by (induct s) (simp_all)
 
-lemma CPT_simps:
-  shows "CPT ZERO s = {}"
-  and   "CPT ONE s = (if s = [] then {Void} else {})"
-  and   "CPT (CHAR c) s = (if s = [c] then {Char c} else {})"
-  and   "CPT (ALT r1 r2) s = Left ` CPT r1 s \<union> Right ` CPT r2 s"
-  and   "CPT (SEQ r1 r2) s = 
-          {Seq v1 v2 | v1 v2. flat v1 @ flat v2 = s \<and> v1 \<in> CPT r1 (flat v1) \<and> v2 \<in> CPT r2 (flat v2)}"
-  and   "CPT (STAR r) s = 
-          Stars ` {vs. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. v \<in> CPT r (flat v) \<and> flat v \<noteq> [])}"
-apply -
-apply(auto simp add: CPT_def intro: CPrf.intros)[1]
+lemma finite_SSuffixes: 
+  shows "finite (SSuffixes s)"
+proof -
+  have "SSuffixes s \<subseteq> Suffixes s"
+   unfolding suffix_def suffixeq_def by auto
+  then show "finite (SSuffixes s)"
+   using finite_Suffixes finite_subset by blast
+qed
+
+lemma finite_Prefixes: 
+  shows "finite (Prefixes s)"
+proof -
+  have "finite (Suffixes (rev s))" 
+    by (rule finite_Suffixes)
+  then have "finite (rev ` Suffixes (rev s))" by simp
+  moreover
+  have "rev ` (Suffixes (rev s)) = Prefixes s"
+  unfolding suffixeq_def prefixeq_def image_def
+   by (auto)(metis rev_append rev_rev_ident)+
+  ultimately show "finite (Prefixes s)" by simp
+qed
+
+lemma CV_SEQ_subset:
+  "CV (SEQ r1 r2) s \<subseteq> (\<lambda>(v1,v2). Seq v1 v2) ` ((\<Union>s' \<in> Prefixes s. CV r1 s') \<times> (\<Union>s' \<in> Suffixes s. CV r2 s'))"
+unfolding image_def CV_def prefixeq_def suffixeq_def
+by (auto elim: CPrf.cases)
+
+lemma CV_STAR_subset:
+  "CV (STAR r) s \<subseteq> {Stars []} \<union>
+      (\<lambda>(v,vs). Stars (v#vs)) ` ((\<Union>s' \<in> Prefixes s. CV r s') \<times> (\<Union>s2 \<in> SSuffixes s. Stars -` (CV (STAR r) s2)))"
+unfolding image_def CV_def prefixeq_def suffix_def
+apply(auto)
 apply(erule CPrf.cases)
-apply(simp_all)[6]
-apply(auto simp add: CPT_def intro: CPrf.intros)[1]
-apply(erule CPrf.cases)
-apply(simp_all)[6]
-apply(erule CPrf.cases)
-apply(simp_all)[6]
-apply(auto simp add: CPT_def intro: CPrf.intros)[1]
-apply(erule CPrf.cases)
-apply(simp_all)[6]
-apply(erule CPrf.cases)
-apply(simp_all)[6]
-apply(auto simp add: CPT_def intro: CPrf.intros)[1]
-apply(erule CPrf.cases)
-apply(simp_all)[6]
-apply(auto simp add: CPT_def intro: CPrf.intros)[1]
-apply(erule CPrf.cases)
-apply(simp_all)[6]
-(* STAR case *)
-apply(auto simp add: CPT_def intro: CPrf.intros)[1]
-apply(erule CPrf.cases)
-apply(simp_all)[6]
+apply(auto)
+apply(case_tac vs)
+apply(auto intro: CPrf.intros)
 done
 
 
+lemma CV_STAR_finite:
+  assumes "\<forall>s. finite (CV r s)"
+  shows "finite (CV (STAR r) s)"
+proof(induct s rule: length_induct)
+  fix s::"char list"
+  assume "\<forall>s'. length s' < length s \<longrightarrow> finite (CV (STAR r) s')"
+  then have IH: "\<forall>s' \<in> SSuffixes s. finite (CV (STAR r) s')"
+    by (auto simp add: suffix_def) 
+  def f \<equiv> "\<lambda>(v, vs). Stars (v # vs)"
+  def S1 \<equiv> "\<Union>s' \<in> Prefixes s. CV r s'"
+  def S2 \<equiv> "\<Union>s2 \<in> SSuffixes s. Stars -` (CV (STAR r) s2)"
+  have "finite S1" using assms
+    unfolding S1_def by (simp_all add: finite_Prefixes)
+  moreover 
+  with IH have "finite S2" unfolding S2_def
+    by (auto simp add: finite_SSuffixes inj_on_def finite_vimageI)
+  ultimately 
+  have "finite ({Stars []} \<union> f ` (S1 \<times> S2))" by simp
+  moreover 
+  have "CV (STAR r) s \<subseteq> {Stars []} \<union> f ` (S1 \<times> S2)" unfolding S1_def S2_def f_def
+     by (rule CV_STAR_subset)
+  ultimately
+  show "finite (CV (STAR r) s)" by (simp add: finite_subset)
+qed  
+    
+
+lemma CV_finite:
+  shows "finite (CV r s)"
+proof(induct r arbitrary: s)
+  case (ZERO s) 
+  show "finite (CV ZERO s)" by (simp add: CV_simps)
+next
+  case (ONE s)
+  show "finite (CV ONE s)" by (simp add: CV_simps)
+next
+  case (CHAR c s)
+  show "finite (CV (CHAR c) s)" by (simp add: CV_simps)
+next 
+  case (ALT r1 r2 s)
+  then show "finite (CV (ALT r1 r2) s)" by (simp add: CV_simps)
+next 
+  case (SEQ r1 r2 s)
+  def f \<equiv> "\<lambda>(v1, v2). Seq v1 v2"
+  def S1 \<equiv> "\<Union>s' \<in> Prefixes s. CV r1 s'"
+  def S2 \<equiv> "\<Union>s' \<in> Suffixes s. CV r2 s'"
+  have IHs: "\<And>s. finite (CV r1 s)" "\<And>s. finite (CV r2 s)" by fact+
+  then have "finite S1" "finite S2" unfolding S1_def S2_def
+    by (simp_all add: finite_Prefixes finite_Suffixes)
+  moreover
+  have "CV (SEQ r1 r2) s \<subseteq> f ` (S1 \<times> S2)"
+    unfolding f_def S1_def S2_def by (auto simp add: CV_SEQ_subset)
+  ultimately 
+  show "finite (CV (SEQ r1 r2) s)"
+    by (simp add: finite_subset)
+next
+  case (STAR r s)
+  then show "finite (CV (STAR r) s)" by (simp add: CV_STAR_finite)
+qed
+
+
 
 section {* Our POSIX Definition *}
 
@@ -531,12 +616,12 @@
   Our POSIX value is a canonical value.
 *}
 
-lemma Posix_CPT:
+lemma Posix_CV:
   assumes "s \<in> r \<rightarrow> v"
-  shows "v \<in> CPT r s"
+  shows "v \<in> CV r s"
 using assms
 apply(induct rule: Posix.induct)
-apply(auto simp add: CPT_def intro: CPrf.intros elim: CPrf.cases)
+apply(auto simp add: CV_def intro: CPrf.intros elim: CPrf.cases)
 apply(rotate_tac 5)
 apply(erule CPrf.cases)
 apply(simp_all)
@@ -544,203 +629,17 @@
 apply(simp_all)
 done
 
-
-
-(*
-lemma CPTpre_STAR_finite:
-  assumes "\<And>s. finite (CPT r s)"
-  shows "finite (CPT (STAR r) s)"
-apply(induct s rule: length_induct)
-apply(case_tac xs)
-apply(simp)
-apply(simp add: CPT_simps)
-apply(auto)
-apply(rule finite_imageI)
-using assms
-thm finite_Un
-prefer 2
-apply(simp add: CPT_simps)
-apply(rule finite_imageI)
-apply(rule finite_subset)
-apply(rule CPTpre_subsets)
-apply(simp)
-apply(rule_tac B="(\<lambda>(v, vs). Stars (v#vs)) ` {(v, vs). v \<in> CPTpre r (a#list) \<and> flat v \<noteq> [] \<and> Stars vs \<in> CPTpre (STAR r) (drop (length (flat v)) (a#list))}" in finite_subset)
-apply(auto)[1]
-apply(rule finite_imageI)
-apply(simp add: Collect_case_prod_Sigma)
-apply(rule finite_SigmaI)
-apply(rule assms)
-apply(case_tac "flat v = []")
-apply(simp)
-apply(drule_tac x="drop (length (flat v)) (a # list)" in spec)
-apply(simp)
-apply(auto)[1]
-apply(rule test)
-apply(simp)
-done
-
-lemma CPTpre_subsets:
-  "CPTpre ZERO s = {}"
-  "CPTpre ONE s \<subseteq> {Void}"
-  "CPTpre (CHAR c) s \<subseteq> {Char c}"
-  "CPTpre (ALT r1 r2) s \<subseteq> Left ` CPTpre r1 s \<union> Right ` CPTpre r2 s"
-  "CPTpre (SEQ r1 r2) s \<subseteq> {Seq v1 v2 | v1 v2. v1 \<in> CPTpre r1 s \<and> v2 \<in> CPTpre r2 (drop (length (flat v1)) s)}"
-  "CPTpre (STAR r) s \<subseteq> {Stars []} \<union>
-    {Stars (v#vs) | v vs. v \<in> CPTpre r s \<and> flat v \<noteq> [] \<and> Stars vs \<in> CPTpre (STAR r) (drop (length (flat v)) s)}"
-  "CPTpre (STAR r) [] = {Stars []}"
-apply(auto simp add: CPTpre_def)
-apply(erule CPrf.cases)
-apply(simp_all)
-apply(erule CPrf.cases)
-apply(simp_all)
-apply(erule CPrf.cases)
-apply(simp_all)
-apply(erule CPrf.cases)
-apply(simp_all)
-apply(erule CPrf.cases)
-apply(simp_all)
-
-apply(erule CPrf.cases)
-apply(simp_all)
-apply(erule CPrf.cases)
-apply(simp_all)
-apply(rule CPrf.intros)
-done
-
-
-lemma CPTpre_simps:
-  shows "CPTpre ONE s = {Void}"
-  and   "CPTpre (CHAR c) (d#s) = (if c = d then {Char c} else {})"
-  and   "CPTpre (ALT r1 r2) s = Left ` CPTpre r1 s \<union> Right ` CPTpre r2 s"
-  and   "CPTpre (SEQ r1 r2) s = 
-          {Seq v1 v2 | v1 v2. v1 \<in> CPTpre r1 s \<and> v2 \<in> CPTpre r2 (drop (length (flat v1)) s)}"
-apply -
-apply(rule subset_antisym)
-apply(rule CPTpre_subsets)
-apply(auto simp add: CPTpre_def intro: "CPrf.intros")[1]
-apply(case_tac "c = d")
-apply(simp)
-apply(rule subset_antisym)
-apply(rule CPTpre_subsets)
-apply(auto simp add: CPTpre_def intro: CPrf.intros)[1]
-apply(simp)
-apply(auto simp add: CPTpre_def intro: CPrf.intros)[1]
-apply(erule CPrf.cases)
-apply(simp_all)
-apply(rule subset_antisym)
-apply(rule CPTpre_subsets)
-apply(auto simp add: CPTpre_def intro: CPrf.intros)[1]
-apply(rule subset_antisym)
-apply(rule CPTpre_subsets)
-apply(auto simp add: CPTpre_def intro: CPrf.intros)[1]
-done
-
-lemma CPT_simps:
-  shows "CPT ONE s = (if s = [] then {Void} else {})"
-  and   "CPT (CHAR c) [d] = (if c = d then {Char c} else {})"
-  and   "CPT (ALT r1 r2) s = Left ` CPT r1 s \<union> Right ` CPT r2 s"
-  and   "CPT (SEQ r1 r2) s = 
-          {Seq v1 v2 | v1 v2 s1 s2. s1 @ s2 = s \<and> v1 \<in> CPT r1 s1 \<and> v2 \<in> CPT r2 s2}"
-apply -
-apply(rule subset_antisym)
-apply(auto simp add: CPT_def)[1]
-apply(erule CPrf.cases)
-apply(simp_all)[7]
-apply(erule CPrf.cases)
-apply(simp_all)[7]
-apply(auto simp add: CPT_def intro: CPrf.intros)[1]
-apply(auto simp add: CPT_def intro: CPrf.intros)[1]
-apply(erule CPrf.cases)
-apply(simp_all)[7]
-apply(erule CPrf.cases)
-apply(simp_all)[7]
-apply(auto simp add: CPT_def image_def intro: CPrf.intros)[1]
-apply(erule CPrf.cases)
-apply(simp_all)[7]
-apply(clarify)
-apply blast
-apply(auto simp add: CPT_def image_def intro: CPrf.intros)[1]
-apply(erule CPrf.cases)
-apply(simp_all)[7]
-done
-
-lemma test: 
-  assumes "finite A"
-  shows "finite {vs. Stars vs \<in> A}"
-using assms
-apply(induct A)
-apply(simp)
-apply(auto)
-apply(case_tac x)
-apply(simp_all)
-done
-
-lemma CPTpre_STAR_finite:
-  assumes "\<And>s. finite (CPTpre r s)"
-  shows "finite (CPTpre (STAR r) s)"
-apply(induct s rule: length_induct)
-apply(case_tac xs)
-apply(simp)
-apply(simp add: CPTpre_subsets)
-apply(rule finite_subset)
-apply(rule CPTpre_subsets)
-apply(simp)
-apply(rule_tac B="(\<lambda>(v, vs). Stars (v#vs)) ` {(v, vs). v \<in> CPTpre r (a#list) \<and> flat v \<noteq> [] \<and> Stars vs \<in> CPTpre (STAR r) (drop (length (flat v)) (a#list))}" in finite_subset)
-apply(auto)[1]
-apply(rule finite_imageI)
-apply(simp add: Collect_case_prod_Sigma)
-apply(rule finite_SigmaI)
-apply(rule assms)
-apply(case_tac "flat v = []")
-apply(simp)
-apply(drule_tac x="drop (length (flat v)) (a # list)" in spec)
-apply(simp)
-apply(auto)[1]
-apply(rule test)
-apply(simp)
-done
-
-lemma CPTpre_finite:
-  shows "finite (CPTpre r s)"
-apply(induct r arbitrary: s)
-apply(simp add: CPTpre_subsets)
-apply(rule finite_subset)
-apply(rule CPTpre_subsets)
-apply(simp)
-apply(rule finite_subset)
-apply(rule CPTpre_subsets)
-apply(simp)
-apply(rule finite_subset)
-apply(rule CPTpre_subsets)
-apply(rule_tac B="(\<lambda>(v1, v2). Seq v1 v2) ` {(v1, v2).  v1 \<in> CPTpre r1 s \<and> v2 \<in> CPTpre r2 (drop (length (flat v1)) s)}" in finite_subset)
-apply(auto)[1]
-apply(rule finite_imageI)
-apply(simp add: Collect_case_prod_Sigma)
-apply(rule finite_subset)
-apply(rule CPTpre_subsets)
-apply(simp)
-by (simp add: CPTpre_STAR_finite)
-
-
-lemma CPT_finite:
-  shows "finite (CPT r s)"
-apply(rule finite_subset)
-apply(rule CPT_CPTpre_subset)
-apply(rule CPTpre_finite)
-done
-*)
-
 lemma test2: 
   assumes "\<forall>v \<in> set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []"
-  shows "(Stars vs) \<in> CPT (STAR r) (flat (Stars vs))" 
+  shows "(Stars vs) \<in> CV (STAR r) (flat (Stars vs))" 
 using assms
 apply(induct vs)
-apply(auto simp add: CPT_def)
+apply(auto simp add: CV_def)
 apply(rule CPrf.intros)
 apply(simp)
 apply(rule CPrf.intros)
 apply(simp_all)
-by (metis (no_types, lifting) CPT_def Posix_CPT mem_Collect_eq)
+by (metis (no_types, lifting) CV_def Posix_CV mem_Collect_eq)
 
 
 end
\ No newline at end of file