Closures2.thy
changeset 368 2d6beddb6fa6
parent 348 bea94f1e6771
equal deleted inserted replaced
367:79401279ba21 368:2d6beddb6fa6
     1 theory Closures2
     1 theory Closures2
     2 imports 
     2 imports 
     3   Closures
     3   Closures
     4   Higman
     4   (*Higman*)
       
     5   WQO_Finite_Lists
     5 begin
     6 begin
     6 
     7 
     7 section {* Closure under @{text SUBSEQ} and @{text SUPSEQ} *}
     8 section {* Closure under @{text SUBSEQ} and @{text SUPSEQ} *}
     8 
     9 
     9 (* compatibility with Higman theory by Stefan *)
    10 (* compatibility with Higman theory by Stefan *)
    12 
    13 
    13 declare  emb0 [intro]
    14 declare  emb0 [intro]
    14 declare  emb1 [intro]
    15 declare  emb1 [intro]
    15 declare  emb2 [intro]
    16 declare  emb2 [intro]
    16 
    17 
       
    18 (*
    17 lemma letter_UNIV:
    19 lemma letter_UNIV:
    18   shows "UNIV = {A, B::letter}"
    20   shows "UNIV = {A, B::letter}"
    19 apply(auto)
    21 apply(auto)
    20 apply(case_tac x)
    22 apply(case_tac x)
    21 apply(auto)
    23 apply(auto)
    27 done
    29 done
    28 
    30 
    29 hide_const A
    31 hide_const A
    30 hide_const B
    32 hide_const B
    31 hide_const R
    33 hide_const R
    32 
    34 *)
    33 (*
    35 (*
    34 inductive 
    36 inductive 
    35   emb :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<preceq> _")
    37   emb :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<preceq> _")
    36 where
    38 where
    37    emb0 [intro]: "emb [] y"
    39    emb0 [intro]: "emb [] y"
   188 | "UP (Plus r1 r2) = Plus (UP r1) (UP r2)"
   190 | "UP (Plus r1 r2) = Plus (UP r1) (UP r2)"
   189 | "UP (Times r1 r2) = Times (UP r1) (UP r2)"
   191 | "UP (Times r1 r2) = Times (UP r1) (UP r2)"
   190 | "UP (Star r) = Star Allreg"
   192 | "UP (Star r) = Star Allreg"
   191 
   193 
   192 lemma lang_UP:
   194 lemma lang_UP:
   193   fixes r::"letter rexp"
   195   fixes r::"'a::finite rexp"
   194   shows "lang (UP r) = SUPSEQ (lang r)"
   196   shows "lang (UP r) = SUPSEQ (lang r)"
   195 by (induct r) (simp_all)
   197 by (induct r) (simp_all)
   196 
   198 
   197 lemma regular_SUPSEQ: 
   199 lemma regular_SUPSEQ: 
   198   fixes A::"letter lang"
   200   fixes A::"('a::finite) lang"
   199   assumes "regular A"
   201   assumes "regular A"
   200   shows "regular (SUPSEQ A)"
   202   shows "regular (SUPSEQ A)"
   201 proof -
   203 proof -
   202   from assms obtain r::"letter rexp" where "lang r = A" by auto
   204   from assms obtain r::"'a::finite rexp" where "lang r = A" by auto
   203   then have "lang (UP r) = SUPSEQ A" by (simp add: lang_UP)
   205   then have "lang (UP r) = SUPSEQ A" by (simp add: lang_UP)
   204   then show "regular (SUPSEQ A)" by auto
   206   then show "regular (SUPSEQ A)" by auto
   205 qed
   207 qed
   206 
   208 
   207 lemma SUPSEQ_subset:
   209 lemma SUPSEQ_subset:
   234     with c show "False" by simp
   236     with c show "False" by simp
   235   qed
   237   qed
   236   ultimately show "- (SUBSEQ A) = SUPSEQ (- (SUBSEQ A))" by simp
   238   ultimately show "- (SUBSEQ A) = SUPSEQ (- (SUBSEQ A))" by simp
   237 qed
   239 qed
   238 
   240 
       
   241 (*
   239 lemma Higman_antichains:
   242 lemma Higman_antichains:
   240   assumes a: "\<forall>x \<in> A. \<forall>y \<in> A. x \<noteq> y \<longrightarrow> \<not>(x \<preceq> y) \<and> \<not>(y \<preceq> x)"
   243   assumes a: "\<forall>x \<in> A. \<forall>y \<in> A. x \<noteq> y \<longrightarrow> \<not>(x \<preceq> y) \<and> \<not>(y \<preceq> x)"
   241   shows "finite A"
   244   shows "finite A"
   242 proof (rule ccontr)
   245 proof (rule ccontr)
   243   assume "infinite A"
   246   assume "infinite A"
   250   moreover
   253   moreover
   251   have "f j \<in> A" using c by auto
   254   have "f j \<in> A" using c by auto
   252   ultimately have "\<not>(f i \<preceq> f j)" using a by simp
   255   ultimately have "\<not>(f i \<preceq> f j)" using a by simp
   253   with e show "False" by simp
   256   with e show "False" by simp
   254 qed
   257 qed
       
   258 *)
   255 
   259 
   256 definition
   260 definition
   257   minimal :: "letter list \<Rightarrow> letter lang \<Rightarrow> bool"
   261   minimal :: "'a::finite list \<Rightarrow> 'a lang \<Rightarrow> bool"
   258 where
   262 where
   259   "minimal x A \<equiv> (\<forall>y \<in> A. y \<preceq> x \<longrightarrow> x \<preceq> y)"
   263   "minimal x A \<equiv> (\<forall>y \<in> A. y \<preceq> x \<longrightarrow> x \<preceq> y)"
   260 
   264 
   261 lemma main_lemma:
   265 lemma main_lemma:
       
   266   fixes A::"('a::finite) list set" 
   262   shows "\<exists>M. finite M \<and> SUPSEQ A = SUPSEQ M"
   267   shows "\<exists>M. finite M \<and> SUPSEQ A = SUPSEQ M"
   263 proof -
   268 proof -
   264   def M \<equiv> "{x \<in> A. minimal x A}"
   269   def M \<equiv> "{x \<in> A. minimal x A}"
   265   have "finite M"
   270   have "finite M"
   266     unfolding M_def minimal_def
   271     unfolding M_def minimal_def
   286   ultimately
   291   ultimately
   287   show "\<exists>M. finite M \<and> SUPSEQ A = SUPSEQ M" by blast
   292   show "\<exists>M. finite M \<and> SUPSEQ A = SUPSEQ M" by blast
   288 qed
   293 qed
   289 
   294 
   290 lemma closure_SUPSEQ:
   295 lemma closure_SUPSEQ:
   291   fixes A::"letter lang" 
   296   fixes A::"'a::finite lang" 
   292   shows "regular (SUPSEQ A)"
   297   shows "regular (SUPSEQ A)"
   293 proof -
   298 proof -
   294   obtain M where a: "finite M" and b: "SUPSEQ A = SUPSEQ M"
   299   obtain M where a: "finite M" and b: "SUPSEQ A = SUPSEQ M"
   295     using main_lemma by blast
   300     using main_lemma by blast
   296   have "regular M" using a by (rule finite_regular)
   301   have "regular M" using a by (rule finite_regular)
   297   then have "regular (SUPSEQ M)" by (rule regular_SUPSEQ)
   302   then have "regular (SUPSEQ M)" by (rule regular_SUPSEQ)
   298   then show "regular (SUPSEQ A)" using b by simp
   303   then show "regular (SUPSEQ A)" using b by simp
   299 qed
   304 qed
   300 
   305 
   301 lemma closure_SUBSEQ:
   306 lemma closure_SUBSEQ:
   302   fixes A::"letter lang"
   307   fixes A::"'a::finite lang"
   303   shows "regular (SUBSEQ A)"
   308   shows "regular (SUBSEQ A)"
   304 proof -
   309 proof -
   305   have "regular (SUPSEQ (- SUBSEQ A))" by (rule closure_SUPSEQ)
   310   have "regular (SUPSEQ (- SUBSEQ A))" by (rule closure_SUPSEQ)
   306   then have "regular (- SUBSEQ A)" by (subst SUBSEQ_complement) (simp)
   311   then have "regular (- SUBSEQ A)" by (subst SUBSEQ_complement) (simp)
   307   then have "regular (- (- (SUBSEQ A)))" by (rule closure_complement)
   312   then have "regular (- (- (SUBSEQ A)))" by (rule closure_complement)