--- a/Closures2.thy Sun Sep 04 07:28:48 2011 +0000
+++ b/Closures2.thy Mon Sep 05 12:07:16 2011 +0000
@@ -1,4 +1,4 @@
-theory Closure2
+theory Closures2
imports
Closures
Higman
@@ -29,6 +29,7 @@
hide_const A
hide_const B
+hide_const R
(*
inductive
@@ -255,14 +256,12 @@
definition
minimal :: "letter list \<Rightarrow> letter lang \<Rightarrow> bool"
where
- "minimal x A = (\<forall>y \<in> A. y \<preceq> x \<longrightarrow> x \<preceq> y)"
+ "minimal x A \<equiv> (\<forall>y \<in> A. y \<preceq> x \<longrightarrow> x \<preceq> y)"
lemma main_lemma:
- shows "\<exists>M. M \<subseteq> A \<and> finite M \<and> SUPSEQ A = SUPSEQ M"
+ shows "\<exists>M. finite M \<and> SUPSEQ A = SUPSEQ M"
proof -
def M \<equiv> "{x \<in> A. minimal x A}"
- have "M \<subseteq> A" unfolding M_def minimal_def by auto
- moreover
have "finite M"
unfolding M_def minimal_def
by (rule Higman_antichains) (auto simp add: emb_antisym)
@@ -278,14 +277,14 @@
then have "z \<in> M"
unfolding M_def minimal_def
by (auto intro: emb_trans)
- with b show "x \<in> SUPSEQ M"
+ 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. M \<subseteq> A \<and> finite M \<and> SUPSEQ A = SUPSEQ M" by blast
+ show "\<exists>M. finite M \<and> SUPSEQ A = SUPSEQ M" by blast
qed
lemma closure_SUPSEQ: