--- 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