Myhill_2.thy
author urbanc
Wed, 18 May 2011 19:54:43 +0000
changeset 162 e93760534354
parent 160 ea2e5acbfe4a
child 166 7743d2ad71d1
permissions -rw-r--r--
added directory for journal version; took uptodate version of the theory files
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
63
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
     1
theory Myhill_2
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
     2
  imports Myhill_1 Prefix_subtract
149
e122cb146ecc added the most current versions of the theories.
urbanc
parents: 132
diff changeset
     3
          "~~/src/HOL/Library/List_Prefix"
63
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
     4
begin
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
     5
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
     6
section {* Direction @{text "regular language \<Rightarrow>finite partition"} *}
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
     7
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
     8
definition
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
     9
  str_eq :: "string \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> bool" ("_ \<approx>_ _")
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
    10
where
75
d63baacbdb16 parts of the 3 section
urbanc
parents: 63
diff changeset
    11
  "x \<approx>A y \<equiv> (x, y) \<in> (\<approx>A)"
63
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
    12
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
    13
definition 
117
22ba25b808c8 updated second direction
urbanc
parents: 113
diff changeset
    14
   tag_eq_rel :: "(string \<Rightarrow> 'b) \<Rightarrow> (string \<times> string) set" ("=_=")
63
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
    15
where
117
22ba25b808c8 updated second direction
urbanc
parents: 113
diff changeset
    16
   "=tag= \<equiv> {(x, y) | x y. tag x = tag y}"
22ba25b808c8 updated second direction
urbanc
parents: 113
diff changeset
    17
22ba25b808c8 updated second direction
urbanc
parents: 113
diff changeset
    18
lemma finite_eq_tag_rel:
63
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
    19
  assumes rng_fnt: "finite (range tag)"
109
79b37ef9505f minor updated
urbanc
parents: 99
diff changeset
    20
  shows "finite (UNIV // =tag=)"
63
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
    21
proof -
119
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
    22
  let "?f" =  "\<lambda>X. tag ` X" and ?A = "(UNIV // =tag=)"
118
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
    23
  have "finite (?f ` ?A)" 
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
    24
  proof -
119
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
    25
    have "range ?f \<subseteq> (Pow (range tag))" unfolding Pow_def by auto
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
    26
    moreover 
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
    27
    have "finite (Pow (range tag))" using rng_fnt by simp
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
    28
    ultimately 
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
    29
    have "finite (range ?f)" unfolding image_def by (blast intro: finite_subset)
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
    30
    moreover
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
    31
    have "?f ` ?A \<subseteq> range ?f" by auto
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
    32
    ultimately show "finite (?f ` ?A)" by (rule rev_finite_subset) 
63
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
    33
  qed
118
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
    34
  moreover
119
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
    35
  have "inj_on ?f ?A"
118
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
    36
  proof -
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
    37
    { fix X Y
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
    38
      assume X_in: "X \<in> ?A"
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
    39
        and  Y_in: "Y \<in> ?A"
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
    40
        and  tag_eq: "?f X = ?f Y"
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
    41
      then obtain x y 
119
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
    42
        where "x \<in> X" "y \<in> Y" "tag x = tag y"
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
    43
        unfolding quotient_def Image_def image_def tag_eq_rel_def
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
    44
        by (simp) (blast)
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
    45
      with X_in Y_in 
118
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
    46
      have "X = Y"
119
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
    47
	unfolding quotient_def tag_eq_rel_def by auto
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
    48
    } 
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
    49
    then show "inj_on ?f ?A" unfolding inj_on_def by auto
118
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
    50
  qed
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
    51
  ultimately show "finite (UNIV // =tag=)" by (rule finite_imageD)
63
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
    52
qed
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
    53
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
    54
lemma refined_partition_finite:
118
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
    55
  assumes fnt: "finite (UNIV // R1)"
63
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
    56
  and refined: "R1 \<subseteq> R2"
118
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
    57
  and eq1: "equiv UNIV R1" and eq2: "equiv UNIV R2"
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
    58
  shows "finite (UNIV // R2)"
63
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
    59
proof -
118
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
    60
  let ?f = "\<lambda>X. {R1 `` {x} | x. x \<in> X}" 
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
    61
    and ?A = "UNIV // R2" and ?B = "UNIV // R1"
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
    62
  have "?f ` ?A \<subseteq> Pow ?B"
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
    63
    unfolding image_def Pow_def quotient_def by auto
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
    64
  moreover
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
    65
  have "finite (Pow ?B)" using fnt by simp
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
    66
  ultimately  
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
    67
  have "finite (?f ` ?A)" by (rule finite_subset)
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
    68
  moreover
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
    69
  have "inj_on ?f ?A"
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
    70
  proof -
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
    71
    { fix X Y
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
    72
      assume X_in: "X \<in> ?A" and Y_in: "Y \<in> ?A" and eq_f: "?f X = ?f Y"
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
    73
      from quotientE [OF X_in]
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
    74
      obtain x where "X = R2 `` {x}" by blast
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
    75
      with equiv_class_self[OF eq2] have x_in: "x \<in> X" by simp
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
    76
      then have "R1 ``{x} \<in> ?f X" by auto
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
    77
      with eq_f have "R1 `` {x} \<in> ?f Y" by simp
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
    78
      then obtain y 
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
    79
        where y_in: "y \<in> Y" and eq_r1_xy: "R1 `` {x} = R1 `` {y}" by auto
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
    80
      with eq_equiv_class[OF _ eq1] 
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
    81
      have "(x, y) \<in> R1" by blast
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
    82
      with refined have "(x, y) \<in> R2" by auto
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
    83
      with quotient_eqI [OF eq2 X_in Y_in x_in y_in]
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
    84
      have "X = Y" .
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
    85
    } 
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
    86
    then show "inj_on ?f ?A" unfolding inj_on_def by blast 
63
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
    87
  qed
118
c3fa11ee776e first proof
urbanc
parents: 117
diff changeset
    88
  ultimately show "finite (UNIV // R2)" by (rule finite_imageD)
63
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
    89
qed
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
    90
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
    91
lemma tag_finite_imageD:
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
    92
  assumes rng_fnt: "finite (range tag)" 
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
    93
  and same_tag_eqvt: "\<And>m n. tag m = tag n \<Longrightarrow> m \<approx>A n"
119
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
    94
  shows "finite (UNIV // \<approx>A)"
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
    95
proof (rule_tac refined_partition_finite [of "=tag="])
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
    96
  show "finite (UNIV // =tag=)" by (rule finite_eq_tag_rel[OF rng_fnt])
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
    97
next
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
    98
  from same_tag_eqvt
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
    99
  show "=tag= \<subseteq> \<approx>A" unfolding tag_eq_rel_def str_eq_def
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
   100
    by auto
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
   101
next
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
   102
  show "equiv UNIV =tag="
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
   103
    unfolding equiv_def tag_eq_rel_def refl_on_def sym_def trans_def
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
   104
    by auto
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
   105
next
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
   106
  show "equiv UNIV (\<approx>A)" 
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
   107
    unfolding equiv_def str_eq_rel_def sym_def refl_on_def trans_def
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
   108
    by blast
63
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   109
qed
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   110
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   111
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   112
subsection {* The proof *}
63
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   113
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   114
subsubsection {* The base case for @{const "NULL"} *}
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   115
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   116
lemma quot_null_eq:
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   117
  shows "UNIV // \<approx>{} = {UNIV}"
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   118
unfolding quotient_def Image_def str_eq_rel_def by auto
63
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   119
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   120
lemma quot_null_finiteI [intro]:
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   121
  shows "finite (UNIV // \<approx>{})"
63
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   122
unfolding quot_null_eq by simp
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   123
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   124
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   125
subsubsection {* The base case for @{const "EMPTY"} *}
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   126
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   127
lemma quot_empty_subset:
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   128
  shows "UNIV // \<approx>{[]} \<subseteq> {{[]}, UNIV - {[]}}"
63
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   129
proof
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   130
  fix x
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   131
  assume "x \<in> UNIV // \<approx>{[]}"
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   132
  then obtain y where h: "x = {z. (y, z) \<in> \<approx>{[]}}" 
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   133
    unfolding quotient_def Image_def by blast
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   134
  show "x \<in> {{[]}, UNIV - {[]}}"
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   135
  proof (cases "y = []")
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   136
    case True with h
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   137
    have "x = {[]}" by (auto simp: str_eq_rel_def)
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   138
    thus ?thesis by simp
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   139
  next
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   140
    case False with h
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   141
    have "x = UNIV - {[]}" by (auto simp: str_eq_rel_def)
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   142
    thus ?thesis by simp
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   143
  qed
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   144
qed
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   145
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   146
lemma quot_empty_finiteI [intro]:
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   147
  shows "finite (UNIV // \<approx>{[]})"
63
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   148
by (rule finite_subset[OF quot_empty_subset]) (simp)
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   149
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   150
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   151
subsubsection {* The base case for @{const "CHAR"} *}
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   152
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   153
lemma quot_char_subset:
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   154
  "UNIV // (\<approx>{[c]}) \<subseteq> {{[]},{[c]}, UNIV - {[], [c]}}"
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   155
proof 
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   156
  fix x 
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   157
  assume "x \<in> UNIV // \<approx>{[c]}"
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   158
  then obtain y where h: "x = {z. (y, z) \<in> \<approx>{[c]}}" 
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   159
    unfolding quotient_def Image_def by blast
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   160
  show "x \<in> {{[]},{[c]}, UNIV - {[], [c]}}"
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   161
  proof -
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   162
    { assume "y = []" hence "x = {[]}" using h 
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   163
        by (auto simp:str_eq_rel_def) } 
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   164
    moreover 
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   165
    { assume "y = [c]" hence "x = {[c]}" using h 
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   166
        by (auto dest!:spec[where x = "[]"] simp:str_eq_rel_def) } 
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   167
    moreover 
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   168
    { assume "y \<noteq> []" and "y \<noteq> [c]"
63
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   169
      hence "\<forall> z. (y @ z) \<noteq> [c]" by (case_tac y, auto)
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   170
      moreover have "\<And> p. (p \<noteq> [] \<and> p \<noteq> [c]) = (\<forall> q. p @ q \<noteq> [c])" 
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   171
        by (case_tac p, auto)
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   172
      ultimately have "x = UNIV - {[],[c]}" using h
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   173
        by (auto simp add:str_eq_rel_def)
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   174
    } 
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   175
    ultimately show ?thesis by blast
63
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   176
  qed
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   177
qed
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   178
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   179
lemma quot_char_finiteI [intro]:
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   180
  shows "finite (UNIV // \<approx>{[c]})"
63
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   181
by (rule finite_subset[OF quot_char_subset]) (simp)
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   182
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   183
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   184
subsubsection {* The inductive case for @{const ALT} *}
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   185
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   186
definition 
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   187
  tag_str_ALT :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang)"
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   188
where
119
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
   189
  "tag_str_ALT A B \<equiv> (\<lambda>x. (\<approx>A `` {x}, \<approx>B `` {x}))"
63
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   190
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   191
lemma quot_union_finiteI [intro]:
119
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
   192
  assumes finite1: "finite (UNIV // \<approx>A)"
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
   193
  and     finite2: "finite (UNIV // \<approx>B)"
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
   194
  shows "finite (UNIV // \<approx>(A \<union> B))"
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
   195
proof (rule_tac tag = "tag_str_ALT A B" in tag_finite_imageD)
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
   196
  have "finite ((UNIV // \<approx>A) \<times> (UNIV // \<approx>B))" 
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
   197
    using finite1 finite2 by auto
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
   198
  then show "finite (range (tag_str_ALT A B))"
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
   199
    unfolding tag_str_ALT_def quotient_def
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
   200
    by (rule rev_finite_subset) (auto)
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
   201
next
ece3f197b92b first two proofs in 2 direction
urbanc
parents: 118
diff changeset
   202
  show "\<And>x y. tag_str_ALT A B x = tag_str_ALT A B y \<Longrightarrow> x \<approx>(A \<union> B) y"
120
c1f596c7f59e ALT case done
urbanc
parents: 119
diff changeset
   203
    unfolding tag_str_ALT_def
63
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   204
    unfolding str_eq_def
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   205
    unfolding str_eq_rel_def
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   206
    by auto
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   207
qed
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   208
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   209
63
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   210
subsubsection {* The inductive case for @{text "SEQ"}*}
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   211
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   212
definition 
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   213
  tag_str_SEQ :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang set)"
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   214
where
109
79b37ef9505f minor updated
urbanc
parents: 99
diff changeset
   215
  "tag_str_SEQ L1 L2 \<equiv>
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   216
     (\<lambda>x. (\<approx>L1 `` {x}, {(\<approx>L2 `` {x - xa}) | xa.  xa \<le> x \<and> xa \<in> L1}))"
63
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   217
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   218
lemma Seq_in_cases:
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   219
  assumes "x @ z \<in> A ;; B"
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   220
  shows "(\<exists> x' \<le> x. x' \<in> A \<and> (x - x') @ z \<in> B) \<or> 
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   221
         (\<exists> z' \<le> z. (x @ z') \<in> A \<and> (z - z') \<in> B)"
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   222
using assms
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   223
unfolding Seq_def prefix_def
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   224
by (auto simp add: append_eq_append_conv2)
63
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   225
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   226
lemma tag_str_SEQ_injI:
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   227
  assumes eq_tag: "tag_str_SEQ A B x = tag_str_SEQ A B y" 
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   228
  shows "x \<approx>(A ;; B) y"
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   229
proof -
63
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   230
  { fix x y z
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   231
    assume xz_in_seq: "x @ z \<in> A ;; B"
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   232
    and tag_xy: "tag_str_SEQ A B x = tag_str_SEQ A B y"
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   233
    have"y @ z \<in> A ;; B" 
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   234
    proof -
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   235
      { (* first case with x' in A and (x - x') @ z in B *)
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   236
        fix x'
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   237
        assume h1: "x' \<le> x" and h2: "x' \<in> A" and h3: "(x - x') @ z \<in> B"
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   238
        obtain y' 
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   239
          where "y' \<le> y" 
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   240
          and "y' \<in> A" 
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   241
          and "(y - y') @ z \<in> B"
63
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   242
        proof -
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   243
          have "{\<approx>B `` {x - x'} |x'. x' \<le> x \<and> x' \<in> A} = 
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   244
                {\<approx>B `` {y - y'} |y'. y' \<le> y \<and> y' \<in> A}" (is "?Left = ?Right")
63
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   245
            using tag_xy unfolding tag_str_SEQ_def by simp
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   246
          moreover 
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   247
	  have "\<approx>B `` {x - x'} \<in> ?Left" using h1 h2 by auto
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   248
          ultimately 
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   249
	  have "\<approx>B `` {x - x'} \<in> ?Right" by simp
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   250
          then obtain y' 
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   251
            where eq_xy': "\<approx>B `` {x - x'} = \<approx>B `` {y - y'}" 
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   252
            and pref_y': "y' \<le> y" and y'_in: "y' \<in> A"
63
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   253
            by simp blast
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   254
	  
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   255
	  have "(x - x')  \<approx>B (y - y')" using eq_xy'
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   256
            unfolding Image_def str_eq_rel_def str_eq_def by auto
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   257
          with h3 have "(y - y') @ z \<in> B" 
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   258
	    unfolding str_eq_rel_def str_eq_def by simp
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   259
          with pref_y' y'_in 
63
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   260
          show ?thesis using that by blast
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   261
        qed
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   262
	then have "y @ z \<in> A ;; B" by (erule_tac prefixE) (auto simp: Seq_def)
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   263
      } 
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   264
      moreover 
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   265
      { (* second case with x @ z' in A and z - z' in B *)
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   266
        fix z'
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   267
        assume h1: "z' \<le> z" and h2: "(x @ z') \<in> A" and h3: "z - z' \<in> B"
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   268
	 have "\<approx>A `` {x} = \<approx>A `` {y}" 
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   269
           using tag_xy unfolding tag_str_SEQ_def by simp
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   270
         with h2 have "y @ z' \<in> A"
63
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   271
            unfolding Image_def str_eq_rel_def str_eq_def by auto
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   272
        with h1 h3 have "y @ z \<in> A ;; B"
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   273
	  unfolding prefix_def Seq_def
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   274
	  by (auto) (metis append_assoc)
63
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   275
      }
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   276
      ultimately show "y @ z \<in> A ;; B" 
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   277
	using Seq_in_cases [OF xz_in_seq] by blast
63
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   278
    qed
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   279
  }
63
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   280
  from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]]
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   281
    show "x \<approx>(A ;; B) y" unfolding str_eq_def str_eq_rel_def by blast
63
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   282
qed 
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   283
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   284
lemma quot_seq_finiteI [intro]:
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   285
  fixes L1 L2::"lang"
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   286
  assumes fin1: "finite (UNIV // \<approx>L1)" 
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   287
  and     fin2: "finite (UNIV // \<approx>L2)" 
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   288
  shows "finite (UNIV // \<approx>(L1 ;; L2))"
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   289
proof (rule_tac tag = "tag_str_SEQ L1 L2" in tag_finite_imageD)
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   290
  show "\<And>x y. tag_str_SEQ L1 L2 x = tag_str_SEQ L1 L2 y \<Longrightarrow> x \<approx>(L1 ;; L2) y"
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   291
    by (rule tag_str_SEQ_injI)
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   292
next
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   293
  have *: "finite ((UNIV // \<approx>L1) \<times> (Pow (UNIV // \<approx>L2)))" 
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   294
    using fin1 fin2 by auto
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   295
  show "finite (range (tag_str_SEQ L1 L2))" 
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   296
    unfolding tag_str_SEQ_def
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   297
    apply(rule finite_subset[OF _ *])
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   298
    unfolding quotient_def
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   299
    by auto
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   300
qed
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   301
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   302
63
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   303
subsubsection {* The inductive case for @{const "STAR"} *}
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   304
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   305
definition 
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   306
  tag_str_STAR :: "lang \<Rightarrow> string \<Rightarrow> lang set"
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   307
where
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   308
  "tag_str_STAR L1 \<equiv> (\<lambda>x. {\<approx>L1 `` {x - xa} | xa. xa < x \<and> xa \<in> L1\<star>})"
63
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   309
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   310
text {* A technical lemma. *}
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   311
lemma finite_set_has_max: "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> 
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   312
           (\<exists> max \<in> A. \<forall> a \<in> A. f a <= (f max :: nat))"
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   313
proof (induct rule:finite.induct)
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   314
  case emptyI thus ?case by simp
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   315
next
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   316
  case (insertI A a)
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   317
  show ?case
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   318
  proof (cases "A = {}")
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   319
    case True thus ?thesis by (rule_tac x = a in bexI, auto)
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   320
  next
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   321
    case False
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   322
    with insertI.hyps and False  
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   323
    obtain max 
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   324
      where h1: "max \<in> A" 
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   325
      and h2: "\<forall>a\<in>A. f a \<le> f max" by blast
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   326
    show ?thesis
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   327
    proof (cases "f a \<le> f max")
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   328
      assume "f a \<le> f max"
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   329
      with h1 h2 show ?thesis by (rule_tac x = max in bexI, auto)
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   330
    next
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   331
      assume "\<not> (f a \<le> f max)"
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   332
      thus ?thesis using h2 by (rule_tac x = a in bexI, auto)
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   333
    qed
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   334
  qed
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   335
qed
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   336
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   337
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   338
text {* The following is a technical lemma, which helps to show the range finiteness of tag function. *}
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   339
63
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   340
lemma finite_strict_prefix_set: "finite {xa. xa < (x::string)}"
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   341
apply (induct x rule:rev_induct, simp)
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   342
apply (subgoal_tac "{xa. xa < xs @ [x]} = {xa. xa < xs} \<union> {xs}")
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   343
by (auto simp:strict_prefix_def)
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   344
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   345
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   346
lemma tag_str_STAR_injI:
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   347
  assumes eq_tag: "tag_str_STAR L\<^isub>1 v = tag_str_STAR L\<^isub>1 w"
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   348
  shows "v \<approx>(L\<^isub>1\<star>) w"
63
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   349
proof-
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   350
  { fix x y z
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   351
    assume xz_in_star: "x @ z \<in> L\<^isub>1\<star>" 
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   352
      and tag_xy: "tag_str_STAR L\<^isub>1 x = tag_str_STAR L\<^isub>1 y"
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   353
    have "y @ z \<in> L\<^isub>1\<star>"
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   354
    proof(cases "x = []")
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   355
      case True
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   356
      with tag_xy have "y = []" 
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   357
        by (auto simp add: tag_str_STAR_def strict_prefix_def)
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   358
      thus ?thesis using xz_in_star True by simp
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   359
    next
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   360
      case False
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   361
      let ?S = "{xa. xa < x \<and> xa \<in> L\<^isub>1\<star> \<and> (x - xa) @ z \<in> L\<^isub>1\<star>}"
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   362
      have "finite ?S"
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   363
        by (rule_tac B = "{xa. xa < x}" in finite_subset, 
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   364
          auto simp:finite_strict_prefix_set)
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   365
      moreover have "?S \<noteq> {}" using False xz_in_star
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   366
        by (simp, rule_tac x = "[]" in exI, auto simp:strict_prefix_def)
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   367
      ultimately have "\<exists> xa_max \<in> ?S. \<forall> xa \<in> ?S. length xa \<le> length xa_max" 
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   368
        using finite_set_has_max by blast
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   369
      then obtain xa_max 
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   370
        where h1: "xa_max < x" 
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   371
        and h2: "xa_max \<in> L\<^isub>1\<star>" 
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   372
        and h3: "(x - xa_max) @ z \<in> L\<^isub>1\<star>" 
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   373
        and h4:"\<forall> xa < x. xa \<in> L\<^isub>1\<star> \<and> (x - xa) @ z \<in> L\<^isub>1\<star>  
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   374
                                     \<longrightarrow> length xa \<le> length xa_max"
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   375
        by blast
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   376
      obtain ya 
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   377
        where h5: "ya < y" and h6: "ya \<in> L\<^isub>1\<star>" 
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   378
        and eq_xya: "(x - xa_max) \<approx>L\<^isub>1 (y - ya)"
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   379
      proof-
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   380
        from tag_xy have "{\<approx>L\<^isub>1 `` {x - xa} |xa. xa < x \<and> xa \<in> L\<^isub>1\<star>} = 
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   381
          {\<approx>L\<^isub>1 `` {y - xa} |xa. xa < y \<and> xa \<in> L\<^isub>1\<star>}" (is "?left = ?right")
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   382
          by (auto simp:tag_str_STAR_def)
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   383
        moreover have "\<approx>L\<^isub>1 `` {x - xa_max} \<in> ?left" using h1 h2 by auto
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   384
        ultimately have "\<approx>L\<^isub>1 `` {x - xa_max} \<in> ?right" by simp
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   385
        thus ?thesis using that 
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   386
          apply (simp add:Image_def str_eq_rel_def str_eq_def) by blast
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   387
      qed 
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   388
      have "(y - ya) @ z \<in> L\<^isub>1\<star>" 
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   389
      proof-
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   390
        obtain za zb where eq_zab: "z = za @ zb" 
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   391
          and l_za: "(y - ya)@za \<in> L\<^isub>1" and ls_zb: "zb \<in> L\<^isub>1\<star>"
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   392
        proof -
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   393
          from h1 have "(x - xa_max) @ z \<noteq> []" 
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   394
            by (auto simp:strict_prefix_def elim:prefixE)
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   395
          from star_decom [OF h3 this]
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   396
          obtain a b where a_in: "a \<in> L\<^isub>1" 
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   397
            and a_neq: "a \<noteq> []" and b_in: "b \<in> L\<^isub>1\<star>" 
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   398
            and ab_max: "(x - xa_max) @ z = a @ b" by blast
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   399
          let ?za = "a - (x - xa_max)" and ?zb = "b"
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   400
          have pfx: "(x - xa_max) \<le> a" (is "?P1") 
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   401
            and eq_z: "z = ?za @ ?zb" (is "?P2")
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   402
          proof -
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   403
            have "((x - xa_max) \<le> a \<and> (a - (x - xa_max)) @ b = z) \<or> 
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   404
              (a < (x - xa_max) \<and> ((x - xa_max) - a) @ z = b)" 
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   405
              using append_eq_dest[OF ab_max] by (auto simp:strict_prefix_def)
63
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   406
            moreover {
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   407
              assume np: "a < (x - xa_max)" 
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   408
                and b_eqs: "((x - xa_max) - a) @ z = b"
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   409
              have "False"
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   410
              proof -
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   411
                let ?xa_max' = "xa_max @ a"
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   412
                have "?xa_max' < x" 
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   413
                  using np h1 by (clarsimp simp:strict_prefix_def diff_prefix) 
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   414
                moreover have "?xa_max' \<in> L\<^isub>1\<star>" 
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   415
                  using a_in h2 by (simp add:star_intro3) 
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   416
                moreover have "(x - ?xa_max') @ z \<in> L\<^isub>1\<star>" 
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   417
                  using b_eqs b_in np h1 by (simp add:diff_diff_append)
63
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   418
                moreover have "\<not> (length ?xa_max' \<le> length xa_max)" 
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   419
                  using a_neq by simp
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   420
                ultimately show ?thesis using h4 by blast
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   421
              qed }
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   422
            ultimately show ?P1 and ?P2 by auto
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   423
          qed
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   424
          hence "(x - xa_max)@?za \<in> L\<^isub>1" using a_in by (auto elim:prefixE)
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   425
          with eq_xya have "(y - ya) @ ?za \<in> L\<^isub>1" 
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   426
            by (auto simp:str_eq_def str_eq_rel_def)
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   427
           with eq_z and b_in 
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   428
          show ?thesis using that by blast
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   429
        qed
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   430
        have "((y - ya) @ za) @ zb \<in> L\<^isub>1\<star>" using  l_za ls_zb by blast
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   431
        with eq_zab show ?thesis by simp
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   432
      qed
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   433
      with h5 h6 show ?thesis 
160
ea2e5acbfe4a added comments from Chunhan
urbanc
parents: 149
diff changeset
   434
        by (drule_tac star_intro1) (auto simp:strict_prefix_def elim:prefixE)
63
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   435
    qed
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   436
  } 
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   437
  from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]]
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   438
    show  ?thesis unfolding str_eq_def str_eq_rel_def by blast
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   439
qed
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   440
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   441
lemma quot_star_finiteI [intro]:
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   442
  assumes finite1: "finite (UNIV // \<approx>L1)"
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   443
  shows "finite (UNIV // \<approx>(L1\<star>))"
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   444
proof (rule_tac tag = "tag_str_STAR L1" in tag_finite_imageD)
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   445
  show "\<And>x y. tag_str_STAR L1 x = tag_str_STAR L1 y \<Longrightarrow> x \<approx>(L1\<star>) y"
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   446
    by (rule tag_str_STAR_injI)
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   447
next
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   448
  have *: "finite (Pow (UNIV // \<approx>L1))" 
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   449
    using finite1 by auto
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   450
  show "finite (range (tag_str_STAR L1))"
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   451
    unfolding tag_str_STAR_def
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   452
    apply(rule finite_subset[OF _ *])
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   453
    unfolding quotient_def
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   454
    by auto
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   455
qed
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   456
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   457
subsubsection{* The conclusion *}
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   458
112
62fdb4bf7239 more on the conclusion
urbanc
parents: 109
diff changeset
   459
lemma Myhill_Nerode2:
63
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   460
  fixes r::"rexp"
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   461
  shows "finite (UNIV // \<approx>(L r))"
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   462
by (induct r) (auto)
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   463
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   464
132
f77a7138f791 comments by Xingyuan
urbanc
parents: 128
diff changeset
   465
theorem Myhill_Nerode:
f77a7138f791 comments by Xingyuan
urbanc
parents: 128
diff changeset
   466
  shows "(\<exists>r::rexp. A = L r) \<longleftrightarrow> finite (UNIV // \<approx>A)"
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 160
diff changeset
   467
using Myhill_Nerode1 Myhill_Nerode2 by auto
112
62fdb4bf7239 more on the conclusion
urbanc
parents: 109
diff changeset
   468
63
649ff0b8766d Myhill_2.thy added
zhang
parents:
diff changeset
   469
end