27 |
27 |
28 lemma distinct_list_rexp_up_to_certain_size_bouded_by_set_enumerating_up_to_that_size: |
28 lemma distinct_list_rexp_up_to_certain_size_bouded_by_set_enumerating_up_to_that_size: |
29 shows "\<forall>r\<in> set rs. (rsize r ) \<le> N \<Longrightarrow> sum_list (map rsize (rdistinct rs {})) \<le> |
29 shows "\<forall>r\<in> set rs. (rsize r ) \<le> N \<Longrightarrow> sum_list (map rsize (rdistinct rs {})) \<le> |
30 (card (sizeNregex N))* N" |
30 (card (sizeNregex N))* N" |
31 |
31 |
|
32 sorry |
|
33 |
|
34 |
|
35 lemma star_lambda_ders: |
|
36 shows " \<forall>s. rsize (rders_simp r0 s) \<le> N \<Longrightarrow> |
|
37 \<forall>r\<in>set (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0)) (star_updates s r0 [[c]])). |
|
38 rsize r \<le> Suc (N + rsize (RSTAR r0))" |
32 sorry |
39 sorry |
33 |
40 |
34 |
41 |
35 lemma star_control_bounded: |
42 lemma star_control_bounded: |
36 shows "\<forall>s. rsize (rders_simp r0 s) \<le> N \<Longrightarrow> |
43 shows "\<forall>s. rsize (rders_simp r0 s) \<le> N \<Longrightarrow> |
37 (sum_list (map rsize (rdistinct (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0)) |
44 (sum_list (map rsize (rdistinct (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0)) |
38 (star_updates s r0 [[c]]) ) {}) ) ) \<le> |
45 (star_updates s r0 [[c]]) ) {}) ) ) \<le> |
39 (card (sizeNregex (Suc (N + rsize (RSTAR r0))))) * (Suc (N + rsize (RSTAR r0))) |
46 (card (sizeNregex (Suc (N + rsize (RSTAR r0))))) * (Suc (N + rsize (RSTAR r0))) |
40 " |
47 " |
41 sorry |
48 apply(subgoal_tac "\<forall>r \<in> set (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0)) |
|
49 (star_updates s r0 [[c]]) ). (rsize r ) \<le> Suc (N + rsize (RSTAR r0))") |
|
50 prefer 2 |
|
51 using star_lambda_ders apply blast |
|
52 using distinct_list_rexp_up_to_certain_size_bouded_by_set_enumerating_up_to_that_size by blast |
|
53 |
42 |
54 |
43 lemma star_control_variant: |
55 lemma star_control_variant: |
44 assumes "\<forall>s. rsize (rders_simp r0 s) \<le> N" |
56 assumes "\<forall>s. rsize (rders_simp r0 s) \<le> N" |
45 shows"Suc |
57 shows"Suc |
46 (sum_list (map rsize (rdistinct (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0)) |
58 (sum_list (map rsize (rdistinct (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0)) |
76 (rdistinct (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0)) (star_updates list r0 [[a]])) {}))) |
88 (rdistinct (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0)) (star_updates list r0 [[a]])) {}))) |
77 \<le> (Suc (card (sizeNregex (Suc (N + rsize (RSTAR r0))))) * Suc (N + rsize (RSTAR r0))) ") |
89 \<le> (Suc (card (sizeNregex (Suc (N + rsize (RSTAR r0))))) * Suc (N + rsize (RSTAR r0))) ") |
78 apply auto[1] |
90 apply auto[1] |
79 using star_control_variant by blast |
91 using star_control_variant by blast |
80 |
92 |
81 |
93 lemma alts_simp_ineq_unfold: |
|
94 shows "rsize (rsimp (RALTS rs)) \<le> Suc (sum_list (map rsize (rdistinct (rflts (map rsimp rs)) {})))" |
|
95 using rsimp_aalts_smaller by auto |
|
96 |
|
97 lemma flts_has_no_zero: |
|
98 shows "rdistinct (rflts rs) rset = rdistinct (rflts rs) (insert RZERO rset)" |
|
99 sorry |
|
100 |
|
101 lemma flts_vs_nflts: |
|
102 shows "\<forall>r \<in> noalts_set. \<forall>xs. r \<noteq> RALTS xs |
|
103 \<and> (\<forall>a \<in> alts_set. \<exists>xs. a = RALTS xs \<and> set xs \<subseteq> corr_set) |
|
104 \<Longrightarrow> Suc (sum_list (map rsize (rdistinct ( rflts rs) (noalts_set \<union> corr_set) ))) |
|
105 \<le> Suc (sum_list (map rsize (rdistinct rs (noalts_set \<union> alts_set) )))" |
|
106 apply(induct rs arbitrary: noalts_set) |
|
107 apply simp |
|
108 |
|
109 sorry |
|
110 |
|
111 |
|
112 lemma without_flts_ineq: |
|
113 shows " Suc (sum_list (map rsize (rdistinct (rflts rs) {}) )) \<le> |
|
114 Suc (sum_list (map rsize (rdistinct ( rs ) {} )))" |
|
115 by (metis empty_iff flts_vs_nflts sup_bot_left) |
|
116 |
|
117 |
|
118 lemma distinct_simp_ineq: |
|
119 shows "Suc (sum_list (map rsize (rdistinct (map rsimp rs) {}))) |
|
120 \<le> Suc (sum_list (map rsize (rdistinct rs {})))" |
|
121 sorry |
|
122 |
|
123 |
|
124 lemma alts_simp_control: |
|
125 shows "rsize (rsimp (RALTS rs)) \<le> Suc (sum_list (map rsize (rdistinct rs {})))" |
|
126 proof - |
|
127 have "rsize (rsimp (RALTS rs)) \<le> Suc (sum_list (map rsize (rdistinct (rflts (map rsimp rs)) {})))" |
|
128 |
|
129 using alts_simp_ineq_unfold by auto |
|
130 then have "\<dots> \<le> Suc (sum_list (map rsize (rdistinct (map rsimp rs) {})))" |
|
131 using without_flts_ineq by blast |
|
132 |
|
133 show "rsize (rsimp (RALTS rs)) \<le> Suc (sum_list (map rsize (rdistinct rs {})))" |
|
134 by (meson \<open>Suc (sum_list (map rsize (rdistinct (rflts (map rsimp rs)) {}))) \<le> Suc (sum_list (map rsize (rdistinct (map rsimp rs) {})))\<close> \<open>rsize (rsimp (RALTS rs)) \<le> Suc (sum_list (map rsize (rdistinct (rflts (map rsimp rs)) {})))\<close> distinct_simp_ineq order_trans) |
|
135 qed |
82 |
136 |
83 |
137 |
84 |
138 |
85 |
139 |
86 lemma seq_list_estimate_control: shows |
140 lemma seq_list_estimate_control: shows |
87 " rsize (rsimp (RALTS (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)))) |
141 " rsize (rsimp (RALTS (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)))) |
88 \<le> Suc (sum_list (map rsize (rdistinct (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)) {})))" |
142 \<le> Suc (sum_list (map rsize (rdistinct (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)) {})))" |
89 |
143 by(metis alts_simp_control) |
90 sorry |
|
91 |
144 |
92 lemma rdistinct_equality1: |
145 lemma rdistinct_equality1: |
93 shows "a \<notin> ss \<Longrightarrow> rdistinct (a # rs) ss = a # rdistinct rs (insert a ss) " |
146 shows "a \<notin> ss \<Longrightarrow> rdistinct (a # rs) ss = a # rdistinct rs (insert a ss) " |
94 by auto |
147 by auto |
95 |
148 |
113 by blast |
166 by blast |
114 |
167 |
115 |
168 |
116 lemma larger_acc_smaller_distinct_res: |
169 lemma larger_acc_smaller_distinct_res: |
117 shows " (sum_list (map rsize (rdistinct rs ss))) \<ge> (sum_list (map rsize (rdistinct rs (insert a ss))))" |
170 shows " (sum_list (map rsize (rdistinct rs ss))) \<ge> (sum_list (map rsize (rdistinct rs (insert a ss))))" |
118 sorry |
171 apply(subgoal_tac "ss \<subseteq> (insert a ss)") |
|
172 apply(rule larger_acc_smaller_distinct_res0) |
|
173 apply simp |
|
174 by (simp add: subset_insertI) |
119 |
175 |
120 lemma size_list_triangle1: |
176 lemma size_list_triangle1: |
121 shows "sum_list (map rsize (a # (rdistinct as ss))) \<ge> rsize a + sum_list (map rsize (rdistinct as (insert a ss)))" |
177 shows "sum_list (map rsize (a # (rdistinct as ss))) \<ge> rsize a + sum_list (map rsize (rdistinct as (insert a ss)))" |
122 by (simp add: larger_acc_smaller_distinct_res) |
178 by (simp add: larger_acc_smaller_distinct_res) |
123 |
179 |