equal
deleted
inserted
replaced
113 shows " Suc (sum_list (map rsize (rdistinct (rflts rs) {}) )) \<le> |
113 shows " Suc (sum_list (map rsize (rdistinct (rflts rs) {}) )) \<le> |
114 Suc (sum_list (map rsize (rdistinct ( rs ) {} )))" |
114 Suc (sum_list (map rsize (rdistinct ( rs ) {} )))" |
115 by (metis empty_iff flts_vs_nflts sup_bot_left) |
115 by (metis empty_iff flts_vs_nflts sup_bot_left) |
116 |
116 |
117 |
117 |
|
118 lemma distinct_simp_ineq_general: |
|
119 shows "rsimp ` no_simp = has_simp \<Longrightarrow>Suc (sum_list (map rsize (rdistinct (map rsimp rs) has_simp))) |
|
120 \<le> Suc (sum_list (map rsize (rdistinct rs no_simp)))" |
|
121 sorry |
|
122 |
|
123 |
118 lemma distinct_simp_ineq: |
124 lemma distinct_simp_ineq: |
119 shows "Suc (sum_list (map rsize (rdistinct (map rsimp rs) {}))) |
125 shows "Suc (sum_list (map rsize (rdistinct (map rsimp rs) {}))) |
120 \<le> Suc (sum_list (map rsize (rdistinct rs {})))" |
126 \<le> Suc (sum_list (map rsize (rdistinct rs {})))" |
121 sorry |
127 |
|
128 using distinct_simp_ineq_general by blast |
|
129 |
|
130 |
122 |
131 |
123 |
132 |
124 lemma alts_simp_control: |
133 lemma alts_simp_control: |
125 shows "rsize (rsimp (RALTS rs)) \<le> Suc (sum_list (map rsize (rdistinct rs {})))" |
134 shows "rsize (rsimp (RALTS rs)) \<le> Suc (sum_list (map rsize (rdistinct rs {})))" |
126 proof - |
135 proof - |