diff -r 91e3e906034c -r 68e28debe995 Closures2.thy
--- a/Closures2.thy	Tue Aug 30 11:31:18 2011 +0000
+++ b/Closures2.thy	Thu Sep 01 20:26:30 2011 +0000
@@ -1,243 +1,141 @@
 theory Closure2
-imports Closures
+imports 
+  Closures
+  (* "~~/src/HOL/Proofs/Extraction/Higman" *)
 begin
 
-inductive emb :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<preceq> _")
+inductive 
+  emb :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<preceq> _")
 where
-   emb0 [Pure.intro]: "emb [] bs"
- | emb1 [Pure.intro]: "emb as bs \<Longrightarrow> emb as (b # bs)"
- | emb2 [Pure.intro]: "emb as bs \<Longrightarrow> emb (a # as) (a # bs)"
+   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:
+lemma emb_refl [intro]:
   shows "x \<preceq> x"
-apply(induct x)
-apply(auto intro: emb.intros)
-done
+by (induct x) (auto intro: emb.intros)
 
-lemma emb_right:
+lemma emb_right [intro]:
   assumes a: "x \<preceq> y"
   shows "x \<preceq> y @ y'"
-using a
-apply(induct arbitrary: y')
-apply(auto intro: emb.intros)
-done
+using a by (induct arbitrary: y') (auto)
 
-lemma emb_left:
+lemma emb_left [intro]:
   assumes a: "x \<preceq> y"
   shows "x \<preceq> y' @ y"
-using a
-apply(induct y')
-apply(auto intro: emb.intros)
-done
+using a by (induct y') (auto)
 
-lemma emb_appendI:
+lemma emb_appendI [intro]:
   assumes a: "x \<preceq> x'"
   and     b: "y \<preceq> y'"
   shows "x @ y \<preceq> x' @ y'"
-using a b
-apply(induct)
-apply(auto intro: emb.intros emb_left)
+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_append:
-  assumes a: "x \<preceq> y1 @ y2"
-  shows "\<exists>x1 x2. x = x1 @ x2 \<and> x1 \<preceq> y1 \<and> x2 \<preceq> y2"
-using a
-apply(induct x y\<equiv>"y1 @ y2" arbitrary: y1 y2)
-apply(auto intro: emb0)[1]
-apply(simp add: Cons_eq_append_conv)
-apply(auto)[1]
-apply(rule_tac x="[]" in exI)
-apply(rule_tac x="as" in exI)
-apply(auto intro: emb.intros)[1]
-apply(simp add: append_eq_append_conv2)
-apply(drule_tac x="ys'" in meta_spec)
-apply(drule_tac x="y2" in meta_spec)
-apply(auto)[1]
-apply(rule_tac x="x1" in exI)
-apply(rule_tac x="x2" in exI)
-apply(auto intro: emb.intros)[1]
-apply(subst (asm) Cons_eq_append_conv)
-apply(auto)[1]
-apply(rule_tac x="[]" in exI)
-apply(rule_tac x="a # as" in exI)
-apply(auto intro: emb.intros)[1]
-apply(simp add: append_eq_append_conv2)
-apply(drule_tac x="ys'" in meta_spec)
-apply(drule_tac x="y2" in meta_spec)
-apply(auto)[1]
-apply(rule_tac x="a # x1" in exI)
-apply(rule_tac x="x2" in exI)
-apply(auto intro: emb.intros)[1]
+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> (- SUBSEQ A) \<union> A"
-
-lemma [simp]:
-  "SUBSEQ {} = {}"
-unfolding SUBSEQ_def
-by auto
-
-lemma [simp]:
-  "SUBSEQ {[]} = {[]}"
-unfolding SUBSEQ_def
-apply(auto)
-apply(erule emb.cases)
-apply(auto)[3]
-apply(rule emb0)
-done
+ "SUPSEQ A \<equiv> {x. \<exists>y \<in> A. y \<preceq> x}"
 
-lemma SUBSEQ_atom [simp]:
-  "SUBSEQ {[a]} = {[], [a]}"
-apply(auto simp add: SUBSEQ_def)
-apply(erule emb.cases)
-apply(auto)[3]
-apply(erule emb.cases)
-apply(auto)[3]
-apply(erule emb.cases)
-apply(auto)[3]
-apply(rule emb0)
-apply(rule emb2)
-apply(rule emb0)
-done
+lemma SUPSEQ_simps [simp]:
+  shows "SUPSEQ {} = {}"
+  and   "SUPSEQ {[]} = UNIV"
+unfolding SUPSEQ_def by auto
 
-lemma SUBSEQ_union [simp]:
-  "SUBSEQ (A \<union> B) = SUBSEQ A \<union> SUBSEQ B"
-unfolding SUBSEQ_def by auto
-
-lemma SUBSEQ_Union [simp]:
-  fixes A :: "nat \<Rightarrow> 'a lang"
-  shows "SUBSEQ (\<Union>n. (A n)) = (\<Union>n. (SUBSEQ  (A n)))"
-unfolding SUBSEQ_def image_def by auto
+lemma SUPSEQ_atom [simp]:
+  shows "SUPSEQ {[a]} = UNIV \<cdot> {[a]} \<cdot> UNIV"
+unfolding SUPSEQ_def conc_def
+by (auto) (metis append_Cons emb_cons_leftD)
 
-lemma SUBSEQ_conc1:
-  "\<lbrakk>x \<in> SUBSEQ A; y \<in> SUBSEQ B\<rbrakk> \<Longrightarrow> x @ y \<in> SUBSEQ (A \<cdot> B)"
-unfolding SUBSEQ_def 
-apply(auto)
-apply(rule_tac x="xa @ xaa" in bexI)
-apply(rule emb_appendI)
-apply(simp_all)
-done
-
-lemma SUBSEQ_conc2:
-  "x \<in> SUBSEQ (A \<cdot> B) \<Longrightarrow> x \<in> (SUBSEQ A) \<cdot> (SUBSEQ B)"
-unfolding SUBSEQ_def conc_def 
-apply(auto)
-apply(drule emb_append)
-apply(auto)
-done
+lemma SUPSEQ_union [simp]:
+  shows "SUPSEQ (A \<union> B) = SUPSEQ A \<union> SUPSEQ B"
+unfolding SUPSEQ_def by auto
 
-lemma SUBSEQ_conc [simp]:
-  "SUBSEQ (A \<cdot> B) = SUBSEQ A \<cdot> SUBSEQ B"
-apply(auto)
-apply(simp add: SUBSEQ_conc2)
-apply(subst (asm) conc_def)
-apply(auto simp add: SUBSEQ_conc1)
-done
+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 SUBSEQ_star1:
-  assumes a: "x \<in> (SUBSEQ A)\<star>" 
-  shows "x \<in> SUBSEQ (A\<star>)"
-using a
-apply(induct rule: star_induct)
-apply(simp add: SUBSEQ_def)
-apply(rule_tac x="[]" in bexI)
-apply(rule emb0)
-apply(auto)[1]
-apply(drule SUBSEQ_conc1)
-apply(assumption)
+lemma SUPSEQ_star [simp]:
+  shows "SUPSEQ (A\<star>) = UNIV"
 apply(subst star_unfold_left)
-apply(simp only: SUBSEQ_union)
+apply(simp only: SUPSEQ_union) 
 apply(simp)
 done
 
-lemma SUBSEQ_star2_aux:
-  assumes a: "x \<in> SUBSEQ (A ^^ n)" 
-  shows "x \<in> (SUBSEQ A)\<star>"
-using a
-apply(induct n arbitrary: x)
-apply(simp)
-apply(simp)
-apply(simp add: conc_def)
-apply(auto)
-done
-
-lemma SUBSEQ_star2:
-  assumes a: "x \<in> SUBSEQ (A\<star>)" 
-  shows "x \<in> (SUBSEQ A)\<star>"
-using a
-apply(subst (asm) star_def)
-apply(auto simp add: SUBSEQ_star2_aux)
-done
-
-lemma SUBSEQ_star [simp]:
-  shows "SUBSEQ (A\<star>) = (SUBSEQ A)\<star>"
-using SUBSEQ_star1 SUBSEQ_star2 by auto
-
-lemma SUBSEQ_fold:
-  shows "SUBSEQ A \<union> A = SUBSEQ A"
-apply(auto simp add: SUBSEQ_def)
-apply(rule_tac x="x" in bexI)
-apply(auto simp add: emb_refl)
-done
-
-
-lemma SUPSEQ_union [simp]:
-  "SUPSEQ (A \<union> B) = (SUPSEQ A \<union> B) \<inter> (SUPSEQ B \<union> A)"
-unfolding SUPSEQ_def 
-by auto
-
-
-definition
-  Notreg :: "'a::finite rexp \<Rightarrow> 'a rexp"
-where
-  "Notreg r \<equiv> SOME r'. lang r' = - (lang r)"
-
-lemma [simp]:
-  "lang (Notreg r) = - lang r"
-apply(simp add: Notreg_def)
-apply(rule someI2_ex)
-apply(auto)
-apply(subgoal_tac "regular (lang r)")
-apply(drule closure_complement)
-apply(auto) 
-done
-
-definition
-  Interreg :: "'a::finite rexp \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"
-where
-  "Interreg r1 r2 = Notreg (Plus (Notreg r1) (Notreg r2))"
-
-lemma [simp]:
-  "lang (Interreg r1 r2) = (lang r1) \<inter> (lang r2)"
-by (simp add: Interreg_def)
-
-definition
-  Diffreg :: "'a::finite rexp \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"
-where
-  "Diffreg r1 r2 = Notreg (Plus (Notreg r1) r2)"
-
-lemma [simp]:
-  "lang (Diffreg r1 r2) = (lang r1) - (lang r2)"
-by (auto simp add: Diffreg_def)
-
 definition
   Allreg :: "'a::finite rexp"
 where
   "Allreg \<equiv> \<Uplus>(Atom ` UNIV)"
 
 lemma Allreg_lang [simp]:
-  "lang Allreg = (\<Union>a. {[a]})"
-unfolding Allreg_def
-by auto
+  shows "lang Allreg = (\<Union>a. {[a]})"
+unfolding Allreg_def by auto
 
 lemma [simp]:
-  "(\<Union>a. {[a]})\<star> = UNIV"
+  shows "(\<Union>a. {[a]})\<star> = UNIV"
 apply(auto)
 apply(induct_tac x rule: list.induct)
 apply(auto)
@@ -248,63 +146,149 @@
 done
 
 lemma Star_Allreg_lang [simp]:
-  "lang (Star Allreg) = UNIV"
-by (simp)
-
-fun UP :: "'a::finite rexp \<Rightarrow> 'a rexp"
-where
-  "UP (Zero) = Star Allreg"
-| "UP (One) = Star Allreg"
-| "UP (Atom c) = Times Allreg (Star Allreg)"   
-| "UP (Plus r1 r2) = Interreg (Plus (UP r1) (r2)) (Plus (UP r2) r1)"
-| "UP (Times r1 r2) = 
-     Plus (Notreg (Times (Plus (Notreg (UP r1)) r1) (Plus (Notreg (UP r2)) r2))) (Times r1 r2)"
-| "UP (Star r) = Plus (Notreg (Star (Plus (Notreg (UP r)) r))) (Star r)"
+  shows "lang (Star Allreg) = UNIV"
+by simp
 
-lemma UP:
-  "lang (UP r) = SUPSEQ (lang r)"
-apply(induct r)
-apply(simp add: SUPSEQ_def)
-apply(simp add: SUPSEQ_def)
-apply(simp add: Compl_eq_Diff_UNIV)
-apply(auto)[1]
-apply(simp add: SUPSEQ_def)
-apply(simp add: Compl_eq_Diff_UNIV)
-apply(rule sym)
-apply(rule_tac s="UNIV - {[]}" in trans)
-apply(auto)[1]
-apply(auto simp add: conc_def)[1]
-apply(case_tac x)
-apply(simp)
-apply(simp)
-apply(rule_tac x="[a]" in exI)
-apply(simp)
-apply(simp)
-apply(simp)
-apply(simp add: SUPSEQ_def)
-apply(simp add: Un_Int_distrib2)
-apply(simp add: Compl_partition2)
-apply(simp add: SUBSEQ_fold)
-apply(simp add: Un_Diff)
-apply(simp add: SUPSEQ_def)
-apply(simp add: Un_Int_distrib2)
-apply(simp add: Compl_partition2)
-apply(simp add: SUBSEQ_fold)
-done
+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 SUPSEQ_reg:
-  fixes A :: "'a::finite lang"
+lemma lang_UP:
+  shows "lang (UP r) = SUPSEQ (lang r)"
+by (induct r) (simp_all)
+
+lemma regular_SUPSEQ: 
+  fixes A::"'a::finite lang"
   assumes "regular A"
   shows "regular (SUPSEQ A)"
 proof -
-  from assms obtain r::"'a::finite rexp" where eq: "lang r = A" by auto
-  moreover 
-  have "lang (UP r) = SUPSEQ (lang r)" by (rule UP)
-  ultimately show "regular (SUPSEQ A)" by auto
+  from assms obtain r::"'a::finite 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 w3:
+  assumes eq: "T = - (SUBSEQ A)"
+  shows "T = SUPSEQ T"
+apply(rule)
+apply(rule SUPSEQ_subset)
+apply(rule ccontr)
+apply(auto)
+apply(rule ccontr)
+apply(subgoal_tac "x \<in> SUBSEQ A")
+prefer 2
+apply(subst (asm) (2) eq)
+apply(simp)
+apply(simp add: SUPSEQ_def)
+apply(erule bexE)
+apply(subgoal_tac "y \<in> SUBSEQ A")
+prefer 2
+apply(simp add: SUBSEQ_def)
+apply(erule bexE)
+apply(rule_tac x="xa" in bexI)
+apply(rule emb_trans)
+apply(assumption)
+apply(assumption)
+apply(assumption)
+apply(subst (asm) (2) eq)
+apply(simp)
+done
+
+lemma w4:
+  shows "- (SUBSEQ A) = SUPSEQ (- (SUBSEQ A))"
+by (rule w3) (simp)
+
+definition
+  "minimal_in x L \<equiv> \<forall>y \<in> L. y \<preceq> x \<longrightarrow> y = x"
+
+lemma minimal_in2:
+  shows "minimal_in x L = (\<forall>y \<in> L. y \<preceq> x \<longrightarrow> x \<preceq> y)"
+by (auto simp add: minimal_in_def intro: emb_antisym)
+
+lemma higman:
+  assumes "\<forall>x \<in> A. \<forall>y \<in> A. x \<noteq> y \<longrightarrow> \<not>(x \<preceq> y) \<and> \<not>(y \<preceq> x)"
+  shows "finite A"
+sorry
+
+lemma minimal:
+  assumes "minimal_in x A" "minimal_in y A"
+  and "x \<noteq> y" "x \<in> A" "y \<in> A"
+  shows "\<not>(x \<preceq> y) \<and> \<not>(y \<preceq> x)"
+using assms unfolding minimal_in_def 
+by auto
 
- 
+lemma main_lemma:
+  "\<exists>M. M \<subseteq> A \<and> finite M \<and> SUPSEQ A = SUPSEQ M"
+proof -
+  def M \<equiv> "{x \<in> A. minimal_in x A}"
+  have "M \<subseteq> A" unfolding M_def minimal_in_def by auto
+  moreover
+  have "finite M"
+    apply(rule higman)
+    unfolding M_def minimal_in_def
+    by auto
+  moreover
+  have "SUPSEQ A \<subseteq> SUPSEQ M"
+    apply(rule)
+    apply(simp only: SUPSEQ_def)
+    apply(auto)[1]
+    using emb_wf
+    apply(erule_tac Q="{y' \<in> A. y' \<preceq> x}" and x="y" in wfE_min)
+    apply(simp)
+    apply(simp)
+    apply(rule_tac x="z" in bexI)
+    apply(simp)
+    apply(simp add: M_def)
+    apply(simp add: minimal_in2)
+    apply(rule ballI)
+    apply(rule impI)
+    apply(drule_tac x="ya" in meta_spec)
+    apply(simp)
+    apply(case_tac "ya = z")
+    apply(auto)[1]
+    apply(simp)
+    by (metis emb_trans)
+  moreover
+  have "SUPSEQ M \<subseteq> SUPSEQ A"
+    by (auto simp add: SUPSEQ_def M_def)
+  ultimately
+  show "\<exists>M. M \<subseteq> A \<and> finite M \<and> SUPSEQ A = SUPSEQ M" by blast
+qed
+
+lemma closure_SUPSEQ:
+  fixes A::"'a::finite 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::"'a::finite lang"
+  shows "regular (SUBSEQ A)"
+proof -
+  have "regular (SUPSEQ (- SUBSEQ A))" by (rule closure_SUPSEQ)
+  then have "regular (- SUBSEQ A)" 
+    apply(subst w4) 
+    apply(assumption) 
+    done
+  then have "regular (- (- (SUBSEQ A)))" by (rule closure_complement)
+  then show "regular (SUBSEQ A)" by simp
+qed
+
 
 
 end