# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1549927072 0
# Node ID a7769a89c5290a909dfb1583d3ce389e603ce20c
# Parent  496a37d816e9fa919fbf34d9b8db08f6af1364ff
added cardinality proof of Antimirov

diff -r 496a37d816e9 -r a7769a89c529 thys/PDerivs.thy
--- a/thys/PDerivs.thy	Mon Feb 11 14:36:23 2019 +0000
+++ b/thys/PDerivs.thy	Mon Feb 11 23:17:52 2019 +0000
@@ -3,19 +3,10 @@
   imports Spec
 begin
 
-(*
-  ZERO
-| ONE
-| CHAR char
-| SEQ rexp rexp
-| ALT rexp rexp
-| STAR rexp
-*)
-
 abbreviation
   "SEQs rs r \<equiv> (\<Union>r' \<in> rs. {SEQ r' r})"
 
-lemma Timess_eq_image:
+lemma SEQs_eq_image:
   "SEQs rs r = (\<lambda>r'. SEQ r' r) ` rs"
   by auto
 
@@ -67,8 +58,8 @@
 subsection \<open>Relating left-quotients and partial derivatives\<close>
 
 lemma Sequ_UNION_distrib:
-shows "A ;; \<Union>(M ` I) = \<Union>((%i. A ;; M i) ` I)"
-and   "\<Union>(M ` I) ;; A = \<Union>((%i. M i ;; A) ` I)"
+shows "A ;; \<Union>(M ` I) = \<Union>((\<lambda>i. A ;; M i) ` I)"
+and   "\<Union>(M ` I) ;; A = \<Union>((\<lambda>i. M i ;; A) ` I)"
 by (auto simp add: Sequ_def)
 
 
@@ -168,7 +159,7 @@
 unfolding pders_Set_def
 by (simp add: PSuf_Union pders_snoc)
 
-lemma pderivs_Times:
+lemma pderivs_SEQ:
   shows "pders s (SEQ r1 r2) \<subseteq> SEQs (pders s r1) r2 \<union> (pders_Set (PSuf s) r2)"
 proof (induct s rule: rev_induct)
   case (snoc c s)
@@ -209,7 +200,7 @@
   shows "pders_Set UNIV1 (SEQ r1 r2) \<subseteq> SEQs (pders_Set UNIV1 r1) r2 \<union> pders_Set UNIV1 r2"
 apply(rule pders_Set_subsetI)
 apply(rule subset_trans)
-apply(rule pderivs_Times)
+apply(rule pderivs_SEQ)
 using pders_Set_SEQ_aux1 pders_Set_SEQ_aux2
 apply auto
 apply blast
@@ -280,7 +271,7 @@
 by (metis finite_pders_Set_UNIV pders_Set_subset rev_finite_subset subset_UNIV)
 
 
-text\<open>The following relationship between the alphabetic width of regular expressions
+text \<open>The following relationship between the alphabetic width of regular expressions
 (called \<open>awidth\<close> below) and the number of partial derivatives was proved
 by Antimirov~\cite{Antimirov95} and formalized by Max Haslbeck.\<close>
 
@@ -293,10 +284,13 @@
 "awidth (STAR r1) = awidth r1"
 
 lemma card_SEQs_pders_Set_le:
-  "card (SEQs (pders_Set A r) s) \<le> card (pders_Set A r)"
-  using finite_pders_set unfolding Timess_eq_image by (rule card_image_le)
+  shows  "card (SEQs (pders_Set A r) s) \<le> card (pders_Set A r)"
+  using finite_pders_set 
+  unfolding SEQs_eq_image 
+  by (rule card_image_le)
 
-lemma card_pders_set_UNIV1_le_awidth: "card (pders_Set UNIV1 r) \<le> awidth r"
+lemma card_pders_set_UNIV1_le_awidth: 
+  shows "card (pders_Set UNIV1 r) \<le> awidth r"
 proof (induction r)
   case (ALT r1 r2)
   have "card (pders_Set UNIV1 (ALT r1 r2)) = card (pders_Set UNIV1 r1 \<union> pders_Set UNIV1 r2)" by simp
@@ -324,7 +318,9 @@
 qed (auto)
 
 text\<open>Antimirov's Theorem 3.4:\<close>
-theorem card_pders_set_UNIV_le_awidth: "card (pders_Set UNIV r) \<le> awidth r + 1"
+
+theorem card_pders_set_UNIV_le_awidth: 
+  shows "card (pders_Set UNIV r) \<le> awidth r + 1"
 proof -
   have "card (insert r (pders_Set UNIV1 r)) \<le> Suc (card (pders_Set UNIV1 r))"
     by(auto simp: card_insert_if[OF finite_pders_Set_UNIV1])
@@ -333,10 +329,16 @@
 qed 
 
 text\<open>Antimirov's Corollary 3.5:\<close>
-corollary card_pders_set_le_awidth: "card (pders_Set A r) \<le> awidth r + 1"
-by(rule order_trans[OF
-  card_mono[OF finite_pders_Set_UNIV pders_Set_subset[OF subset_UNIV]]
-  card_pders_set_UNIV_le_awidth])
+
+corollary card_pders_set_le_awidth: 
+  shows "card (pders_Set A r) \<le> awidth r + 1"
+proof -
+  have "card (pders_Set A r) \<le> card (pders_Set UNIV r)"
+    by (simp add: card_mono finite_pders_set pders_Set_subset)
+  also have "... \<le> awidth r + 1"
+    by (rule card_pders_set_UNIV_le_awidth)
+  finally show "card (pders_Set A r) \<le> awidth r + 1" by simp
+qed
 
 
 end
\ No newline at end of file