diff -r 65e786a58365 -r a73b2e553804 thys2/SizeBound6CT.thy
--- a/thys2/SizeBound6CT.thy	Tue Mar 01 11:14:17 2022 +0000
+++ b/thys2/SizeBound6CT.thy	Wed Mar 02 23:13:59 2022 +0000
@@ -21,6 +21,12 @@
 |"orderedPrefAux 0 ss = Nil"
 
 
+fun ordsuf :: "char list \<Rightarrow> char list list"
+  where
+  "ordsuf [] = []"
+| "ordsuf (x # xs) = (ordsuf xs) @ [(x # xs)]" 
+
+
 fun orderedPref :: "char list \<Rightarrow> char list list"
   where
 "orderedPref s = orderedPrefAux (length s) s"
@@ -46,6 +52,26 @@
 lemma shape_of_suf_3list:
   shows "orderedSuf [c1, c2, c3] = [[c3], [c2, c3], [c1, c2, c3]]"
   by auto
+
+
+lemma ordsuf_last:
+  shows "ordsuf (xs @ [x]) = [x] # (map (\<lambda>s. s @ [x]) (ordsuf xs))" 
+  apply(induct xs)
+  apply(auto)
+  done
+
+lemma ordsuf_append:
+  shows "ordsuf (s1 @ s) = (ordsuf s) @ (map (\<lambda>s11. s11 @ s) (ordsuf s1))"
+apply(induct s1 arbitrary: s rule: rev_induct)
+  apply(simp)
+  apply(drule_tac x="[x] @ s" in meta_spec)
+  apply(simp)
+  apply(subst ordsuf_last)
+  apply(simp)
+  done
+
+
+
 (*
 lemma throwing_elem_around:
   shows "orderedSuf (s1 @ [a] @ s) = (orderedSuf s) @ (map (\<lambda>s11. s11 @ s) (orderedSuf ( s1 @ [a]) ))"
@@ -90,10 +116,16 @@
 
 *)
 
+datatype cchar = 
+Achar
+|Bchar
+|Cchar
+|Dchar
+
 datatype rrexp = 
   RZERO
 | RONE 
-| RCHAR char
+| RCHAR cchar
 | RSEQ rrexp rrexp
 | RALTS "rrexp list"
 | RSTAR rrexp
@@ -113,13 +145,19 @@
 | "rnullable (RSEQ  r1 r2) = (rnullable r1 \<and> rnullable r2)"
 | "rnullable (RSTAR   r) = True"
 
+fun convert_cchar_char :: "cchar \<Rightarrow> char"
+  where
+"convert_cchar_char Achar = (CHR 0x41) "
+| "convert_cchar_char Bchar = (CHR 0x42) "
+| "convert_cchar_char Cchar = (CHR 0x43) "
+| "convert_cchar_char Dchar = (CHR 0x44) "
 
 fun
  rder :: "char \<Rightarrow> rrexp \<Rightarrow> rrexp"
 where
   "rder c (RZERO) = RZERO"
 | "rder c (RONE) = RZERO"
-| "rder c (RCHAR d) = (if c = d then RONE else RZERO)"
+| "rder c (RCHAR d) = (if c = (convert_cchar_char d) then RONE else RZERO)"
 | "rder c (RALTS rs) = RALTS (map (rder c) rs)"
 | "rder c (RSEQ r1 r2) = 
      (if rnullable r1
@@ -252,6 +290,12 @@
 "cond_list r1 r2 s = rders_cond_list r2 (nullable_bools r1 (orderedPref s) ) (orderedSuf s)"
 
 
+fun seq_update :: " char \<Rightarrow> rrexp \<Rightarrow> char list list \<Rightarrow> char list list"
+  where
+"seq_update c r Ss = (if (rnullable r) then ([c] # (map (\<lambda>s1. s1 @ [c]) Ss)) else (map (\<lambda>s1. s1 @ [c]) Ss))"
+
+
+
 lemma rSEQ_mono:
   shows "rsize (rsimp_SEQ r1 r2) \<le>rsize ( RSEQ r1 r2)"
   apply auto
@@ -378,7 +422,7 @@
   apply(case_tac r2)
        apply simp_all
   done
-
+(*
 lemma rsimp_aalts_another:
   shows "\<forall>r \<in> (set  (map rsimp  ((RSEQ (rders r1 s) r2) #
            (rders_cond_list r2 (nullable_bools r1 (orderedPref s))  (orderedSuf s))  )) ). (rsize r) < N "
@@ -424,8 +468,55 @@
    prefer 2
    apply auto
   sorry
+*)
 
+(*
+lemma shape_derssimpseq_onechar2:
+  shows "rders_simp (RSEQ r1 r2) [c] = 
+         rsimp (RALTS  ((RSEQ (rders_simp r1 [c]) r2) #
+           (rders_cond_list r2 (nullable_bools r1 (orderedPref [c]))  (orderedSuf [c]))) )"
+  sorry
 
+*)
+
+lemma shape_derssimpseq_onechar:
+  shows "   (rders_simp r [c]) =  (rsimp (rders r [c]))"
+and "rders_simp (RSEQ r1 r2) [c] = 
+         rsimp (RALTS  ((RSEQ (rders r1 [c]) r2) #
+           (rders_cond_list r2 (nullable_bools r1 (orderedPref [c]))  (orderedSuf [c]))) )"
+   apply simp
+  apply(simp add: rders.simps)
+  apply(case_tac "rsimp (rder c r1) = RZERO")
+   apply auto
+  apply(case_tac "rsimp (rder c r1) = RONE")
+   apply auto
+   apply(subgoal_tac "rsimp_SEQ RONE (rsimp r2) = rsimp r2")
+  prefer 2
+  using idiot
+    apply simp
+   apply(subgoal_tac "rsimp_SEQ RONE (rsimp r2) = rsimp_ALTs (rdistinct (rflts [rsimp r2]) {})")
+    prefer 2
+    apply auto
+   apply(case_tac "rsimp r2")
+        apply auto
+   apply(subgoal_tac "rdistinct x5 {} = x5")
+  prefer 2
+  using no_further_dB_after_simp
+    apply metis
+   apply(subgoal_tac "rsimp_ALTs (rdistinct x5 {}) = rsimp_ALTs x5")
+    prefer 2
+    apply fastforce  
+   apply auto
+   apply (metis no_alt_short_list_after_simp)
+  apply (case_tac "rsimp r2 = RZERO")
+   apply(subgoal_tac "rsimp_SEQ (rsimp (rder c r1)) (rsimp r2) = RZERO")
+    prefer 2
+    apply(case_tac "rsimp ( rder c r1)")
+         apply auto
+  apply(subgoal_tac "rsimp_SEQ (rsimp (rder c r1)) (rsimp r2) = RSEQ (rsimp (rder c r1)) (rsimp r2)")
+   prefer 2
+   apply auto
+  sorry
 
 lemma shape_derssimpseq_onechar2:
   shows "rders_simp (RSEQ r1 r2) [c] = 
@@ -433,6 +524,31 @@
            (rders_cond_list r2 (nullable_bools r1 (orderedPref [c]))  (orderedSuf [c]))) )"
   sorry
 
+(*
+lemma simp_helps_der_pierce_dB:
+  shows " rsimp
+            (rsimp_ALTs
+              (map (rder x)
+                (rdistinct rs {}))) = 
+          rsimp (rsimp_ALTs (rdistinct (map (rder x) rs) {}))"
+
+  sorry
+*)
+(*
+lemma simp_helps_der_pierce_flts:
+  shows " rsimp
+            (rsimp_ALTs
+             (rdistinct 
+                (map (rder x)
+                  (rflts rs )
+                ) {}
+             )
+            ) = 
+          rsimp (rsimp_ALTs (rdistinct (rflts (map (rder x) rs)) {})  )"
+
+  sorry
+
+*)
 
 lemma rders__onechar:
   shows " (rders_simp r [c]) =  (rsimp (rders r [c]))"
@@ -484,29 +600,6 @@
             )"
   sorry
 
-lemma simp_helps_der_pierce_dB:
-  shows " rsimp
-            (rsimp_ALTs
-              (map (rder x)
-                (rdistinct rs {}))) = 
-          rsimp (rsimp_ALTs (rdistinct (map (rder x) rs) {}))"
-
-  sorry
-
-lemma simp_helps_der_pierce_flts:
-  shows " rsimp
-            (rsimp_ALTs
-             (rdistinct 
-                (map (rder x)
-                  (rflts rs )
-                ) {}
-             )
-            ) = 
-          rsimp (rsimp_ALTs (rdistinct (rflts (map (rder x) rs)) {})  )"
-
-  sorry
-
-
 lemma unfold_ders_simp_inside_only: 
   shows "    (rders_simp (RSEQ r1 r2) xs =
            rsimp (RALTS (RSEQ (rders_simp r1 xs) r2 # rders_cond_list r2 (nullable_bools r1 (orderedPref xs)) (orderedSuf xs))))
@@ -594,6 +687,55 @@
   sorry
 
 
+
+
+lemma seq_update_seq_ders:
+  shows "rsimp (rder c ( rsimp (RALTS ((RSEQ (rders_simp r1 s) r2) # 
+(map (rders_simp r2) Ss))))) = 
+         rsimp (RALTS ((RSEQ (rders_simp r1 (s @ [c])) r2) # 
+(map (rders_simp r2) (seq_update c (rders_simp r1 s) Ss))))  "
+  sorry
+
+lemma seq_ders_closed_form1:
+  shows "\<exists>Ss. rders_simp (RSEQ r1 r2) [c] = rsimp (RALTS ((RSEQ (rders_simp r1 [c]) r2) # 
+(map ( rders_simp r2 ) Ss)))"
+  apply(case_tac "rnullable r1")
+   apply(subgoal_tac " rders_simp (RSEQ r1 r2) [c] = 
+rsimp (RALTS ((RSEQ (rders_simp r1 [c]) r2) # (map (rders_simp r2) [[c]])))")
+    prefer 2
+    apply (simp add: rsimp_idem)
+   apply(rule_tac x = "[[c]]" in exI)
+   apply simp
+  apply(subgoal_tac  " rders_simp (RSEQ r1 r2) [c] = 
+rsimp (RALTS ((RSEQ (rders_simp r1 [c]) r2) # (map (rders_simp r2) [])))")
+   apply blast
+  apply(simp add: rsimp_idem)
+  sorry
+
+
+
+lemma seq_ders_closed_form:
+  shows "s \<noteq> [] \<Longrightarrow> \<exists>Ss. rders_simp (RSEQ r1 r2) s = rsimp (RALTS ((RSEQ (rders_simp r1 s) r2) # 
+(map ( rders_simp r2 ) Ss)))"
+  apply(induct s rule: rev_induct)
+   apply simp
+  apply(case_tac xs)
+  using seq_ders_closed_form1 apply auto[1]
+  apply(subgoal_tac "\<exists>Ss. rders_simp (RSEQ r1 r2) xs = rsimp (RALTS (RSEQ (rders_simp r1 xs) r2 # map (rders_simp r2) Ss))")
+  prefer 2
+  
+   apply blast
+  apply(erule exE)
+  apply(rule_tac x = "seq_update x (rders_simp r1 xs) Ss" in exI)
+  apply(subst rders_simp_append)
+  apply(subgoal_tac "rders_simp (rders_simp (RSEQ r1 r2) xs) [x] = rsimp (rder x (rders_simp (RSEQ r1 r2) xs))")
+   apply(simp only:)
+   apply(subst seq_update_seq_ders)
+   apply blast
+  using rders_simp_one_char by presburger
+
+
+
 (*nullable_seq_with_list1 related *)
 lemma LHS0_def_der_alt:
   shows "rsimp (rder x (RALTS ( (RSEQ (rders_simp r1 xs) r2) # (cond_list r1 r2 xs)))) = 
@@ -710,32 +852,6 @@
    apply simp
   using r1r2ders_whole rders_simp_append rders_simp_one_char by presburger
 
-(*
-
-  apply(subgoal_tac " rsimp
-            (rder x
-              (rsimp_ALTs
-                (rdistinct
-                  (rflts
-                    (rsimp_SEQ (rsimp (rders_simp r1 xs)) (rsimp r2) #
-                     map rsimp
-                      (rders_cond_list r2 (nullable_bools r1 (orderedPrefAux (length xs) xs)) (orderedSufAux (length xs) xs))))
-                  {}))) =  
-                      rsimp
-            (
-              (rsimp_ALTs
-               (map (rder x)
-                (rdistinct
-                  (rflts
-                    (rsimp_SEQ (rsimp (rders_simp r1 xs)) (rsimp r2) #
-                     map rsimp
-                      (rders_cond_list r2 (nullable_bools r1 (orderedPrefAux (length xs) xs)) (orderedSufAux (length xs) xs))))
-                  {})
-               )
-              )
-            ) ")
-   prefer 2
-*)
 
 lemma shape_derssimp_alts:
   shows "s \<noteq> [] \<Longrightarrow> rders_simp (RALTS rs) s = rsimp (RALTS (map (\<lambda>r. rders r s) rs))"
@@ -751,13 +867,10 @@
 |"rexp_encode (RCHAR c) = 2"
 |"rexp_encode (RSEQ r1 r2) = ( 2 ^ (rexp_encode r1)) "
 *)
-lemma finite_chars:
-  shows " \<exists>N. ( (\<forall>r \<in> (set rs). \<exists>c. r = RCHAR c) \<and> (distinct rs) \<longrightarrow> length rs < N)"
-  apply(rule_tac x = "Suc 256" in exI)
-  sorry
+
 
-definition all_chars :: "int \<Rightarrow> char list"
-  where "all_chars n = map char_of [0..n]"
+
+
 (*
 fun rexp_enum :: "nat \<Rightarrow> rrexp list"
   where 
@@ -766,26 +879,150 @@
 |"rexp_enum (Suc n) = [(RSEQ r1 r2). r1 \<in> set (rexp_enum i) \<and> r2 \<in> set (rexp_enum j) \<and> i + j = n]"
 
 *)
-
-fun rexp_enum :: "nat \<Rightarrow> rrexp set"
+context notes rev_conj_cong[fundef_cong] begin
+function (sequential) rexp_enum :: "nat \<Rightarrow> rrexp set"
   where 
 "rexp_enum 0 = {}"
-|"rexp_enum (Suc 0) =  {RALTS []} \<union> {RZERO} \<union> {RONE} \<union> { (RCHAR c) |c. c \<in> set (all_chars 255)}"
-|"rexp_enum (Suc n) = {(RSEQ r1 r2)|r1 r2 i j. r1 \<in>  (rexp_enum i) \<and> r2 \<in>  (rexp_enum j) \<and> i + j = n}"
+|"rexp_enum (Suc 0) =  {RALTS []} \<union> {RZERO} \<union> {RONE} \<union> { (RCHAR c) |c. c \<in>{Achar, Bchar, Cchar, Dchar} }"
+|"rexp_enum (Suc n) = {(RSEQ r1 r2)|r1 r2 i j. r1 \<in>  (rexp_enum i) \<and> r2 \<in>  (rexp_enum j) \<and> i + j = n} \<union>
+{(RALTS (a # rs)) | a rs i j. a \<in> (rexp_enum i) \<and> (RALTS rs) \<in> (rexp_enum j) \<and> i + j = Suc n \<and> i \<le> n \<and> j \<le> n} \<union>
+{RSTAR r0 | r0. r0 \<in> (rexp_enum n)} \<union>
+(rexp_enum n)"
+  by pat_completeness auto
+termination
+  by (relation "measure size") auto
+end
+
+lemma rexp_enum_inclusion:
+  shows "(rexp_enum n) \<subseteq> (rexp_enum (Suc n))"
+  apply(induct n)
+   apply auto[1]
+  apply(simp)
+  done
+
+lemma rexp_enum_mono:
+  shows "n \<le> m \<Longrightarrow> (rexp_enum n) \<subseteq> (rexp_enum m)"
+  by (simp add: lift_Suc_mono_le rexp_enum_inclusion)
+
+lemma enum_inductive_cases:
+  shows "rsize (RSEQ r1 r2) = Suc n \<Longrightarrow> \<exists>i j. rsize r1 = i \<and> rsize r2 = j\<and> i + j = n"
+  by (metis Suc_inject rsize.simps(5))
+thm rsize.simps(5)
+
+lemma enumeration_finite:
+  shows "\<exists>Nn. card (rexp_enum n) < Nn"
+  apply(simp add:no_top_class.gt_ex)
+  done
+
+lemma size1_rexps:
+  shows "RCHAR x \<in> rexp_enum 1"
+  apply(cases x)
+     apply auto
+  done
+
+lemma non_zero_size:
+  shows "rsize r \<ge> Suc 0"
+  apply(induct r)
+  apply auto done
+
+corollary size_geq1:
+  shows "rsize r \<ge> 1"
+  by (simp add: non_zero_size)
+
+
+lemma rexp_size_induct:
+  shows "\<And>N r x5 a list.
+       \<lbrakk> rsize r = Suc N; r = RALTS x5;
+        x5 = a # list\<rbrakk>  \<Longrightarrow>\<exists>i j. rsize a = i \<and> rsize (RALTS list) = j \<and> i + j =  Suc N \<and> i \<le> N \<and> j \<le> N"
+  apply(rule_tac x = "rsize a" in exI)
+  apply(rule_tac x = "rsize (RALTS list)" in exI)
+  apply(subgoal_tac "rsize a \<ge> 1")
+   prefer 2
+  using One_nat_def non_zero_size apply presburger
+  apply(subgoal_tac "rsize (RALTS list) \<ge> 1 ")
+  prefer 2
+  using size_geq1 apply blast
+  apply simp
+  done
 
- 
-lemma finite_sized_rexp_forms_finite_set:
-  shows " \<exists>SN. ( \<forall>r.( rsize r < N \<longrightarrow> r \<in> SN)) \<and> (finite SN)"
-  apply(induct N)
+lemma rexp_enum_case3:
+  shows "N \<ge> Suc 0 \<Longrightarrow> rexp_enum (Suc N) =  {(RSEQ r1 r2)|r1 r2 i j. r1 \<in>  (rexp_enum i) \<and> r2 \<in>  (rexp_enum j) \<and> i + j = N} \<union>
+{(RALTS (a # rs)) | a rs i j. a \<in> (rexp_enum i) \<and> (RALTS rs) \<in> (rexp_enum j) \<and> i + j = Suc N \<and> i \<le> N \<and> j \<le> N} \<union>
+{RSTAR r0 | r0. r0 \<in> (rexp_enum N)} \<union>
+(rexp_enum N)"
+  apply(case_tac N)
    apply simp
-   apply auto
- (*\<lbrakk>\<forall>r. rsize r < N \<longrightarrow> r \<in> SN; finite SN\<rbrakk> \<Longrightarrow> \<exists>SN. (\<forall>r. rsize r < Suc N \<longrightarrow> r \<in> SN) \<and> finite SN*)
- (* \<And>N. \<exists>SN. (\<forall>r. rsize r < N \<longrightarrow> r \<in> SN) \<and> finite SN \<Longrightarrow> \<exists>SN. (\<forall>r. rsize r < Suc N \<longrightarrow> r \<in> SN) \<and> finite SN*)
+  apply auto
+  done
+
+
+
+lemma def_enum_alts:
+  shows "\<lbrakk> r = RALTS x5; x5 = a # list;
+        rsize a = i \<and> rsize (RALTS list) = j \<and> i + j = Suc N \<and> a \<in> (rexp_enum i) \<and> (RALTS list) \<in> (rexp_enum j) \<rbrakk>
+       \<Longrightarrow> r \<in> rexp_enum (Suc N)"
+  apply(subgoal_tac "N \<ge> 1")
+  prefer 2
+  apply (metis One_nat_def add_is_1 less_Suc0 linorder_le_less_linear non_zero_size)
+  apply(subgoal_tac " rexp_enum (Suc N) =  {(RSEQ r1 r2)|r1 r2 i j. r1 \<in>  (rexp_enum i) \<and> r2 \<in>  (rexp_enum j) \<and> i + j = N} \<union>
+{(RALTS (a # rs)) | a rs i j. a \<in> (rexp_enum i) \<and> (RALTS rs) \<in> (rexp_enum j) \<and> i + j = Suc N\<and> i \<le> N \<and> j \<le> N} \<union>
+{RSTAR r0 | r0. r0 \<in> (rexp_enum N)} \<union>
+(rexp_enum N)")
+  prefer 2
+  using One_nat_def rexp_enum_case3 apply presburger
+  apply(subgoal_tac "i \<le> N \<and> j \<le> N")
+  prefer 2
+  using non_zero_size apply auto[1]
+  apply(subgoal_tac "r \<in> {uu.
+      \<exists>a rs i j. uu = RALTS (a # rs) \<and> a \<in> rexp_enum i \<and> RALTS rs \<in> rexp_enum j \<and> i + j = Suc N \<and> i \<le> N \<and> j \<le> N}")
+   apply auto[1]
+  apply(subgoal_tac "RALTS (a # list) \<in>  {uu.
+      \<exists>a rs i j. uu = RALTS (a # rs) \<and> a \<in> rexp_enum i \<and> RALTS rs \<in> rexp_enum j \<and> i + j = Suc N \<and> i \<le> N \<and> j \<le> N}")
+
+  
+   apply fastforce
+  apply(subgoal_tac "a \<in> rexp_enum i")
+  prefer 2
+  
+   apply linarith
+  by blast
+
+lemma rexp_enum_covers:
+  shows " rsize r \<le> N \<Longrightarrow> r \<in> rexp_enum N \<and> r \<in> rexp_enum (rsize r)"
+  apply(induct N arbitrary : r)
+   apply simp
+  
+  using rsize.elims apply auto[1]
+  apply(case_tac "rsize r \<le> N")
+  using enumeration_finite
+  
+   apply (meson in_mono rexp_enum_inclusion)
+  apply(subgoal_tac "rsize r = Suc N")
+  prefer 2
+  using le_Suc_eq apply blast
+
+  apply(case_tac r)
+       prefer 5
+       apply(case_tac x5)
+        apply(subgoal_tac "rsize r =1")
+  prefer 2
+  using hand_made_def_rlist_size rlist_size.simps(2) rsize.simps(4) apply presburger
+        apply simp
+  apply(subgoal_tac "a \<in> rexp_enum (rsize a)")
+  apply(subgoal_tac "RALTS list \<in> rexp_enum (rsize (RALTS list))")
+  
+         apply (meson def_enum_alts rexp_size_induct)
+        apply(subgoal_tac "rsize (RALTS list) \<le> N")
+         apply(subgoal_tac "RALTS list \<in> rexp_enum N")
+  prefer 2
+          apply presburger
+  
   sorry
 
 
 lemma finite_size_finite_regx:
   shows " \<exists>l. \<forall>rs. ((\<forall>r \<in> (set rs). rsize r < N) \<and> (distinct rs) \<longrightarrow> (length rs) < l) "
+
   sorry
 
 (*below  probably needs proved concurrently*)