diff -r 48b452a2d4df -r b73478aaf33e Derivatives.thy --- a/Derivatives.thy Tue Aug 09 22:14:41 2011 +0000 +++ b/Derivatives.thy Tue Aug 09 22:15:11 2011 +0000 @@ -173,11 +173,11 @@ subsection {* Relating derivatives and partial derivatives *} -lemma +lemma der_pder: shows "(\ lang ` (pder c r)) = lang (der c r)" unfolding Der_der[symmetric] Der_pder by simp -lemma +lemma ders_pders: shows "(\ lang ` (pders s r)) = lang (ders s r)" unfolding Ders_ders[symmetric] Ders_pders by simp @@ -185,7 +185,7 @@ subsection {* There are only finitely many partial derivatives for a language *} abbreviation - "pders_set A r \ \s \ A. pders s r" + "pders_lang A r \ \s \ A. pders s r" text {* Non-empty suffixes of a string *} @@ -201,61 +201,61 @@ shows "(\v \ Suf s \ {[c]}. f v) = (\v \ Suf s. f (v @ [c]))" by (auto simp add: conc_def) -lemma pders_set_snoc: - shows "pders_set (Suf s \ {[c]}) r = (pder_set c (pders_set (Suf s) r))" +lemma pders_lang_snoc: + shows "pders_lang (Suf s \ {[c]}) r = (pder_set c (pders_lang (Suf s) r))" by (simp add: Suf_Union pders_snoc) lemma pders_Times: - shows "pders s (Times r1 r2) \ Timess (pders s r1) r2 \ (pders_set (Suf s) r2)" + shows "pders s (Times r1 r2) \ Timess (pders s r1) r2 \ (pders_lang (Suf s) r2)" proof (induct s rule: rev_induct) case (snoc c s) - have ih: "pders s (Times r1 r2) \ Timess (pders s r1) r2 \ (pders_set (Suf s) r2)" + have ih: "pders s (Times r1 r2) \ Timess (pders s r1) r2 \ (pders_lang (Suf s) r2)" by fact have "pders (s @ [c]) (Times r1 r2) = pder_set c (pders s (Times r1 r2))" by (simp add: pders_snoc) - also have "\ \ pder_set c (Timess (pders s r1) r2 \ (pders_set (Suf s) r2))" + also have "\ \ pder_set c (Timess (pders s r1) r2 \ (pders_lang (Suf s) r2))" using ih by (auto) (blast) - also have "\ = pder_set c (Timess (pders s r1) r2) \ pder_set c (pders_set (Suf s) r2)" + also have "\ = pder_set c (Timess (pders s r1) r2) \ pder_set c (pders_lang (Suf s) r2)" by (simp) - also have "\ = pder_set c (Timess (pders s r1) r2) \ pders_set (Suf s \ {[c]}) r2" - by (simp add: pders_set_snoc) - also have "\ \ pder_set c (Timess (pders s r1) r2) \ pder c r2 \ pders_set (Suf s \ {[c]}) r2" + also have "\ = pder_set c (Timess (pders s r1) r2) \ pders_lang (Suf s \ {[c]}) r2" + by (simp add: pders_lang_snoc) + also have "\ \ pder_set c (Timess (pders s r1) r2) \ pder c r2 \ pders_lang (Suf s \ {[c]}) r2" by auto - also have "\ \ Timess (pders (s @ [c]) r1) r2 \ pder c r2 \ pders_set (Suf s \ {[c]}) r2" - by (auto simp add: if_splits pders_snoc) (blast) - also have "\ = Timess (pders (s @ [c]) r1) r2 \ pders_set (Suf (s @ [c])) r2" + also have "\ \ Timess (pder_set c (pders s r1)) r2 \ pder c r2 \ pders_lang (Suf s \ {[c]}) r2" + by (auto simp add: if_splits) (blast) + also have "\ = Timess (pders (s @ [c]) r1) r2 \ pder c r2 \ pders_lang (Suf s \ {[c]}) r2" + by (simp add: pders_snoc) + also have "\ \ Timess (pders (s @ [c]) r1) r2 \ pders_lang (Suf (s @ [c])) r2" by (auto simp add: Suf_snoc) finally show ?case . qed (simp) - lemma pders_Star: assumes a: "s \ []" - shows "pders s (Star r) \ (\v \ Suf s. Timess (pders v r) (Star r))" + shows "pders s (Star r) \ Timess (pders_lang (Suf s) r) (Star r)" using a proof (induct s rule: rev_induct) case (snoc c s) - have ih: "s \ [] \ pders s (Star r) \ (\v\Suf s. Timess (pders v r) (Star r))" by fact + have ih: "s \ [] \ pders s (Star r) \ Timess (pders_lang (Suf s) r) (Star r)" by fact { assume asm: "s \ []" have "pders (s @ [c]) (Star r) = pder_set c (pders s (Star r))" by (simp add: pders_snoc) - also have "\ \ (pder_set c (\v\Suf s. Timess (pders v r) (Star r)))" + also have "\ \ pder_set c (Timess (pders_lang (Suf s) r) (Star r))" using ih[OF asm] by (auto) (blast) - also have "\ = (\v\Suf s. pder_set c (Timess (pders v r) (Star r)))" - by simp - also have "\ \ (\v\Suf s. (Timess (pder_set c (pders v r)) (Star r) \ pder c (Star r)))" - by (auto split: if_splits) - also have "\ = (\v\Suf s. (Timess (pder_set c (pders v r)) (Star r))) \ pder c (Star r)" - using asm by (auto simp add: Suf_def) - also have "\ = (\v\Suf s. (Timess (pders (v @ [c]) r) (Star r))) \ (Timess (pder c r) (Star r))" - by (simp add: pders_snoc) - also have "\ = (\v\Suf (s @ [c]). (Timess (pders v r) (Star r)))" + also have "\ \ Timess (pder_set c (pders_lang (Suf s) r)) (Star r) \ pder c (Star r)" + by (auto split: if_splits) (blast)+ + also have "\ \ Timess (pders_lang (Suf (s @ [c])) r) (Star r) \ (Timess (pder c r) (Star r))" + by (auto simp add: Suf_snoc pders_lang_snoc) + also have "\ = Timess (pders_lang (Suf (s @ [c])) r) (Star r)" by (auto simp add: Suf_snoc Suf_Union pders_snoc) finally have ?case . } moreover { assume asm: "s = []" then have ?case - by (auto simp add: pders_snoc Suf_def) + apply (auto simp add: pders_snoc Suf_def) + apply(rule_tac x = "[c]" in exI) + apply(auto) + done } ultimately show ?case by blast qed (simp) @@ -263,29 +263,29 @@ definition "UNIV1 \ UNIV - {[]}" -lemma pders_set_Zero: - shows "pders_set UNIV1 Zero = {Zero}" +lemma pders_lang_Zero [simp]: + shows "pders_lang UNIV1 Zero = {Zero}" unfolding UNIV1_def by auto -lemma pders_set_One: - shows "pders_set UNIV1 One = {Zero}" +lemma pders_lang_One [simp]: + shows "pders_lang UNIV1 One = {Zero}" unfolding UNIV1_def by (auto split: if_splits) -lemma pders_set_Atom: - shows "pders_set UNIV1 (Atom c) \ {One, Zero}" +lemma pders_lang_Atom: + shows "pders_lang UNIV1 (Atom c) \ {One, Zero}" unfolding UNIV1_def by (auto split: if_splits) -lemma pders_set_Plus: - shows "pders_set UNIV1 (Plus r1 r2) = pders_set UNIV1 r1 \ pders_set UNIV1 r2" +lemma pders_lang_Plus: + shows "pders_lang UNIV1 (Plus r1 r2) = pders_lang UNIV1 r1 \ pders_lang UNIV1 r2" unfolding UNIV1_def by auto -lemma pders_set_Times_aux: +lemma pders_lang_Times_aux: assumes a: "s \ UNIV1" - shows "pders_set (Suf s) r2 \ pders_set UNIV1 r2" -using a unfolding UNIV1_def Suf_def by (auto) + shows "pders_lang (Suf s) r \ pders_lang UNIV1 r" +using a unfolding UNIV1_def Suf_def by auto -lemma pders_set_Times: - shows "pders_set UNIV1 (Times r1 r2) \ Timess (pders_set UNIV1 r1) r2 \ pders_set UNIV1 r2" +lemma pders_lang_Times [intro]: + shows "pders_lang UNIV1 (Times r1 r2) \ Timess (pders_lang UNIV1 r1) r2 \ pders_lang UNIV1 r2" unfolding UNIV1_def apply(rule UN_least) apply(rule subset_trans) @@ -294,12 +294,12 @@ apply(rule conjI) apply(auto)[1] apply(rule subset_trans) -apply(rule pders_set_Times_aux) +apply(rule pders_lang_Times_aux) apply(auto simp add: UNIV1_def) done -lemma pders_set_Star: - shows "pders_set UNIV1 (Star r) \ Timess (pders_set UNIV1 r) (Star r)" +lemma pders_lang_Star [intro]: + shows "pders_lang UNIV1 (Star r) \ Timess (pders_lang UNIV1 r) (Star r)" unfolding UNIV1_def apply(rule UN_least) apply(rule subset_trans) @@ -312,60 +312,60 @@ lemma finite_Timess: assumes a: "finite A" shows "finite (Timess A r)" -using a by (auto) +using a by auto -lemma finite_pders_set_UNIV1: - shows "finite (pders_set UNIV1 r)" +lemma finite_pders_lang_UNIV1: + shows "finite (pders_lang UNIV1 r)" apply(induct r) apply(simp) -apply(simp only: pders_set_One) +apply(simp only: pders_lang_One) apply(simp) apply(rule finite_subset) -apply(rule pders_set_Atom) +apply(rule pders_lang_Atom) apply(simp) -apply(simp only: pders_set_Plus) +apply(simp only: pders_lang_Plus) apply(simp) apply(rule finite_subset) -apply(rule pders_set_Times) +apply(rule pders_lang_Times) apply(simp only: finite_Timess finite_Un) apply(simp) apply(rule finite_subset) -apply(rule pders_set_Star) +apply(rule pders_lang_Star) apply(simp only: finite_Timess) done -lemma pders_set_UNIV_UNIV1: - shows "pders_set UNIV r = pders [] r \ pders_set UNIV1 r" +lemma pders_lang_UNIV_UNIV1: + shows "pders_lang UNIV r = pders [] r \ pders_lang UNIV1 r" unfolding UNIV1_def apply(auto) apply(rule_tac x="[]" in exI) apply(simp) done -lemma finite_pders_set_UNIV: - shows "finite (pders_set UNIV r)" -unfolding pders_set_UNIV_UNIV1 -by (simp add: finite_pders_set_UNIV1) +lemma finite_pders_lang_UNIV: + shows "finite (pders_lang UNIV r)" +unfolding pders_lang_UNIV_UNIV1 +by (simp add: finite_pders_lang_UNIV1) -lemma finite_pders_set: - shows "finite (pders_set A r)" +lemma finite_pders_lang: + shows "finite (pders_lang A r)" apply(rule rev_finite_subset) -apply(rule_tac r="r" in finite_pders_set_UNIV) +apply(rule_tac r="r" in finite_pders_lang_UNIV) apply(auto) done lemma finite_pders: shows "finite (pders s r)" -using finite_pders_set[where A="{s}" and r="r"] +using finite_pders_lang[where A="{s}" and r="r"] by simp lemma finite_pders2: shows "finite {pders s r | s. s \ A}" proof - - have "{pders s r | s. s \ A} \ Pow (pders_set A r)" by auto + have "{pders s r | s. s \ A} \ Pow (pders_lang A r)" by auto moreover - have "finite (Pow (pders_set A r))" - using finite_pders_set by simp + have "finite (Pow (pders_lang A r))" + using finite_pders_lang by simp ultimately show "finite {pders s r | s. s \ A}" by(rule finite_subset) @@ -405,13 +405,9 @@ by (auto simp add: MN_Rel_Ders Ders_pders) moreover have "equiv UNIV =(\x. pders x r)=" + and "equiv UNIV (\(lang r))" unfolding equiv_def refl_on_def sym_def trans_def - unfolding tag_eq_def - by auto - moreover - have "equiv UNIV (\(lang r))" - unfolding equiv_def refl_on_def sym_def trans_def - unfolding str_eq_def + unfolding tag_eq_def str_eq_def by auto ultimately show "finite (UNIV // \(lang r))" by (rule refined_partition_finite)