--- a/IsaMakefile Mon Jan 31 12:54:31 2011 +0000
+++ b/IsaMakefile Mon Jan 31 14:51:47 2011 +0000
@@ -32,7 +32,7 @@
session2: tphols-2011/ROOT.ML \
tphols-2011/document/root* \
*.thy
- @$(USEDIR) -D generated -f ROOT.ML HOL tphols-2011
+ @$(USEDIR) -D generated -f ROOT.ML ListP tphols-2011
paper: session2
rm -f tphols-2011/generated/*.aux # otherwise latex will fall over
--- a/Myhill.thy Mon Jan 31 12:54:31 2011 +0000
+++ b/Myhill.thy Mon Jan 31 14:51:47 2011 +0000
@@ -18,19 +18,27 @@
"x \<approx>Lang y \<equiv> (x, y) \<in> (\<approx>Lang)"
text {*
- The basic idea to show the finiteness of the partition induced by relation @{text "\<approx>Lang"}
- is to attach a tag @{text "tag(x)"} to every string @{text "x"}, the set of tags are carfully
- choosen, so that the range of tagging function @{text "tag"} (denoted @{text "range(tag)"}) is finite.
- If strings with the same tag are equivlent with respect @{text "\<approx>Lang"},
- i.e. @{text "tag(x) = tag(y) \<Longrightarrow> x \<approx>Lang y"} (this property is named `injectivity' in the following),
- then it can be proved that: the partition given rise by @{text "(\<approx>Lang)"} is finite.
-
- There are two arguments for this. The first goes as the following:
+ The main lemma (@{text "rexp_imp_finite"}) is proved by a structural induction over regular expressions.
+ While base cases (cases for @{const "NULL"}, @{const "EMPTY"}, @{const "CHAR"}) are quite straight forward,
+ the inductive cases are rather involved. What we have when starting to prove these inductive caes is that
+ the partitions induced by the componet language are finite. The basic idea to show the finiteness of the
+ partition induced by the composite language is to attach a tag @{text "tag(x)"} to every string
+ @{text "x"}. The tags are made of equivalent classes from the component partitions. Let @{text "tag"}
+ be the tagging function and @{text "Lang"} be the composite language, it can be proved that
+ if strings with the same tag are equivalent with respect to @{text "Lang"}, expressed as:
+ \[
+ @{text "tag(x) = tag(y) \<Longrightarrow> x \<approx>Lang y"}
+ \]
+ then the partition induced by @{text "Lang"} must be finite. There are two arguments for this.
+ The first goes as the following:
\begin{enumerate}
\item First, the tagging function @{text "tag"} induces an equivalent relation @{text "(=tag=)"}
(defiintion of @{text "f_eq_rel"} and lemma @{text "equiv_f_eq_rel"}).
- \item It is shown that: if the range of @{text "tag"} is finite,
+ \item It is shown that: if the range of @{text "tag"} (denoted @{text "range(tag)"}) is finite,
the partition given rise by @{text "(=tag=)"} is finite (lemma @{text "finite_eq_f_rel"}).
+ Since tags are made from equivalent classes from component partitions, and the inductive
+ hypothesis ensures the finiteness of these partitions, it is not difficult to prove
+ the finiteness of @{text "range(tag)"}.
\item It is proved that if equivalent relation @{text "R1"} is more refined than @{text "R2"}
(expressed as @{text "R1 \<subseteq> R2"}),
and the partition induced by @{text "R1"} is finite, then the partition induced by @{text "R2"}
@@ -117,7 +125,8 @@
next
from eq2
show " ?f ` A // R2 \<subseteq> Pow ?B"
- apply (unfold image_def Pow_def quotient_def, auto)
+ unfolding image_def Pow_def quotient_def
+ apply auto
by (rule_tac x = xb in bexI, simp,
unfold equiv_def sym_def refl_on_def, blast)
qed
@@ -132,7 +141,7 @@
fix x
assume "X = R2 `` {x}" and "x \<in> A" with eq2
have x_in: "x \<in> X"
- by (unfold equiv_def quotient_def refl_on_def, auto)
+ unfolding equiv_def quotient_def refl_on_def by auto
with eq_f have "R1 `` {x} \<in> ?R" by auto
then obtain y where
y_in: "y \<in> Y" and eq_r: "R1 `` {x} = R1 ``{y}" by auto
@@ -140,7 +149,7 @@
proof -
from x_in X_in y_in Y_in eq2
have "x \<in> A" and "y \<in> A"
- by (unfold equiv_def quotient_def refl_on_def, auto)
+ unfolding equiv_def quotient_def refl_on_def by auto
from eq_equiv_class_iff [OF eq1 this] and eq_r
show ?thesis by simp
qed
@@ -154,7 +163,7 @@
qed
lemma equiv_lang_eq: "equiv UNIV (\<approx>Lang)"
- apply (unfold equiv_def str_eq_rel_def sym_def refl_on_def trans_def)
+ unfolding equiv_def str_eq_rel_def sym_def refl_on_def trans_def
by blast
lemma tag_finite_imageD:
@@ -245,7 +254,32 @@
subsection {* The proof*}
-subsubsection {* The case for @{const "NULL"} *}
+text {*
+ Each case is given in a separate section, as well as the final main lemma. Detailed explainations accompanied by
+ illustrations are given for non-trivial cases.
+
+
+ For ever inductive case, there are two tasks, the easier one is to show the range finiteness of
+ of the tagging function based on the finiteness of component partitions, the
+ difficult one is to show that strings with the same tag are equivalent with respect to the
+ composite language. Suppose the composite language be @{text "Lang"}, tagging function be
+ @{text "tag"}, it amounts to show:
+ \[
+ @{text "tag(x) = tag(y) \<Longrightarrow> x \<approx>Lang y"}
+ \]
+ expanding the definition of @{text "\<approx>Lang"}, it amounts to show:
+ \[
+ @{text "tag(x) = tag(y) \<Longrightarrow> (\<forall> z. x@z \<in> Lang \<longleftrightarrow> y@z \<in> Lang)"}
+ \]
+ Because the assumed tag equlity @{text "tag(x) = tag(y)"} is symmetric,
+ it is suffcient to show just one direction:
+ \[
+ @{text "\<And> x y z. \<lbrakk>tag(x) = tag(y); x@z \<in> Lang\<rbrakk> \<Longrightarrow> y@z \<in> Lang"}
+ \]
+ This is the pattern followed by every inductive case.
+ *}
+
+subsubsection {* The base case for @{const "NULL"} *}
lemma quot_null_eq:
shows "(UNIV // \<approx>{}) = ({UNIV}::lang set)"
@@ -256,7 +290,7 @@
unfolding quot_null_eq by simp
-subsubsection {* The case for @{const "EMPTY"} *}
+subsubsection {* The base case for @{const "EMPTY"} *}
lemma quot_empty_subset:
@@ -283,7 +317,7 @@
by (rule finite_subset[OF quot_empty_subset]) (simp)
-subsubsection {* The case for @{const "CHAR"} *}
+subsubsection {* The base case for @{const "CHAR"} *}
lemma quot_char_subset:
"UNIV // (\<approx>{[c]}) \<subseteq> {{[]},{[c]}, UNIV - {[], [c]}}"
@@ -315,110 +349,13 @@
by (rule finite_subset[OF quot_char_subset]) (simp)
-
-subsubsection {* The case for @{text "SEQ"}*}
-
-definition
- tag_str_SEQ :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang set)"
-where
- "tag_str_SEQ L1 L2 =
- (\<lambda>x. (\<approx>L1 `` {x}, {(\<approx>L2 `` {x - xa}) | xa. xa \<le> x \<and> xa \<in> L1}))"
-
-
-lemma append_seq_elim:
- assumes "x @ y \<in> L\<^isub>1 ;; L\<^isub>2"
- shows "(\<exists> xa \<le> x. xa \<in> L\<^isub>1 \<and> (x - xa) @ y \<in> L\<^isub>2) \<or>
- (\<exists> ya \<le> y. (x @ ya) \<in> L\<^isub>1 \<and> (y - ya) \<in> L\<^isub>2)"
-proof-
- from assms obtain s\<^isub>1 s\<^isub>2
- where "x @ y = s\<^isub>1 @ s\<^isub>2"
- and in_seq: "s\<^isub>1 \<in> L\<^isub>1 \<and> s\<^isub>2 \<in> L\<^isub>2"
- by (auto simp:Seq_def)
- hence "(x \<le> s\<^isub>1 \<and> (s\<^isub>1 - x) @ s\<^isub>2 = y) \<or> (s\<^isub>1 \<le> x \<and> (x - s\<^isub>1) @ y = s\<^isub>2)"
- using app_eq_dest by auto
- moreover have "\<lbrakk>x \<le> s\<^isub>1; (s\<^isub>1 - x) @ s\<^isub>2 = y\<rbrakk> \<Longrightarrow>
- \<exists> ya \<le> y. (x @ ya) \<in> L\<^isub>1 \<and> (y - ya) \<in> L\<^isub>2"
- using in_seq by (rule_tac x = "s\<^isub>1 - x" in exI, auto elim:prefixE)
- moreover have "\<lbrakk>s\<^isub>1 \<le> x; (x - s\<^isub>1) @ y = s\<^isub>2\<rbrakk> \<Longrightarrow>
- \<exists> xa \<le> x. xa \<in> L\<^isub>1 \<and> (x - xa) @ y \<in> L\<^isub>2"
- using in_seq by (rule_tac x = s\<^isub>1 in exI, auto)
- ultimately show ?thesis by blast
-qed
-
-lemma tag_str_SEQ_injI:
- "tag_str_SEQ L\<^isub>1 L\<^isub>2 m = tag_str_SEQ L\<^isub>1 L\<^isub>2 n \<Longrightarrow> m \<approx>(L\<^isub>1 ;; L\<^isub>2) n"
-proof-
- { fix x y z
- assume xz_in_seq: "x @ z \<in> L\<^isub>1 ;; L\<^isub>2"
- and tag_xy: "tag_str_SEQ L\<^isub>1 L\<^isub>2 x = tag_str_SEQ L\<^isub>1 L\<^isub>2 y"
- have"y @ z \<in> L\<^isub>1 ;; L\<^isub>2"
- proof-
- have "(\<exists> xa \<le> x. xa \<in> L\<^isub>1 \<and> (x - xa) @ z \<in> L\<^isub>2) \<or>
- (\<exists> za \<le> z. (x @ za) \<in> L\<^isub>1 \<and> (z - za) \<in> L\<^isub>2)"
- using xz_in_seq append_seq_elim by simp
- moreover {
- fix xa
- assume h1: "xa \<le> x" and h2: "xa \<in> L\<^isub>1" and h3: "(x - xa) @ z \<in> L\<^isub>2"
- obtain ya where "ya \<le> y" and "ya \<in> L\<^isub>1" and "(y - ya) @ z \<in> L\<^isub>2"
- proof -
- have "\<exists> ya. ya \<le> y \<and> ya \<in> L\<^isub>1 \<and> (x - xa) \<approx>L\<^isub>2 (y - ya)"
- proof -
- have "{\<approx>L\<^isub>2 `` {x - xa} |xa. xa \<le> x \<and> xa \<in> L\<^isub>1} =
- {\<approx>L\<^isub>2 `` {y - xa} |xa. xa \<le> y \<and> xa \<in> L\<^isub>1}"
- (is "?Left = ?Right")
- using h1 tag_xy by (auto simp:tag_str_SEQ_def)
- moreover have "\<approx>L\<^isub>2 `` {x - xa} \<in> ?Left" using h1 h2 by auto
- ultimately have "\<approx>L\<^isub>2 `` {x - xa} \<in> ?Right" by simp
- thus ?thesis by (auto simp:Image_def str_eq_rel_def str_eq_def)
- qed
- with prems show ?thesis by (auto simp:str_eq_rel_def str_eq_def)
- qed
- hence "y @ z \<in> L\<^isub>1 ;; L\<^isub>2" by (erule_tac prefixE, auto simp:Seq_def)
- } moreover {
- fix za
- assume h1: "za \<le> z" and h2: "(x @ za) \<in> L\<^isub>1" and h3: "z - za \<in> L\<^isub>2"
- hence "y @ za \<in> L\<^isub>1"
- proof-
- have "\<approx>L\<^isub>1 `` {x} = \<approx>L\<^isub>1 `` {y}"
- using h1 tag_xy by (auto simp:tag_str_SEQ_def)
- with h2 show ?thesis
- by (auto simp:Image_def str_eq_rel_def str_eq_def)
- qed
- with h1 h3 have "y @ z \<in> L\<^isub>1 ;; L\<^isub>2"
- by (drule_tac A = L\<^isub>1 in seq_intro, auto elim:prefixE)
- }
- ultimately show ?thesis by blast
- qed
- } thus "tag_str_SEQ L\<^isub>1 L\<^isub>2 m = tag_str_SEQ L\<^isub>1 L\<^isub>2 n \<Longrightarrow> m \<approx>(L\<^isub>1 ;; L\<^isub>2) n"
- by (auto simp add: str_eq_def str_eq_rel_def)
-qed
-
-lemma quot_seq_finiteI [intro]:
- fixes L1 L2::"lang"
- assumes fin1: "finite (UNIV // \<approx>L1)"
- and fin2: "finite (UNIV // \<approx>L2)"
- shows "finite (UNIV // \<approx>(L1 ;; L2))"
-proof (rule_tac tag = "tag_str_SEQ L1 L2" in tag_finite_imageD)
- show "\<And>x y. tag_str_SEQ L1 L2 x = tag_str_SEQ L1 L2 y \<Longrightarrow> x \<approx>(L1 ;; L2) y"
- by (rule tag_str_SEQ_injI)
-next
- have *: "finite ((UNIV // \<approx>L1) \<times> (Pow (UNIV // \<approx>L2)))"
- using fin1 fin2 by auto
- show "finite (range (tag_str_SEQ L1 L2))"
- unfolding tag_str_SEQ_def
- apply(rule finite_subset[OF _ *])
- unfolding quotient_def
- by auto
-qed
-
-subsubsection {* The case for @{const ALT} *}
+subsubsection {* The inductive case for @{const ALT} *}
definition
tag_str_ALT :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang)"
where
"tag_str_ALT L1 L2 = (\<lambda>x. (\<approx>L1 `` {x}, \<approx>L2 `` {x}))"
-
lemma quot_union_finiteI [intro]:
fixes L1 L2::"lang"
assumes finite1: "finite (UNIV // \<approx>L1)"
@@ -441,7 +378,161 @@
by auto
qed
-subsubsection {* The case for @{const "STAR"} *}
+subsubsection {* The inductive case for @{text "SEQ"}*}
+
+text {*
+ For case @{const "SEQ"}, the language @{text "L"} is @{text "L\<^isub>1 ;; L\<^isub>2"}.
+ Given @{text "x @ z \<in> L\<^isub>1 ;; L\<^isub>2"}, according to the defintion of @{text " L\<^isub>1 ;; L\<^isub>2"},
+ string @{text "x @ z"} can be splitted with the prefix in @{text "L\<^isub>1"} and suffix in @{text "L\<^isub>2"}.
+ The split point can either be in @{text "x"} (as shown in Fig. \ref{seq_first_split}),
+ or in @{text "z"} (as shown in Fig. \ref{seq_snd_split}). Whichever way it goes, the structure
+ on @{text "x @ z"} cn be transfered faithfully onto @{text "y @ z"}
+ (as shown in Fig. \ref{seq_trans_first_split} and \ref{seq_trans_snd_split}) with the the help of the assumed
+ tag equality. The following tag function @{text "tag_str_SEQ"} is such designed to facilitate
+ such transfers and lemma @{text "tag_str_SEQ_injI"} formalizes the informal argument above. The details
+ of structure transfer will be given their.
+\input{fig_seq}
+
+ *}
+
+definition
+ tag_str_SEQ :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang set)"
+where
+ "tag_str_SEQ L1 L2 =
+ (\<lambda>x. (\<approx>L1 `` {x}, {(\<approx>L2 `` {x - xa}) | xa. xa \<le> x \<and> xa \<in> L1}))"
+
+text {* The following is a techical lemma which helps to split the @{text "x @ z \<in> L\<^isub>1 ;; L\<^isub>2"} mentioned above.*}
+
+lemma append_seq_elim:
+ assumes "x @ y \<in> L\<^isub>1 ;; L\<^isub>2"
+ shows "(\<exists> xa \<le> x. xa \<in> L\<^isub>1 \<and> (x - xa) @ y \<in> L\<^isub>2) \<or>
+ (\<exists> ya \<le> y. (x @ ya) \<in> L\<^isub>1 \<and> (y - ya) \<in> L\<^isub>2)"
+proof-
+ from assms obtain s\<^isub>1 s\<^isub>2
+ where eq_xys: "x @ y = s\<^isub>1 @ s\<^isub>2"
+ and in_seq: "s\<^isub>1 \<in> L\<^isub>1 \<and> s\<^isub>2 \<in> L\<^isub>2"
+ by (auto simp:Seq_def)
+ from app_eq_dest [OF eq_xys]
+ have
+ "(x \<le> s\<^isub>1 \<and> (s\<^isub>1 - x) @ s\<^isub>2 = y) \<or> (s\<^isub>1 \<le> x \<and> (x - s\<^isub>1) @ y = s\<^isub>2)"
+ (is "?Split1 \<or> ?Split2") .
+ moreover have "?Split1 \<Longrightarrow> \<exists> ya \<le> y. (x @ ya) \<in> L\<^isub>1 \<and> (y - ya) \<in> L\<^isub>2"
+ using in_seq by (rule_tac x = "s\<^isub>1 - x" in exI, auto elim:prefixE)
+ moreover have "?Split2 \<Longrightarrow> \<exists> xa \<le> x. xa \<in> L\<^isub>1 \<and> (x - xa) @ y \<in> L\<^isub>2"
+ using in_seq by (rule_tac x = s\<^isub>1 in exI, auto)
+ ultimately show ?thesis by blast
+qed
+
+
+lemma tag_str_SEQ_injI:
+ fixes v w
+ assumes eq_tag: "tag_str_SEQ L\<^isub>1 L\<^isub>2 v = tag_str_SEQ L\<^isub>1 L\<^isub>2 w"
+ shows "v \<approx>(L\<^isub>1 ;; L\<^isub>2) w"
+proof-
+ -- {* As explained before, a pattern for just one direction needs to be dealt with:*}
+ { fix x y z
+ assume xz_in_seq: "x @ z \<in> L\<^isub>1 ;; L\<^isub>2"
+ and tag_xy: "tag_str_SEQ L\<^isub>1 L\<^isub>2 x = tag_str_SEQ L\<^isub>1 L\<^isub>2 y"
+ have"y @ z \<in> L\<^isub>1 ;; L\<^isub>2"
+ proof-
+ -- {* There are two ways to split @{text "x@z"}: *}
+ from append_seq_elim [OF xz_in_seq]
+ have "(\<exists> xa \<le> x. xa \<in> L\<^isub>1 \<and> (x - xa) @ z \<in> L\<^isub>2) \<or>
+ (\<exists> za \<le> z. (x @ za) \<in> L\<^isub>1 \<and> (z - za) \<in> L\<^isub>2)" .
+ -- {* It can be shown that @{text "?thesis"} holds in either case: *}
+ moreover {
+ -- {* The case for the first split:*}
+ fix xa
+ assume h1: "xa \<le> x" and h2: "xa \<in> L\<^isub>1" and h3: "(x - xa) @ z \<in> L\<^isub>2"
+ -- {* The following subgoal implements the structure transfer:*}
+ obtain ya
+ where "ya \<le> y"
+ and "ya \<in> L\<^isub>1"
+ and "(y - ya) @ z \<in> L\<^isub>2"
+ proof -
+ -- {*
+ \begin{minipage}{0.8\textwidth}
+ By expanding the definition of
+ @{thm [display] "tag_xy"}
+ and extracting the second compoent, we get:
+ \end{minipage}
+ *}
+ have "{\<approx>L\<^isub>2 `` {x - xa} |xa. xa \<le> x \<and> xa \<in> L\<^isub>1} =
+ {\<approx>L\<^isub>2 `` {y - ya} |ya. ya \<le> y \<and> ya \<in> L\<^isub>1}" (is "?Left = ?Right")
+ using tag_xy unfolding tag_str_SEQ_def by simp
+ -- {* Since @{thm "h1"} and @{thm "h2"} hold, it is not difficult to show: *}
+ moreover have "\<approx>L\<^isub>2 `` {x - xa} \<in> ?Left" using h1 h2 by auto
+ -- {*
+ \begin{minipage}{0.7\textwidth}
+ Through tag equality, equivalent class @{term "\<approx>L\<^isub>2 `` {x - xa}"} also
+ belongs to the @{text "?Right"}:
+ \end{minipage}
+ *}
+ ultimately have "\<approx>L\<^isub>2 `` {x - xa} \<in> ?Right" by simp
+ -- {* From this, the counterpart of @{text "xa"} in @{text "y"} is obtained:*}
+ then obtain ya
+ where eq_xya: "\<approx>L\<^isub>2 `` {x - xa} = \<approx>L\<^isub>2 `` {y - ya}"
+ and pref_ya: "ya \<le> y" and ya_in: "ya \<in> L\<^isub>1"
+ by simp blast
+ -- {* It can be proved that @{text "ya"} has the desired property:*}
+ have "(y - ya)@z \<in> L\<^isub>2"
+ proof -
+ from eq_xya have "(x - xa) \<approx>L\<^isub>2 (y - ya)"
+ unfolding Image_def str_eq_rel_def str_eq_def by auto
+ with h3 show ?thesis unfolding str_eq_rel_def str_eq_def by simp
+ qed
+ -- {* Now, @{text "ya"} has all properties to be a qualified candidate:*}
+ with pref_ya ya_in
+ show ?thesis using prems by blast
+ qed
+ -- {* From the properties of @{text "ya"}, @{text "y @ z \<in> L\<^isub>1 ;; L\<^isub>2"} is derived easily.*}
+ hence "y @ z \<in> L\<^isub>1 ;; L\<^isub>2" by (erule_tac prefixE, auto simp:Seq_def)
+ } moreover {
+ -- {* The other case is even more simpler: *}
+ fix za
+ assume h1: "za \<le> z" and h2: "(x @ za) \<in> L\<^isub>1" and h3: "z - za \<in> L\<^isub>2"
+ have "y @ za \<in> L\<^isub>1"
+ proof-
+ have "\<approx>L\<^isub>1 `` {x} = \<approx>L\<^isub>1 `` {y}"
+ using tag_xy unfolding tag_str_SEQ_def by simp
+ with h2 show ?thesis
+ unfolding Image_def str_eq_rel_def str_eq_def by auto
+ qed
+ with h1 h3 have "y @ z \<in> L\<^isub>1 ;; L\<^isub>2"
+ by (drule_tac A = L\<^isub>1 in seq_intro, auto elim:prefixE)
+ }
+ ultimately show ?thesis by blast
+ qed
+ }
+ -- {*
+ \begin{minipage}{0.8\textwidth}
+ @{text "?thesis"} is proved by exploiting the symmetry of
+ @{thm [source] "eq_tag"}:
+ \end{minipage}
+ *}
+ from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]]
+ show ?thesis unfolding str_eq_def str_eq_rel_def by blast
+qed
+
+lemma quot_seq_finiteI [intro]:
+ fixes L1 L2::"lang"
+ assumes fin1: "finite (UNIV // \<approx>L1)"
+ and fin2: "finite (UNIV // \<approx>L2)"
+ shows "finite (UNIV // \<approx>(L1 ;; L2))"
+proof (rule_tac tag = "tag_str_SEQ L1 L2" in tag_finite_imageD)
+ show "\<And>x y. tag_str_SEQ L1 L2 x = tag_str_SEQ L1 L2 y \<Longrightarrow> x \<approx>(L1 ;; L2) y"
+ by (rule tag_str_SEQ_injI)
+next
+ have *: "finite ((UNIV // \<approx>L1) \<times> (Pow (UNIV // \<approx>L2)))"
+ using fin1 fin2 by auto
+ show "finite (range (tag_str_SEQ L1 L2))"
+ unfolding tag_str_SEQ_def
+ apply(rule finite_subset[OF _ *])
+ unfolding quotient_def
+ by auto
+qed
+
+subsubsection {* The inductive case for @{const "STAR"} *}
text {*
This turned out to be the trickiest case. The essential goal is
@@ -449,24 +540,25 @@
and that @{text "x"} and @{text "y"} have the same tag. The reasoning goes as the following:
\begin{enumerate}
\item Since @{text "x @ z \<in> L\<^isub>1*"} holds, a prefix @{text "xa"} of @{text "x"} can be found
- such that @{text "xa \<in> L\<^isub>1*"} and @{text "(x - xa)@z \<in> L\<^isub>1*"}, as shown in Fig. \ref{first_split}(a).
+ such that @{text "xa \<in> L\<^isub>1*"} and @{text "(x - xa)@z \<in> L\<^isub>1*"}, as shown in Fig. \ref{first_split}.
Such a prefix always exists, @{text "xa = []"}, for example, is one.
\item There could be many but fintie many of such @{text "xa"}, from which we can find the longest
- and name it @{text "xa_max"}, as shown in Fig. \ref{max_split}(b).
+ and name it @{text "xa_max"}, as shown in Fig. \ref{max_split}.
\item The next step is to split @{text "z"} into @{text "za"} and @{text "zb"} such that
- @{text "(x - xa_max) @ za \<in> L\<^isub>1"} and @{text "zb \<in> L\<^isub>1*"} as shown in Fig. \ref{last_split}(d).
+ @{text "(x - xa_max) @ za \<in> L\<^isub>1"} and @{text "zb \<in> L\<^isub>1*"} as shown in Fig. \ref{last_split}.
Such a split always exists because:
\begin{enumerate}
- \item Because @{text "(x - x_max) @ z \<in> L\<^isub>1*"}, it can always be split into prefix @{text "a"}
+ \item Because @{text "(x - x_max) @ z \<in> L\<^isub>1*"}, it can always be splitted into prefix @{text "a"}
and suffix @{text "b"}, such that @{text "a \<in> L\<^isub>1"} and @{text "b \<in> L\<^isub>1*"},
- as shown in Fig. \ref{ab_split}(c).
- \item But the prefix @{text "a"} CANNOT be shorter than @{text "x - xa_max"}, otherwise
- @{text "xa_max"} is not the max in it's kind.
- \item Now, @{text "za"} is just @{text "a - (x - xa_max)"} and @{text "zb"} is just @{text "b"}.
+ as shown in Fig. \ref{ab_split}.
+ \item But the prefix @{text "a"} CANNOT be shorter than @{text "x - xa_max"}
+ (as shown in Fig. \ref{ab_split_wrong}), becasue otherwise,
+ @{text "ma_max@a"} would be in the same kind as @{text "xa_max"} but with
+ a larger size, conflicting with the fact that @{text "xa_max"} is the longest.
\end{enumerate}
\item \label{tansfer_step}
By the assumption that @{text "x"} and @{text "y"} have the same tag, the structure on @{text "x @ z"}
- can be transferred to @{text "y @ z"} as shown in Fig. \ref{trans_split}(e). The detailed steps are:
+ can be transferred to @{text "y @ z"} as shown in Fig. \ref{trans_split}. The detailed steps are:
\begin{enumerate}
\item A @{text "y"}-prefix @{text "ya"} corresponding to @{text "xa"} can be found,
which satisfies conditions: @{text "ya \<in> L\<^isub>1*"} and @{text "(y - ya)@za \<in> L\<^isub>1"}.
@@ -478,182 +570,9 @@
The formal proof of lemma @{text "tag_str_STAR_injI"} faithfully follows this informal argument
while the tagging function @{text "tag_str_STAR"} is defined to make the transfer in step
- \ref{transfer_step}4 feasible.
-
-
-\begin{figure}[h!]
-\centering
-\subfigure[First split]{\label{first_split}
-\scalebox{0.9}{
-\begin{tikzpicture}
- \node[draw,minimum height=3.8ex] (xa) {$\hspace{2em}xa\hspace{2em}$};
- \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{5em}x - xa\hspace{5em}$ };
- \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (z) { $\hspace{21em}$ };
-
- \draw[decoration={brace,transform={yscale=3}},decorate]
- (xa.north west) -- ($(xxa.north east)+(0em,0em)$)
- node[midway, above=0.5em]{$x$};
-
- \draw[decoration={brace,transform={yscale=3}},decorate]
- (z.north west) -- ($(z.north east)+(0em,0em)$)
- node[midway, above=0.5em]{$z$};
-
- \draw[decoration={brace,transform={yscale=3}},decorate]
- ($(xa.north west)+(0em,3ex)$) -- ($(z.north east)+(0em,3ex)$)
- node[midway, above=0.8em]{$x @ z \in L_1*$};
-
- \draw[decoration={brace,transform={yscale=3}},decorate]
- ($(z.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
- node[midway, below=0.5em]{$(x - xa) @ z \in L_1*$};
-
- \draw[decoration={brace,transform={yscale=3}},decorate]
- ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
- node[midway, below=0.5em]{$xa \in L_1*$};
-\end{tikzpicture}}}
-
-\subfigure[Max split]{\label{max_split}
-\scalebox{0.9}{
-\begin{tikzpicture}
- \node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}xa\_max\hspace{4em}$ };
- \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}x - xa\_max\hspace{0.5em}$ };
- \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (z) { $\hspace{21em}$ };
-
- \draw[decoration={brace,transform={yscale=3}},decorate]
- (xa.north west) -- ($(xxa.north east)+(0em,0em)$)
- node[midway, above=0.5em]{$x$};
-
- \draw[decoration={brace,transform={yscale=3}},decorate]
- (z.north west) -- ($(z.north east)+(0em,0em)$)
- node[midway, above=0.5em]{$z$};
-
- \draw[decoration={brace,transform={yscale=3}},decorate]
- ($(xa.north west)+(0em,3ex)$) -- ($(z.north east)+(0em,3ex)$)
- node[midway, above=0.8em]{$x @ z \in L_1*$};
-
- \draw[decoration={brace,transform={yscale=3}},decorate]
- ($(z.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
- node[midway, below=0.5em]{$(x - xa\_max) @ z \in L_1*$};
-
- \draw[decoration={brace,transform={yscale=3}},decorate]
- ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
- node[midway, below=0.5em]{$xa \in L_1*$};
-\end{tikzpicture}}}
-
-\subfigure[Max split with $a$ and $b$]{\label{ab_split}
-\scalebox{0.9}{
-\begin{tikzpicture}
- \node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}xa\_max\hspace{4em}$ };
- \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}x - xa\_max\hspace{0.5em}$ };
- \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (z) { $\hspace{21em}$ };
-
- \draw[decoration={brace,transform={yscale=3}},decorate]
- (xa.north west) -- ($(xxa.north east)+(0em,0em)$)
- node[midway, above=0.5em]{$x$};
-
- \draw[decoration={brace,transform={yscale=3}},decorate]
- (z.north west) -- ($(z.north east)+(0em,0em)$)
- node[midway, above=0.5em]{$z$};
-
- \draw[decoration={brace,transform={yscale=3}},decorate]
- ($(xa.north west)+(0em,3ex)$) -- ($(z.north east)+(0em,3ex)$)
- node[midway, above=0.8em]{$x @ z \in L_1*$};
-
- \draw[decoration={brace,transform={yscale=3}},decorate]
- ($(z.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
- node[midway, below=0.5em]{$(x - xa\_max) @ z \in L_1*$};
-
- \draw[decoration={brace,transform={yscale=3}},decorate]
- ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
- node[midway, below=0.5em]{$xa \in L_1*$};
+ \ref{ansfer_step} feasible.
- \draw[decoration={brace,transform={yscale=3}},decorate]
- ($(xxa.south east)+(6em,-5ex)$) -- ($(xxa.south west)+(0em,-5ex)$)
- node[midway, below=0.5em]{$a \in L_1$};
-
- \draw[decoration={brace,transform={yscale=3}},decorate]
- ($(z.south east)+(0em,-5ex)$) -- ($(xxa.south east)+(6em,-5ex)$)
- node[midway, below=0.5em]{$b \in L_1*$};
-
-\end{tikzpicture}}}
-
-\subfigure[Last split]{\label{last_split}
-\scalebox{0.9}{
-\begin{tikzpicture}
- \node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}xa\_max\hspace{4em}$ };
- \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}x - xa\_max\hspace{0.5em}$ };
- \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (za) { $\hspace{2em}za\hspace{2em}$ };
- \node[draw,minimum height=3.8ex, right=-0.03em of za] (zb) { $\hspace{7em}zb\hspace{7em}$ };
-
- \draw[decoration={brace,transform={yscale=3}},decorate]
- (xa.north west) -- ($(xxa.north east)+(0em,0em)$)
- node[midway, above=0.5em]{$x$};
-
- \draw[decoration={brace,transform={yscale=3}},decorate]
- (za.north west) -- ($(zb.north east)+(0em,0em)$)
- node[midway, above=0.5em]{$z$};
-
- \draw[decoration={brace,transform={yscale=3}},decorate]
- ($(xa.north west)+(0em,3ex)$) -- ($(zb.north east)+(0em,3ex)$)
- node[midway, above=0.8em]{$x @ z \in L_1*$};
-
- \draw[decoration={brace,transform={yscale=3}},decorate]
- ($(za.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
- node[midway, below=0.5em]{$(x - xa\_max) @ za \in L_1$};
-
- \draw[decoration={brace,transform={yscale=3}},decorate]
- ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
- node[midway, below=0.5em]{$xa\_max \in L_1*$};
-
- \draw[decoration={brace,transform={yscale=3}},decorate]
- ($(zb.south east)+(0em,0ex)$) -- ($(zb.south west)+(0em,0ex)$)
- node[midway, below=0.5em]{$zb \in L_1*$};
-
- \draw[decoration={brace,transform={yscale=3}},decorate]
- ($(zb.south east)+(0em,-4ex)$) -- ($(xxa.south west)+(0em,-4ex)$)
- node[midway, below=0.5em]{$(x - xa\_max)@z \in L_1*$};
-\end{tikzpicture}}}
-
-
-\subfigure[Transferring to $y$]{\label{trans_split}
-\scalebox{0.9}{
-\begin{tikzpicture}
- \node[draw,minimum height=3.8ex] (xa) { $\hspace{5em}ya\hspace{5em}$ };
- \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{2em}y - ya\hspace{2em}$ };
- \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (za) { $\hspace{2em}za\hspace{2em}$ };
- \node[draw,minimum height=3.8ex, right=-0.03em of za] (zb) { $\hspace{7em}zb\hspace{7em}$ };
-
- \draw[decoration={brace,transform={yscale=3}},decorate]
- (xa.north west) -- ($(xxa.north east)+(0em,0em)$)
- node[midway, above=0.5em]{$y$};
-
- \draw[decoration={brace,transform={yscale=3}},decorate]
- (za.north west) -- ($(zb.north east)+(0em,0em)$)
- node[midway, above=0.5em]{$z$};
-
- \draw[decoration={brace,transform={yscale=3}},decorate]
- ($(xa.north west)+(0em,3ex)$) -- ($(zb.north east)+(0em,3ex)$)
- node[midway, above=0.8em]{$y @ z \in L_1*$};
-
- \draw[decoration={brace,transform={yscale=3}},decorate]
- ($(za.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
- node[midway, below=0.5em]{$(y - ya) @ za \in L_1$};
-
- \draw[decoration={brace,transform={yscale=3}},decorate]
- ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
- node[midway, below=0.5em]{$ya \in L_1*$};
-
- \draw[decoration={brace,transform={yscale=3}},decorate]
- ($(zb.south east)+(0em,0ex)$) -- ($(zb.south west)+(0em,0ex)$)
- node[midway, below=0.5em]{$zb \in L_1*$};
-
- \draw[decoration={brace,transform={yscale=3}},decorate]
- ($(zb.south east)+(0em,-4ex)$) -- ($(xxa.south west)+(0em,-4ex)$)
- node[midway, below=0.5em]{$(y - ya)@z \in L_1*$};
-\end{tikzpicture}}}
-
-\caption{The case for $STAR$}
-\end{figure}
-
+ \input{fig_star}
*}
definition
@@ -688,7 +607,7 @@
qed
-text {* Technical lemma. *}
+text {* The following is a technical lemma.which helps to show the range finiteness of tag function. *}
lemma finite_strict_prefix_set: "finite {xa. xa < (x::string)}"
apply (induct x rule:rev_induct, simp)
apply (subgoal_tac "{xa. xa < xs @ [x]} = {xa. xa < xs} \<union> {xs}")
@@ -700,16 +619,7 @@
assumes eq_tag: "tag_str_STAR L\<^isub>1 v = tag_str_STAR L\<^isub>1 w"
shows "(v::string) \<approx>(L\<^isub>1\<star>) w"
proof-
- -- {*
- \begin{minipage}{0.9\textwidth}
- According to the definition of @{text "\<approx>Lang"},
- proving @{text "v \<approx>(L\<^isub>1\<star>) w"} amounts to
- showing: for any string @{text "u"},
- if @{text "v @ u \<in> (L\<^isub>1\<star>)"} then @{text "w @ u \<in> (L\<^isub>1\<star>)"} and vice versa.
- The reasoning pattern for both directions are the same, as derived
- in the following:
- \end{minipage}
- *}
+ -- {* As explained before, a pattern for just one direction needs to be dealt with:*}
{ fix x y z
assume xz_in_star: "x @ z \<in> L\<^isub>1\<star>"
and tag_xy: "tag_str_STAR L\<^isub>1 x = tag_str_STAR L\<^isub>1 y"
@@ -723,16 +633,12 @@
by (auto simp:tag_str_STAR_def strict_prefix_def)
thus ?thesis using xz_in_star True by simp
next
- -- {*
- \begin{minipage}{0.9\textwidth}
- The case when @{text "x"} is not null, and
- @{text "x @ z"} is in @{text "L\<^isub>1\<star>"},
- \end{minipage}
+ -- {* The nontrival case:
*}
case False
-- {*
- \begin{minipage}{0.9\textwidth}
- Since @{text "x @ z \<in> L\<^isub>1\<star>"}, @{text "x"} can always be splited
+ \begin{minipage}{0.8\textwidth}
+ Since @{text "x @ z \<in> L\<^isub>1\<star>"}, @{text "x"} can always be splitted
by a prefix @{text "xa"} together with its suffix @{text "x - xa"}, such
that both @{text "xa"} and @{text "(x - xa) @ z"} are in @{text "L\<^isub>1\<star>"},
and there could be many such splittings.Therefore, the following set @{text "?S"}
@@ -745,8 +651,9 @@
auto simp:finite_strict_prefix_set)
moreover have "?S \<noteq> {}" using False xz_in_star
by (simp, rule_tac x = "[]" in exI, auto simp:strict_prefix_def)
- -- {* Since @{text "?S"} is finite, we can always single out the longest
- and name it @{text "xa_max"}:
+ -- {* \begin{minipage}{0.7\textwidth}
+ Since @{text "?S"} is finite, we can always single out the longest and name it @{text "xa_max"}:
+ \end{minipage}
*}
ultimately have "\<exists> xa_max \<in> ?S. \<forall> xa \<in> ?S. length xa \<le> length xa_max"
using finite_set_has_max by blast
@@ -758,7 +665,7 @@
\<longrightarrow> length xa \<le> length xa_max"
by blast
-- {*
- \begin{minipage}{0.9\textwidth}
+ \begin{minipage}{0.8\textwidth}
By the equality of tags, the counterpart of @{text "xa_max"} among
@{text "y"}-prefixes, named @{text "ya"}, can be found:
\end{minipage}
@@ -776,9 +683,9 @@
(simp add:Image_def str_eq_rel_def str_eq_def) by blast
qed
-- {*
- \begin{minipage}{0.9\textwidth}
- If the following proposition can be proved, then the @{text "?thesis"}:
- @{text "y @ z \<in> L\<^isub>1\<star>"} is just a simple consequence.
+ \begin{minipage}{0.8\textwidth}
+ The @{text "?thesis"}, @{prop "y @ z \<in> L\<^isub>1\<star>"}, is a simple consequence
+ of the following proposition:
\end{minipage}
*}
have "(y - ya) @ z \<in> L\<^isub>1\<star>"
@@ -789,8 +696,8 @@
and l_za: "(y - ya)@za \<in> L\<^isub>1" and ls_zb: "zb \<in> L\<^isub>1\<star>"
proof -
-- {*
- \begin{minipage}{0.9\textwidth}
- Since @{text "(x - xa_max) @ z"} is in @{text "L\<^isub>1\<star>"}, it can be split into
+ \begin{minipage}{0.8\textwidth}
+ Since @{thm "h1"}, @{text "x"} can be splitted into
@{text "a"} and @{text "b"} such that:
\end{minipage}
*}
@@ -806,9 +713,9 @@
and eq_z: "z = ?za @ ?zb" (is "?P2")
proof -
-- {*
- \begin{minipage}{0.9\textwidth}
- Since @{text "(x - xa_max) @ z = a @ b"}, the string @{text "(x - xa_max) @ z"}
- could be splited in two ways:
+ \begin{minipage}{0.8\textwidth}
+ Since @{text "(x - xa_max) @ z = a @ b"}, string @{text "(x - xa_max) @ z"}
+ can be splitted in two ways:
\end{minipage}
*}
have "((x - xa_max) \<le> a \<and> (a - (x - xa_max)) @ b = z) \<or>
@@ -842,10 +749,7 @@
show ?thesis by blast
qed
-- {*
- \begin{minipage}{0.9\textwidth}
- From the properties of @{text "za"} and @{text "zb"} such obtained,
- @{text "?thesis"} can be shown easily.
- \end{minipage}
+ @{text "?thesis"} can easily be shown using properties of @{text "za"} and @{text "zb"}:
*}
from step [OF l_za ls_zb]
have "((y - ya) @ za) @ zb \<in> L\<^isub>1\<star>" .
@@ -858,17 +762,17 @@
-- {* By instantiating the reasoning pattern just derived for both directions:*}
from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]]
-- {* The thesis is proved as a trival consequence: *}
- show ?thesis by (unfold str_eq_def str_eq_rel_def, blast)
+ show ?thesis unfolding str_eq_def str_eq_rel_def by blast
qed
-lemma -- {* The oringal version with a poor readability*}
+lemma -- {* The oringal version with less explicit details. *}
fixes v w
assumes eq_tag: "tag_str_STAR L\<^isub>1 v = tag_str_STAR L\<^isub>1 w"
shows "(v::string) \<approx>(L\<^isub>1\<star>) w"
proof-
-- {*
- \begin{minipage}{0.9\textwidth}
+ \begin{minipage}{0.8\textwidth}
According to the definition of @{text "\<approx>Lang"},
proving @{text "v \<approx>(L\<^isub>1\<star>) w"} amounts to
showing: for any string @{text "u"},
@@ -891,7 +795,7 @@
thus ?thesis using xz_in_star True by simp
next
-- {*
- \begin{minipage}{0.9\textwidth}
+ \begin{minipage}{0.8\textwidth}
The case when @{text "x"} is not null, and
@{text "x @ z"} is in @{text "L\<^isub>1\<star>"},
\end{minipage}
@@ -967,7 +871,7 @@
-- {* By instantiating the reasoning pattern just derived for both directions:*}
from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]]
-- {* The thesis is proved as a trival consequence: *}
- show ?thesis by (unfold str_eq_def str_eq_rel_def, blast)
+ show ?thesis unfolding str_eq_def str_eq_rel_def by blast
qed
lemma quot_star_finiteI [intro]:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/tphols-2011/document/fig_seq.tex Mon Jan 31 14:51:47 2011 +0000
@@ -0,0 +1,102 @@
+\begin{figure}[h!]
+\centering
+
+\subfigure[First possible way to split $x@z$]{\label{seq_first_split}
+\scalebox{0.7}{
+\begin{tikzpicture}
+ \node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}xa\hspace{4em}$ };
+ \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}x - xa\hspace{0.5em}$ };
+ \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (z) { $\hspace{21em}$ };
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ (xa.north west) -- ($(xxa.north east)+(0em,0em)$)
+ node[midway, above=0.5em]{$x$};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ (z.north west) -- ($(z.north east)+(0em,0em)$)
+ node[midway, above=0.5em]{$z$};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(xa.north west)+(0em,3ex)$) -- ($(z.north east)+(0em,3ex)$)
+ node[midway, above=0.8em]{$x @ z \in L_1 ;; L_2$};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(z.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
+ node[midway, below=0.5em]{$(x - xa) @ z \in L_2$};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
+ node[midway, below=0.5em]{$xa \in L_1$};
+\end{tikzpicture}}}
+
+\subfigure[Transferred structure corresponding to the first way of splitting]{\label{seq_trans_first_split}
+\scalebox{0.7}{
+\begin{tikzpicture}
+ \node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}ya\hspace{4em}$ };
+ \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}y - ya\hspace{0.5em}$ };
+ \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (z) { $\hspace{21em}$ };
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ (xa.north west) -- ($(xxa.north east)+(0em,0em)$)
+ node[midway, above=0.5em]{$y$};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ (z.north west) -- ($(z.north east)+(0em,0em)$)
+ node[midway, above=0.5em]{$z$};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(xa.north west)+(0em,3ex)$) -- ($(z.north east)+(0em,3ex)$)
+ node[midway, above=0.8em]{$y @ z \in L_1 ;; L_2$};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(z.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
+ node[midway, below=0.5em]{$(y - ya) @ z \in L_2$};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
+ node[midway, below=0.5em]{$ya \in L_1$};
+\end{tikzpicture}}}
+
+\subfigure[The second possible way to split $x@z$]{\label{seq_snd_split}
+\scalebox{0.7}{
+\begin{tikzpicture}
+ \node[draw,minimum height=3.8ex] (x) { $\hspace{6.5em}x\hspace{6.5em}$ };
+ \node[draw,minimum height=3.8ex, right=-0.03em of x] (za) { $\hspace{2em}za\hspace{2em}$ };
+ \node[draw,minimum height=3.8ex, right=-0.03em of za] (zza) { $\hspace{6.1em}z - za\hspace{6.1em}$ };
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(za.north west)+(0em,0ex)$) -- ($(zza.north east)+(0em,0ex)$)
+ node[midway, above=0.8em]{$z$};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(x.north west)+(0em,3ex)$) -- ($(zza.north east)+(0em,3ex)$)
+ node[midway, above=0.8em]{$x @ z \in L_1 ;; L_2$};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(za.south east)+(0em,0ex)$) -- ($(x.south west)+(0em,0ex)$)
+ node[midway, below=0.5em]{$x @ za \in L_1$};
+\end{tikzpicture}}}
+
+
+\subfigure[Transferred structure corresponding to the second way of splitting]{\label{seq_trans_snd_split}
+\scalebox{0.7}{
+\begin{tikzpicture}
+ \node[draw,minimum height=3.8ex] (x) { $\hspace{6.5em}y\hspace{6.5em}$ };
+ \node[draw,minimum height=3.8ex, right=-0.03em of x] (za) { $\hspace{2em}za\hspace{2em}$ };
+ \node[draw,minimum height=3.8ex, right=-0.03em of za] (zza) { $\hspace{6.1em}z - za\hspace{6.1em}$ };
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(za.north west)+(0em,0ex)$) -- ($(zza.north east)+(0em,0ex)$)
+ node[midway, above=0.8em]{$z$};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(x.north west)+(0em,3ex)$) -- ($(zza.north east)+(0em,3ex)$)
+ node[midway, above=0.8em]{$y @ z \in L_1 ;; L_2$};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(za.south east)+(0em,0ex)$) -- ($(x.south west)+(0em,0ex)$)
+ node[midway, below=0.5em]{$y @ za \in L_1$};
+\end{tikzpicture}}}
+
+\caption{The case for $SEQ$}
+\end{figure}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/tphols-2011/document/fig_star.tex Mon Jan 31 14:51:47 2011 +0000
@@ -0,0 +1,209 @@
+\begin{figure}[h!]
+\centering
+\subfigure[First split]{\label{first_split}
+\scalebox{0.7}{
+\begin{tikzpicture}
+ \node[draw,minimum height=3.8ex] (xa) {$\hspace{2em}xa\hspace{2em}$};
+ \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{5em}x - xa\hspace{5em}$ };
+ \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (z) { $\hspace{21em}$ };
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ (xa.north west) -- ($(xxa.north east)+(0em,0em)$)
+ node[midway, above=0.5em]{$x$};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ (z.north west) -- ($(z.north east)+(0em,0em)$)
+ node[midway, above=0.5em]{$z$};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(xa.north west)+(0em,3ex)$) -- ($(z.north east)+(0em,3ex)$)
+ node[midway, above=0.6em]{$x @ z \in L_1*$};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(z.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
+ node[midway, below=0.5em]{$(x - xa) @ z \in L_1*$};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
+ node[midway, below=0.5em]{$xa \in L_1*$};
+\end{tikzpicture}}}
+
+\subfigure[Max split]{\label{max_split}
+\scalebox{0.7}{
+\begin{tikzpicture}
+ \node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}xa\_max\hspace{4em}$ };
+ \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}x - xa\_max\hspace{0.5em}$ };
+ \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (z) { $\hspace{21em}$ };
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ (xa.north west) -- ($(xxa.north east)+(0em,0em)$)
+ node[midway, above=0.5em]{$x$};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ (z.north west) -- ($(z.north east)+(0em,0em)$)
+ node[midway, above=0.5em]{$z$};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(xa.north west)+(0em,3ex)$) -- ($(z.north east)+(0em,3ex)$)
+ node[midway, above=0.8em]{$x @ z \in L_1*$};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(z.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
+ node[midway, below=0.5em]{$(x - xa\_max) @ z \in L_1*$};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
+ node[midway, below=0.5em]{$xa \in L_1*$};
+\end{tikzpicture}}}
+
+\subfigure[Max split with $a$ and $b$ (the right situation)]{\label{ab_split}
+\scalebox{0.7}{
+\begin{tikzpicture}
+ \node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}xa\_max\hspace{4em}$ };
+ \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}x - xa\_max\hspace{0.5em}$ };
+ \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (z) { $\hspace{21em}$ };
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ (xa.north west) -- ($(xxa.north east)+(0em,0em)$)
+ node[midway, above=0.5em]{$x$};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ (z.north west) -- ($(z.north east)+(0em,0em)$)
+ node[midway, above=0.5em]{$z$};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(xa.north west)+(0em,3ex)$) -- ($(z.north east)+(0em,3ex)$)
+ node[midway, above=0.8em]{$x @ z \in L_1*$};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(z.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
+ node[midway, below=0.5em]{$(x - xa\_max) @ z \in L_1*$};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
+ node[midway, below=0.5em]{$xa \in L_1*$};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(xxa.south east)+(6em,-5ex)$) -- ($(xxa.south west)+(0em,-5ex)$)
+ node[midway, below=0.5em]{$a \in L_1$};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(z.south east)+(0em,-5ex)$) -- ($(xxa.south east)+(6em,-5ex)$)
+ node[midway, below=0.5em]{$b \in L_1*$};
+\end{tikzpicture}}}
+
+
+\subfigure[Max split with $a$ and $b$ (the wrong situation)]{\label{ab_split_wrong}
+\scalebox{0.7}{
+\begin{tikzpicture}
+ \node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}xa\_max\hspace{4em}$ };
+ \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}x - xa\_max\hspace{0.5em}$ };
+ \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (z) { $\hspace{21em}$ };
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ (xa.north west) -- ($(xxa.north east)+(0em,0em)$)
+ node[midway, above=0.5em]{$x$};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ (z.north west) -- ($(z.north east)+(0em,0em)$)
+ node[midway, above=0.5em]{$z$};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(xa.north west)+(0em,3ex)$) -- ($(z.north east)+(0em,3ex)$)
+ node[midway, above=0.8em]{$x @ z \in L_1*$};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(z.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
+ node[midway, below=0.5em]{$(x - xa\_max) @ z \in L_1*$};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
+ node[midway, below=0.5em]{$xa \in L_1*$};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(xxa.south east)+(-3em,-5ex)$) -- ($(xxa.south west)+(0em,-5ex)$)
+ node[midway, below=0.5em]{$a \in L_1$};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(z.south east)+(0em,-5ex)$) -- ($(xxa.south east)+(-3em,-5ex)$)
+ node[midway, below=0.5em]{$b \in L_1*$};
+\end{tikzpicture}}}
+
+
+\subfigure[Last split]{\label{last_split}
+\scalebox{0.7}{
+\begin{tikzpicture}
+ \node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}xa\_max\hspace{4em}$ };
+ \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}x - xa\_max\hspace{0.5em}$ };
+ \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (za) { $\hspace{2em}za\hspace{2em}$ };
+ \node[draw,minimum height=3.8ex, right=-0.03em of za] (zb) { $\hspace{7em}zb\hspace{7em}$ };
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ (xa.north west) -- ($(xxa.north east)+(0em,0em)$)
+ node[midway, above=0.5em]{$x$};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ (za.north west) -- ($(zb.north east)+(0em,0em)$)
+ node[midway, above=0.5em]{$z$};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(xa.north west)+(0em,3ex)$) -- ($(zb.north east)+(0em,3ex)$)
+ node[midway, above=0.8em]{$x @ z \in L_1*$};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(za.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
+ node[midway, below=0.5em]{$(x - xa\_max) @ za \in L_1$};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
+ node[midway, below=0.5em]{$xa\_max \in L_1*$};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(zb.south east)+(0em,0ex)$) -- ($(zb.south west)+(0em,0ex)$)
+ node[midway, below=0.5em]{$zb \in L_1*$};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(zb.south east)+(0em,-4ex)$) -- ($(xxa.south west)+(0em,-4ex)$)
+ node[midway, below=0.5em]{$(x - xa\_max)@z \in L_1*$};
+\end{tikzpicture}}}
+
+
+\subfigure[Structure transferred to $y$]{\label{trans_split}
+\scalebox{0.7}{
+\begin{tikzpicture}
+ \node[draw,minimum height=3.8ex] (xa) { $\hspace{5em}ya\hspace{5em}$ };
+ \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{2em}y - ya\hspace{2em}$ };
+ \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (za) { $\hspace{2em}za\hspace{2em}$ };
+ \node[draw,minimum height=3.8ex, right=-0.03em of za] (zb) { $\hspace{7em}zb\hspace{7em}$ };
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ (xa.north west) -- ($(xxa.north east)+(0em,0em)$)
+ node[midway, above=0.5em]{$y$};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ (za.north west) -- ($(zb.north east)+(0em,0em)$)
+ node[midway, above=0.5em]{$z$};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(xa.north west)+(0em,3ex)$) -- ($(zb.north east)+(0em,3ex)$)
+ node[midway, above=0.8em]{$y @ z \in L_1*$};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(za.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
+ node[midway, below=0.5em]{$(y - ya) @ za \in L_1$};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
+ node[midway, below=0.5em]{$ya \in L_1*$};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(zb.south east)+(0em,0ex)$) -- ($(zb.south west)+(0em,0ex)$)
+ node[midway, below=0.5em]{$zb \in L_1*$};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(zb.south east)+(0em,-4ex)$) -- ($(xxa.south west)+(0em,-4ex)$)
+ node[midway, below=0.5em]{$(y - ya)@z \in L_1*$};
+\end{tikzpicture}}}
+
+\caption{The case for $STAR$}
+\end{figure}
Binary file tphols-2011/myhill.pdf has changed