theory Closures2+
−
imports +
−
  Closures+
−
  Higman+
−
  (* "~~/src/HOL/Proofs/Extraction/Higman" *)+
−
begin+
−
+
−
section {* Closure under @{text SUBSEQ} and @{text SUPSEQ} *}+
−
+
−
(* compatibility with Higman theory by Stefan *)+
−
notation+
−
  emb ("_ \<preceq> _")+
−
+
−
declare  emb0 [intro]+
−
declare  emb1 [intro]+
−
declare  emb2 [intro]+
−
+
−
lemma letter_UNIV:+
−
  shows "UNIV = {A, B::letter}"+
−
apply(auto)+
−
apply(case_tac x)+
−
apply(auto)+
−
done+
−
+
−
instance letter :: finite+
−
apply(default)+
−
apply(simp add: letter_UNIV)+
−
done+
−
+
−
hide_const A+
−
hide_const B+
−
hide_const R+
−
+
−
(*+
−
inductive +
−
  emb :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<preceq> _")+
−
where+
−
   emb0 [intro]: "emb [] y"+
−
 | emb1 [intro]: "emb x y \<Longrightarrow> emb x (c # y)"+
−
 | emb2 [intro]: "emb x y \<Longrightarrow> emb (c # x) (c # y)"+
−
*)+
−
+
−
lemma emb_refl [intro]:+
−
  shows "x \<preceq> x"+
−
by (induct x) (auto)+
−
+
−
lemma emb_right [intro]:+
−
  assumes a: "x \<preceq> y"+
−
  shows "x \<preceq> y @ y'"+
−
using a +
−
by (induct arbitrary: y') (auto)+
−
+
−
lemma emb_left [intro]:+
−
  assumes a: "x \<preceq> y"+
−
  shows "x \<preceq> y' @ y"+
−
using a by (induct y') (auto)+
−
+
−
lemma emb_appendI [intro]:+
−
  assumes a: "x \<preceq> x'"+
−
  and     b: "y \<preceq> y'"+
−
  shows "x @ y \<preceq> x' @ y'"+
−
using a b by (induct) (auto)+
−
+
−
lemma emb_cons_leftD:+
−
  assumes "a # x \<preceq> y"+
−
  shows "\<exists>y1 y2. y = y1 @ [a] @ y2 \<and> x \<preceq> y2"+
−
using assms+
−
apply(induct x\<equiv>"a # x" y\<equiv>"y" arbitrary: a x y)+
−
apply(auto)+
−
apply(metis append_Cons)+
−
done+
−
+
−
lemma emb_append_leftD:+
−
  assumes "x1 @ x2 \<preceq> y"+
−
  shows "\<exists>y1 y2. y = y1 @ y2 \<and> x1 \<preceq> y1 \<and> x2 \<preceq> y2"+
−
using assms+
−
apply(induct x1 arbitrary: x2 y)+
−
apply(auto)+
−
apply(drule emb_cons_leftD)+
−
apply(auto)+
−
apply(drule_tac x="x2" in meta_spec)+
−
apply(drule_tac x="y2" in meta_spec)+
−
apply(auto)+
−
apply(rule_tac x="y1 @ (a # y1a)" in exI)+
−
apply(rule_tac x="y2a" in exI)+
−
apply(auto)+
−
done+
−
+
−
lemma emb_trans:+
−
  assumes a: "x1 \<preceq> x2"+
−
  and     b: "x2 \<preceq> x3"+
−
  shows "x1 \<preceq> x3"+
−
using a b+
−
apply(induct arbitrary: x3)+
−
apply(metis emb0)+
−
apply(metis emb_cons_leftD emb_left)+
−
apply(drule_tac emb_cons_leftD)+
−
apply(auto)+
−
done+
−
+
−
lemma emb_strict_length:+
−
  assumes a: "x \<preceq> y" "x \<noteq> y" +
−
  shows "length x < length y"+
−
using a+
−
by (induct) (auto simp add: less_Suc_eq)+
−
+
−
lemma emb_antisym:+
−
  assumes a: "x \<preceq> y" "y \<preceq> x" +
−
  shows "x = y"+
−
using a emb_strict_length+
−
by (metis not_less_iff_gr_or_eq)+
−
+
−
lemma emb_wf:+
−
  shows "wf {(x, y). x \<preceq> y \<and> x \<noteq> y}"+
−
proof -+
−
  have "wf (measure length)" by simp+
−
  moreover+
−
  have "{(x, y). x \<preceq> y \<and> x \<noteq> y} \<subseteq> measure length"+
−
    unfolding measure_def by (auto simp add: emb_strict_length)+
−
  ultimately +
−
  show "wf {(x, y). x \<preceq> y \<and> x \<noteq> y}" by (rule wf_subset)+
−
qed+
−
+
−
subsection {* Sub- and Supsequences *}+
−
+
−
definition+
−
 "SUBSEQ A \<equiv> {x. \<exists>y \<in> A. x \<preceq> y}"+
−
+
−
definition+
−
 "SUPSEQ A \<equiv> {x. \<exists>y \<in> A. y \<preceq> x}"+
−
+
−
lemma SUPSEQ_simps [simp]:+
−
  shows "SUPSEQ {} = {}"+
−
  and   "SUPSEQ {[]} = UNIV"+
−
unfolding SUPSEQ_def by auto+
−
+
−
lemma SUPSEQ_atom [simp]:+
−
  shows "SUPSEQ {[c]} = UNIV \<cdot> {[c]} \<cdot> UNIV"+
−
unfolding SUPSEQ_def conc_def+
−
by (auto) (metis append_Cons emb_cons_leftD)+
−
+
−
lemma SUPSEQ_union [simp]:+
−
  shows "SUPSEQ (A \<union> B) = SUPSEQ A \<union> SUPSEQ B"+
−
unfolding SUPSEQ_def by auto+
−
+
−
lemma SUPSEQ_conc [simp]:+
−
  shows "SUPSEQ (A \<cdot> B) = SUPSEQ A \<cdot> SUPSEQ B"+
−
unfolding SUPSEQ_def conc_def+
−
by (auto) (metis emb_append_leftD)+
−
+
−
lemma SUPSEQ_star [simp]:+
−
  shows "SUPSEQ (A\<star>) = UNIV"+
−
apply(subst star_unfold_left)+
−
apply(simp only: SUPSEQ_union) +
−
apply(simp)+
−
done+
−
+
−
definition+
−
  Allreg :: "'a::finite rexp"+
−
where+
−
  "Allreg \<equiv> \<Uplus>(Atom ` UNIV)"+
−
+
−
lemma Allreg_lang [simp]:+
−
  shows "lang Allreg = (\<Union>a. {[a]})"+
−
unfolding Allreg_def by auto+
−
+
−
lemma [simp]:+
−
  shows "(\<Union>a. {[a]})\<star> = UNIV"+
−
apply(auto)+
−
apply(induct_tac x rule: list.induct)+
−
apply(auto)+
−
apply(subgoal_tac "[a] @ list \<in> (\<Union>a. {[a]})\<star>")+
−
apply(simp)+
−
apply(rule append_in_starI)+
−
apply(auto)+
−
done+
−
+
−
lemma Star_Allreg_lang [simp]:+
−
  shows "lang (Star Allreg) = UNIV"+
−
by simp+
−
+
−
fun +
−
  UP :: "'a::finite rexp \<Rightarrow> 'a rexp"+
−
where+
−
  "UP (Zero) = Zero"+
−
| "UP (One) = Star Allreg"+
−
| "UP (Atom c) = Times (Star Allreg) (Times (Atom c) (Star Allreg))"   +
−
| "UP (Plus r1 r2) = Plus (UP r1) (UP r2)"+
−
| "UP (Times r1 r2) = Times (UP r1) (UP r2)"+
−
| "UP (Star r) = Star Allreg"+
−
+
−
lemma lang_UP:+
−
  fixes r::"letter rexp"+
−
  shows "lang (UP r) = SUPSEQ (lang r)"+
−
by (induct r) (simp_all)+
−
+
−
lemma regular_SUPSEQ: +
−
  fixes A::"letter lang"+
−
  assumes "regular A"+
−
  shows "regular (SUPSEQ A)"+
−
proof -+
−
  from assms obtain r::"letter rexp" where "lang r = A" by auto+
−
  then have "lang (UP r) = SUPSEQ A" by (simp add: lang_UP)+
−
  then show "regular (SUPSEQ A)" by auto+
−
qed+
−
+
−
lemma SUPSEQ_subset:+
−
  shows "A \<subseteq> SUPSEQ A"+
−
unfolding SUPSEQ_def by auto+
−
+
−
lemma SUBSEQ_complement:+
−
  shows "- (SUBSEQ A) = SUPSEQ (- (SUBSEQ A))"+
−
proof -+
−
  have "- (SUBSEQ A) \<subseteq> SUPSEQ (- (SUBSEQ A))"+
−
    by (rule SUPSEQ_subset)+
−
  moreover +
−
  have "SUPSEQ (- (SUBSEQ A)) \<subseteq> - (SUBSEQ A)"+
−
  proof (rule ccontr)+
−
    assume "\<not> (SUPSEQ (- (SUBSEQ A)) \<subseteq> - (SUBSEQ A))"+
−
    then obtain x where +
−
       a: "x \<in> SUPSEQ (- (SUBSEQ A))" and +
−
       b: "x \<notin> - (SUBSEQ A)" by auto+
−
+
−
    from a obtain y where c: "y \<in> - (SUBSEQ A)" and d: "y \<preceq> x"+
−
      by (auto simp add: SUPSEQ_def)+
−
+
−
    from b have "x \<in> SUBSEQ A" by simp+
−
    then obtain x' where f: "x' \<in> A" and e: "x \<preceq> x'"+
−
      by (auto simp add: SUBSEQ_def)+
−
    +
−
    from d e have "y \<preceq> x'" by (rule emb_trans)+
−
    then have "y \<in> SUBSEQ A" using f+
−
      by (auto simp add: SUBSEQ_def)+
−
    with c show "False" by simp+
−
  qed+
−
  ultimately show "- (SUBSEQ A) = SUPSEQ (- (SUBSEQ A))" by simp+
−
qed+
−
+
−
lemma Higman_antichains:+
−
  assumes a: "\<forall>x \<in> A. \<forall>y \<in> A. x \<noteq> y \<longrightarrow> \<not>(x \<preceq> y) \<and> \<not>(y \<preceq> x)"+
−
  shows "finite A"+
−
proof (rule ccontr)+
−
  assume "infinite A"+
−
  then obtain f::"nat \<Rightarrow> letter list" where b: "inj f" and c: "range f \<subseteq> A"+
−
    by (auto simp add: infinite_iff_countable_subset)+
−
  from higman_idx obtain i j where d: "i < j" and e: "f i \<preceq> f j" by blast+
−
  have "f i \<noteq> f j" using b d by (auto simp add: inj_on_def)+
−
  moreover+
−
  have "f i \<in> A" using c by auto+
−
  moreover+
−
  have "f j \<in> A" using c by auto+
−
  ultimately have "\<not>(f i \<preceq> f j)" using a by simp+
−
  with e show "False" by simp+
−
qed+
−
+
−
definition+
−
  minimal :: "letter list \<Rightarrow> letter lang \<Rightarrow> bool"+
−
where+
−
  "minimal x A \<equiv> (\<forall>y \<in> A. y \<preceq> x \<longrightarrow> x \<preceq> y)"+
−
+
−
lemma main_lemma:+
−
  shows "\<exists>M. finite M \<and> SUPSEQ A = SUPSEQ M"+
−
proof -+
−
  def M \<equiv> "{x \<in> A. minimal x A}"+
−
  have "finite M"+
−
    unfolding M_def minimal_def+
−
    by (rule Higman_antichains) (auto simp add: emb_antisym)+
−
  moreover+
−
  have "SUPSEQ A \<subseteq> SUPSEQ M"+
−
  proof+
−
    fix x+
−
    assume "x \<in> SUPSEQ A"+
−
    then obtain y where "y \<in> A" and "y \<preceq> x" by (auto simp add: SUPSEQ_def)+
−
    then have a: "y \<in> {y' \<in> A. y' \<preceq> x}" by simp+
−
    obtain z where b: "z \<in> A" "z \<preceq> x" and c: "\<forall>y. y \<preceq> z \<and> y \<noteq> z \<longrightarrow> y \<notin> {y' \<in> A. y' \<preceq> x}"+
−
      using wfE_min[OF emb_wf a] by auto+
−
    then have "z \<in> M"+
−
      unfolding M_def minimal_def+
−
      by (auto intro: emb_trans)+
−
    with b(2) show "x \<in> SUPSEQ M"+
−
      by (auto simp add: SUPSEQ_def)+
−
  qed+
−
  moreover+
−
  have "SUPSEQ M \<subseteq> SUPSEQ A"+
−
    by (auto simp add: SUPSEQ_def M_def)+
−
  ultimately+
−
  show "\<exists>M. finite M \<and> SUPSEQ A = SUPSEQ M" by blast+
−
qed+
−
+
−
lemma closure_SUPSEQ:+
−
  fixes A::"letter lang" +
−
  shows "regular (SUPSEQ A)"+
−
proof -+
−
  obtain M where a: "finite M" and b: "SUPSEQ A = SUPSEQ M"+
−
    using main_lemma by blast+
−
  have "regular M" using a by (rule finite_regular)+
−
  then have "regular (SUPSEQ M)" by (rule regular_SUPSEQ)+
−
  then show "regular (SUPSEQ A)" using b by simp+
−
qed+
−
+
−
lemma closure_SUBSEQ:+
−
  fixes A::"letter lang"+
−
  shows "regular (SUBSEQ A)"+
−
proof -+
−
  have "regular (SUPSEQ (- SUBSEQ A))" by (rule closure_SUPSEQ)+
−
  then have "regular (- SUBSEQ A)" by (subst SUBSEQ_complement) (simp)+
−
  then have "regular (- (- (SUBSEQ A)))" by (rule closure_complement)+
−
  then show "regular (SUBSEQ A)" by simp+
−
qed+
−
+
−
end+
−