2063 prefer 2 |
2063 prefer 2 |
2064 apply presburger |
2064 apply presburger |
2065 apply(subst stupdates_append[symmetric]) |
2065 apply(subst stupdates_append[symmetric]) |
2066 using stupdates_join_general by blast |
2066 using stupdates_join_general by blast |
2067 |
2067 |
2068 |
2068 lemma starders_hfau_also1: |
2069 |
2069 shows "hflat_aux (rders (RSTAR r) (c # xs)) = map (\<lambda>s1. RSEQ (rders r s1) (RSTAR r)) (star_updates xs r [[c]])" |
2070 lemma star_closed_form_seq2: |
2070 using star_hfau_induct by force |
2071 shows "RSEQ (rders (rder c r0) s) (RSTAR r0) # map (rders (RSTAR r0)) (vsuf s (rder c r0)) = |
2071 |
2072 map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates s r0 [[c]])" |
2072 lemma hflat_aux_grewrites: |
2073 apply(induct s rule: rev_induct) |
2073 shows "a # rs \<leadsto>g* hflat_aux a @ rs" |
2074 apply simp |
2074 apply(induct a arbitrary: rs) |
2075 apply(subst rders_append)+ |
2075 apply simp+ |
2076 apply(case_tac "rnullable (rder c r0)") |
2076 apply(case_tac x) |
2077 apply simp |
2077 apply simp |
2078 |
2078 apply(case_tac list) |
|
2079 |
|
2080 apply (metis append.right_neutral append_Cons append_eq_append_conv2 grewrites.simps hflat_aux.simps(7) same_append_eq) |
|
2081 apply(case_tac lista) |
|
2082 apply simp |
|
2083 apply (metis (no_types, lifting) append_Cons append_eq_append_conv2 gmany_steps_later greal_trans grewrite.intros(2) grewrites_append self_append_conv) |
|
2084 apply simp |
|
2085 by simp |
|
2086 |
|
2087 |
|
2088 |
|
2089 |
|
2090 lemma cbs_hfau_rsimpeq1: |
|
2091 shows "rsimp (RALT a b) = rsimp (RALTS ((hflat_aux a) @ (hflat_aux b)))" |
|
2092 apply(subgoal_tac "[a, b] \<leadsto>g* hflat_aux a @ hflat_aux b") |
|
2093 using grewrites_equal_rsimp apply presburger |
2079 sorry |
2094 sorry |
2080 |
2095 |
2081 |
2096 |
|
2097 lemma hfau_rsimpeq2: |
|
2098 shows "created_by_star r \<Longrightarrow> rsimp r = rsimp ( (RALTS (hflat_aux r)))" |
|
2099 apply(induct r) |
|
2100 apply simp+ |
|
2101 |
|
2102 apply (metis rsimp_seq_equal1) |
|
2103 prefer 2 |
|
2104 apply simp |
|
2105 apply(case_tac x) |
|
2106 apply simp |
|
2107 apply(case_tac "list") |
|
2108 apply simp |
|
2109 |
|
2110 apply (metis idem_after_simp1) |
|
2111 apply(case_tac "lista") |
|
2112 prefer 2 |
|
2113 apply (metis hflat_aux.simps(8) idem_after_simp1 list.simps(8) list.simps(9) rsimp.simps(2)) |
|
2114 apply(subgoal_tac "rsimp (RALT a aa) = rsimp (RALTS (hflat_aux (RALT a aa)))") |
|
2115 apply simp |
|
2116 apply(subgoal_tac "rsimp (RALT a aa) = rsimp (RALTS (hflat_aux a @ hflat_aux aa))") |
|
2117 using hflat_aux.simps(1) apply presburger |
|
2118 apply simp |
|
2119 using cbs_hfau_rsimpeq1 by fastforce |
|
2120 |
|
2121 |
|
2122 lemma hfau_rsimpeq1: |
|
2123 shows "created_by_star r \<Longrightarrow> hflat_aux r = rs \<Longrightarrow> rsimp r = rsimp (RALTS rs)" |
|
2124 apply(induct r arbitrary: rs rule: created_by_star.induct ) |
|
2125 apply (metis created_by_seq.intros(1) hflat_aux.simps(5) sflat_aux.simps(6) sflat_rsimpeq) |
|
2126 apply simp |
|
2127 oops |
|
2128 |
|
2129 |
|
2130 |
|
2131 |
|
2132 |
|
2133 |
2082 lemma star_closed_form1: |
2134 lemma star_closed_form1: |
2083 shows "rders (RSTAR r0) (c#s) = |
2135 shows "rsimp (rders (RSTAR r0) (c#s)) = |
2084 ( RALTS ( (map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0) ) (star_updates s r0 [[c]]) ) ))" |
2136 rsimp ( ( RALTS ( (map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0) ) (star_updates s r0 [[c]]) ) )))" |
2085 |
2137 using hfau_rsimpeq2 rder.simps(6) rders.simps(2) star_ders_cbs starders_hfau_also1 by presburger |
2086 |
2138 |
2087 sorry |
2139 lemma star_closed_form2: |
|
2140 shows "rsimp (rders_simp (RSTAR r0) (c#s)) = |
|
2141 rsimp ( ( RALTS ( (map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0) ) (star_updates s r0 [[c]]) ) )))" |
|
2142 by (metis list.distinct(1) rders_simp_same_simpders rsimp_idem star_closed_form1) |
|
2143 |
|
2144 lemma star_closed_form3: |
|
2145 shows "rsimp (rders_simp (RSTAR r0) (c#s)) = (rders_simp (RSTAR r0) (c#s))" |
|
2146 by (metis list.distinct(1) rders_simp_same_simpders star_closed_form1 star_closed_form2) |
|
2147 |
|
2148 lemma star_closed_form4: |
|
2149 shows " (rders_simp (RSTAR r0) (c#s)) = |
|
2150 rsimp ( ( RALTS ( (map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0) ) (star_updates s r0 [[c]]) ) )))" |
|
2151 using star_closed_form2 star_closed_form3 by presburger |
|
2152 |
|
2153 lemma star_closed_form5: |
|
2154 shows " rsimp ( ( RALTS ( (map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0) ) Ss )))) = |
|
2155 rsimp ( ( RALTS ( (map (\<lambda>s1. rsimp (RSEQ (rders r0 s1) (RSTAR r0)) ) Ss ))))" |
|
2156 by (metis (mono_tags, lifting) list.map_comp map_eq_conv o_apply rsimp.simps(2) rsimp_idem) |
|
2157 |
|
2158 lemma star_closed_form6_hrewrites: |
|
2159 shows " |
|
2160 (map (\<lambda>s1. (RSEQ (rsimp (rders r0 s1)) (RSTAR r0)) ) Ss ) |
|
2161 scf\<leadsto>* |
|
2162 (map (\<lambda>s1. rsimp (RSEQ (rders r0 s1) (RSTAR r0)) ) Ss )" |
|
2163 apply(induct Ss) |
|
2164 apply simp |
|
2165 apply (simp add: ss1) |
|
2166 by (metis (no_types, lifting) list.simps(9) rsimp.simps(1) rsimp_idem simp_hrewrites ss2) |
|
2167 |
|
2168 lemma star_closed_form6: |
|
2169 shows " rsimp ( ( RALTS ( (map (\<lambda>s1. rsimp (RSEQ (rders r0 s1) (RSTAR r0)) ) Ss )))) = |
|
2170 rsimp ( ( RALTS ( (map (\<lambda>s1. (RSEQ (rsimp (rders r0 s1)) (RSTAR r0)) ) Ss ))))" |
|
2171 apply(subgoal_tac " map (\<lambda>s1. (RSEQ (rsimp (rders r0 s1)) (RSTAR r0)) ) Ss scf\<leadsto>* |
|
2172 map (\<lambda>s1. rsimp (RSEQ (rders r0 s1) (RSTAR r0)) ) Ss ") |
|
2173 using hrewrites_simpeq srewritescf_alt1 apply fastforce |
|
2174 using star_closed_form6_hrewrites by blast |
|
2175 |
|
2176 lemma star_closed_form7: |
|
2177 shows " (rders_simp (RSTAR r0) (c#s)) = |
|
2178 rsimp ( ( RALTS ( (map (\<lambda>s1. RSEQ (rsimp (rders r0 s1)) (RSTAR r0) ) (star_updates s r0 [[c]]) ) )))" |
|
2179 using star_closed_form4 star_closed_form5 star_closed_form6 by presburger |
|
2180 |
|
2181 lemma derssimp_nonempty_list: |
|
2182 shows "\<forall>s \<in> set Ss. s \<noteq> [] \<Longrightarrow> |
|
2183 rsimp ( ( RALTS ( (map (\<lambda>s1. RSEQ (rsimp (rders r0 s1)) (RSTAR r0) ) Ss)))) = |
|
2184 rsimp ( ( RALTS ( (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) Ss)))) " |
|
2185 |
|
2186 by (metis (no_types, lifting) map_eq_conv rders_simp_same_simpders) |
|
2187 |
|
2188 lemma stupdate_nonempty: |
|
2189 shows "\<forall>s \<in> set Ss. s \<noteq> [] \<Longrightarrow> \<forall>s \<in> set (star_update c r Ss). s \<noteq> []" |
|
2190 apply(induct Ss) |
|
2191 apply simp |
|
2192 apply(case_tac "rnullable (rders r a)") |
|
2193 apply simp+ |
|
2194 done |
|
2195 |
|
2196 |
|
2197 lemma stupdates_nonempty: |
|
2198 shows "\<forall>s \<in> set Ss. s\<noteq> [] \<Longrightarrow> \<forall>s \<in> set (star_updates s r Ss). s \<noteq> []" |
|
2199 apply(induct s arbitrary: Ss) |
|
2200 apply simp |
|
2201 apply simp |
|
2202 using stupdate_nonempty by presburger |
|
2203 |
|
2204 |
|
2205 |
|
2206 |
|
2207 lemma star_closed_form8: |
|
2208 shows |
|
2209 "rsimp ( ( RALTS ( (map (\<lambda>s1. RSEQ (rsimp (rders r0 s1)) (RSTAR r0) ) (star_updates s r0 [[c]]) ) ))) = |
|
2210 rsimp ( ( RALTS ( (map (\<lambda>s1. RSEQ ( (rders_simp r0 s1)) (RSTAR r0) ) (star_updates s r0 [[c]]) ) )))" |
|
2211 by (metis derssimp_nonempty_list neq_Nil_conv non_empty_list set_ConsD stupdates_nonempty) |
|
2212 |
|
2213 |
2088 |
2214 |
2089 lemma star_closed_form: |
2215 lemma star_closed_form: |
2090 shows "rders_simp (RSTAR r0) (c#s) = |
2216 shows "rders_simp (RSTAR r0) (c#s) = |
2091 rsimp ( RALTS ( (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) (star_updates s r0 [[c]]) ) ))" |
2217 rsimp ( RALTS ( (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) (star_updates s r0 [[c]]) ) ))" |
2092 apply(induct s) |
2218 apply(induct s) |
2093 apply simp |
2219 apply simp |
2094 apply (metis idem_after_simp1 rsimp.simps(1) rsimp.simps(6) rsimp_idem) |
2220 apply (metis idem_after_simp1 rsimp.simps(1) rsimp.simps(6) rsimp_idem) |
2095 |
2221 using star_closed_form4 star_closed_form5 star_closed_form6 star_closed_form8 by presburger |
2096 |
|
2097 sorry |
|
2098 |
2222 |
2099 |
2223 |
2100 lemma simp_helps_der_pierce: |
2224 lemma simp_helps_der_pierce: |
2101 shows " rsimp |
2225 shows " rsimp |
2102 (rder x |
2226 (rder x |