87 " rsize (rsimp (RALTS (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)))) |
87 " 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)) {})))" |
88 \<le> Suc (sum_list (map rsize (rdistinct (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)) {})))" |
89 |
89 |
90 sorry |
90 sorry |
91 |
91 |
|
92 lemma rdistinct_equality1: |
|
93 shows "a \<notin> ss \<Longrightarrow> rdistinct (a # rs) ss = a # rdistinct rs (insert a ss) " |
|
94 by auto |
|
95 |
|
96 lemma larger_acc_smaller_distinct_res0: |
|
97 shows " ss \<subseteq> SS \<Longrightarrow> sum_list (map rsize (rdistinct rs SS)) \<le> sum_list (map rsize (rdistinct rs ss))" |
|
98 apply(induct rs arbitrary: ss SS) |
|
99 apply simp |
|
100 apply(case_tac "a \<in> ss") |
|
101 apply(subgoal_tac "a \<in> SS") |
|
102 apply simp |
|
103 apply blast |
|
104 apply(case_tac "a \<in> SS") |
|
105 apply simp |
|
106 apply(subgoal_tac "insert a ss \<subseteq> SS") |
|
107 apply simp |
|
108 apply (simp add: trans_le_add2) |
|
109 apply blast |
|
110 apply(simp) |
|
111 apply(subgoal_tac "insert a ss \<subseteq> insert a SS") |
|
112 apply blast |
|
113 by blast |
|
114 |
|
115 |
|
116 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))))" |
|
118 sorry |
|
119 |
|
120 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)))" |
|
122 by (simp add: larger_acc_smaller_distinct_res) |
|
123 |
|
124 |
92 lemma triangle_inequality_distinct: |
125 lemma triangle_inequality_distinct: |
93 shows "sum_list (map rsize (rdistinct (a # rs) ss)) \<le> rsize a + (sum_list (map rsize (rdistinct rs ss)))" |
126 shows "sum_list (map rsize (rdistinct (a # rs) ss)) \<le> rsize a + (sum_list (map rsize (rdistinct rs ss)))" |
94 apply(arbitrary: ss) |
|
95 apply simp |
|
96 apply(case_tac "a \<in> ss") |
127 apply(case_tac "a \<in> ss") |
97 apply simp |
128 apply simp |
98 |
129 apply(subst rdistinct_equality1) |
99 sorry |
130 apply simp |
|
131 using size_list_triangle1 by auto |
100 |
132 |
101 lemma same_regex_property_after_map: |
133 lemma same_regex_property_after_map: |
102 shows "\<forall>s. P (f r2 s) \<Longrightarrow> \<forall>r \<in> set (map (f r2) Ss). P r" |
134 shows "\<forall>s. P (f r2 s) \<Longrightarrow> \<forall>r \<in> set (map (f r2) Ss). P r" |
103 by auto |
135 by auto |
104 |
136 |