701 |
701 |
702 lemma RL_rerase_dB: |
702 lemma RL_rerase_dB: |
703 shows "(\<Union> (RL ` rerase ` (set (distinctBy rs rerase {})))) = \<Union> (RL ` rerase ` (set rs))" |
703 shows "(\<Union> (RL ` rerase ` (set (distinctBy rs rerase {})))) = \<Union> (RL ` rerase ` (set rs))" |
704 by (metis RL_rerase_dB_acc Un_commute Union_image_empty) |
704 by (metis RL_rerase_dB_acc Un_commute Union_image_empty) |
705 |
705 |
706 (* |
|
707 lemma L_bsimp_erase: |
|
708 shows "L (erase r) = L (erase (bsimp r))" |
|
709 apply(induct r) |
|
710 apply(simp) |
|
711 apply(simp) |
|
712 apply(simp) |
|
713 apply(auto simp add: Sequ_def)[1] |
|
714 apply(subst L_bsimp_ASEQ[symmetric]) |
|
715 apply(auto simp add: Sequ_def)[1] |
|
716 apply(subst (asm) L_bsimp_ASEQ[symmetric]) |
|
717 apply(auto simp add: Sequ_def)[1] |
|
718 apply(simp) |
|
719 apply(subst L_bsimp_AALTs[symmetric]) |
|
720 defer |
|
721 apply(simp) |
|
722 apply(subst (2)L_erase_AALTs) |
|
723 apply(subst L_erase_dB) |
|
724 apply(subst L_erase_flts) |
|
725 apply (simp add: L_erase_AALTs) |
|
726 done |
|
727 *) |
|
728 |
706 |
729 lemma RL_bsimp_rerase: |
707 lemma RL_bsimp_rerase: |
730 shows "RL (rerase r) = RL (rerase (bsimp r))" |
708 shows "RL (rerase r) = RL (rerase (bsimp r))" |
731 apply(induct r) |
709 apply(induct r) |
732 apply(simp) |
710 apply(simp) |
1874 using SizeBound3.flts3b distinctBy.elims apply force |
1853 using SizeBound3.flts3b distinctBy.elims apply force |
1875 apply(subgoal_tac " Ball (set ( (flts (bsimp a # map bsimp list)))) anonalt") |
1854 apply(subgoal_tac " Ball (set ( (flts (bsimp a # map bsimp list)))) anonalt") |
1876 prefer 2 |
1855 prefer 2 |
1877 apply (metis Cons_eq_map_conv SizeBound3.nn1b SizeBound3.nn1c ex_map_conv) |
1856 apply (metis Cons_eq_map_conv SizeBound3.nn1b SizeBound3.nn1c ex_map_conv) |
1878 using dB_keeps_property apply presburger |
1857 using dB_keeps_property apply presburger |
1879 sledgehammer |
1858 |
1880 |
1859 |
1881 using dB_does_more_job apply presburger |
1860 using dB_does_more_job apply presburger |
1882 apply(subgoal_tac " Ball (set ( (flts (bsimp a # map bsimp list)) )) agood") |
1861 apply(subgoal_tac " Ball (set ( (flts (bsimp a # map bsimp list)) )) agood") |
1883 using dB_keeps_property apply presburger |
1862 using dB_keeps_property apply presburger |
1884 apply(subgoal_tac "\<forall>r \<in> (set (bsimp a # map bsimp list)). (agood r) \<or> (r = AZERO)") |
1863 apply(subgoal_tac "\<forall>r \<in> (set (bsimp a # map bsimp list)). (agood r) \<or> (r = AZERO)") |
2034 apply(auto)[1] |
2013 apply(auto)[1] |
2035 using agood.simps(1) k0b apply blast |
2014 using agood.simps(1) k0b apply blast |
2036 apply(auto)[1] |
2015 apply(auto)[1] |
2037 done |
2016 done |
2038 |
2017 |
2039 lemma test: |
|
2040 assumes "agood r" |
|
2041 shows "bsimp r = r" |
|
2042 using assms |
|
2043 apply(induct r taking: "asize" rule: measure_induct) |
|
2044 apply(erule agood.elims) |
|
2045 apply(simp_all) |
|
2046 apply(subst k0) |
|
2047 apply(subst (2) k0) |
|
2048 apply(subst flts_qq) |
|
2049 apply(auto)[1] |
|
2050 apply(auto)[1] |
|
2051 oops |
|
2052 |
|
2053 |
|
2054 |
|
2055 lemma bsimp_idem: |
|
2056 shows "bsimp (bsimp r) = bsimp r" |
|
2057 using test good1 |
|
2058 oops |
|
2059 |
|
2060 (* |
|
2061 lemma erase_preimage1: |
|
2062 assumes "anonalt r" |
|
2063 shows "erase r = ONE \<Longrightarrow> \<exists>bs. r = AONE bs" |
|
2064 apply(case_tac r) |
|
2065 apply simp+ |
|
2066 using anonalt.simps(1) assms apply presburger |
|
2067 by fastforce |
|
2068 |
|
2069 lemma erase_preimage_char: |
|
2070 assumes "anonalt r" |
|
2071 shows "erase r = CH c \<Longrightarrow> \<exists>bs. r = ACHAR bs c" |
|
2072 apply(case_tac r) |
|
2073 apply simp+ |
|
2074 using assms apply fastforce |
|
2075 by simp |
|
2076 |
|
2077 lemma erase_preimage_seq: |
|
2078 assumes "anonalt r" |
|
2079 shows "erase r = SEQ r1 r2 \<Longrightarrow> \<exists>bs a1 a2. r = ASEQ bs a1 a2 \<and> erase a1 = r1 \<and> erase a2 = r2" |
|
2080 apply(case_tac r) |
|
2081 apply simp+ |
|
2082 using assms apply fastforce |
|
2083 by simp |
|
2084 |
|
2085 lemma rerase_preimage_seq: |
|
2086 assumes "anonalt r" |
|
2087 shows "rerase r = RSEQ r1 r2 \<Longrightarrow> \<exists>bs a1 a2. r = ASEQ bs a1 a2 \<and> rerase a1 = r1 \<and> rerase a2 = r2 " |
|
2088 using rerase_preimage4 by presburger |
|
2089 |
|
2090 lemma seq_recursive_equality: |
|
2091 shows "\<lbrakk>r1 = a1; r2 = a2\<rbrakk> \<Longrightarrow> SEQ r1 r2 = SEQ a1 a2" |
|
2092 by meson |
|
2093 |
|
2094 lemma almost_identical_image: |
|
2095 assumes "agood r" "\<forall>r \<in> rset. agood r" |
|
2096 shows "erase r \<in> erase ` rset \<Longrightarrow> \<exists>r' \<in> rset. erase r' = erase r" |
|
2097 by auto |
|
2098 |
|
2099 lemma goodalts_never_change: |
|
2100 assumes "r = AALTs bs rs" "agood r" |
|
2101 shows "\<exists>r1 r2. erase r = ALT r1 r2" |
|
2102 by (metis agood.simps(4) agood.simps(5) assms(1) assms(2) bmkepss.cases erase.simps(6)) |
|
2103 |
|
2104 |
|
2105 fun shape_preserving :: "arexp \<Rightarrow> bool" where |
|
2106 "shape_preserving AZERO = True" |
|
2107 | "shape_preserving (AONE bs) = True" |
|
2108 | "shape_preserving (ACHAR bs c) = True" |
|
2109 | "shape_preserving (AALTs bs []) = False" |
|
2110 | "shape_preserving (AALTs bs [a]) = False" |
|
2111 | "shape_preserving (AALTs bs (a1 # a2 # rs)) = (\<forall>r \<in> set (a1 # a2 # rs). shape_preserving r)" |
|
2112 | "shape_preserving (ASEQ bs r1 r2) = (shape_preserving r1 \<and> shape_preserving r2)" |
|
2113 | "shape_preserving (ASTAR bs r) = shape_preserving r" |
|
2114 |
|
2115 |
|
2116 lemma good_shape_preserving: |
|
2117 assumes "\<nexists>bs r0. r = ASTAR bs r0" |
|
2118 shows "agood r \<Longrightarrow> shape_preserving r" |
|
2119 using assms |
|
2120 |
|
2121 apply(induct r) |
|
2122 prefer 6 |
|
2123 |
|
2124 apply blast |
|
2125 apply simp |
|
2126 |
|
2127 oops |
|
2128 |
|
2129 |
|
2130 |
|
2131 |
|
2132 |
|
2133 lemma shadow_arexp_rerase_erase: |
|
2134 shows "\<lbrakk>agood r; agood r'; erase r = erase r'\<rbrakk> \<Longrightarrow> rerase r = rerase r'" |
|
2135 apply(induct r ) |
|
2136 apply simp |
|
2137 apply(induct r') |
|
2138 apply simp+ |
|
2139 apply (metis goodalts_never_change rexp.distinct(15)) |
|
2140 apply simp+ |
|
2141 apply (metis anonalt.elims(3) erase_preimage_char goodalts_never_change rerase.simps(3) rexp.distinct(21)) |
|
2142 apply(induct r') |
|
2143 apply simp |
|
2144 apply simp |
|
2145 apply simp |
|
2146 apply(subgoal_tac "agood r1") |
|
2147 prefer 2 |
|
2148 apply (metis SizeBound3.good_SEQ agood.simps(10) agood.simps(11) agood.simps(2) agood.simps(3) agood.simps(33) agood.simps(7) bsimp.cases) |
|
2149 apply(subgoal_tac "agood r2") |
|
2150 apply(subgoal_tac "agood r'1") |
|
2151 apply(subgoal_tac "agood r'2") |
|
2152 apply(subgoal_tac "rerase r'1 = rerase r1") |
|
2153 apply(subgoal_tac "rerase r'2 = rerase r2") |
|
2154 |
|
2155 using rerase.simps(5) apply presburger |
|
2156 oops |
|
2157 |
|
2158 |
|
2159 |
|
2160 lemma rerase_erase_good: |
|
2161 assumes "agood r" "\<forall>r \<in> rset. agood r" |
|
2162 shows "erase r \<in> erase ` rset \<Longrightarrow> rerase r \<in> rerase ` rset" |
|
2163 using assms |
|
2164 apply(case_tac r) |
|
2165 apply simp+ |
|
2166 oops |
|
2167 |
|
2168 lemma rerase_erase_both: |
|
2169 assumes "\<forall>r \<in> rset. agood r" "agood r" |
|
2170 shows "(rerase r \<in> (rerase ` rset)) \<longleftrightarrow> (erase r \<in> (erase ` rset))" |
|
2171 using assms |
|
2172 apply(induct r ) |
|
2173 apply force |
|
2174 apply simp |
|
2175 apply(case_tac "RONE \<in> rerase ` rset") |
|
2176 apply(subgoal_tac "\<exists>bs. (AONE bs) \<in> rset") |
|
2177 apply (metis erase.simps(2) rev_image_eqI) |
|
2178 apply (metis image_iff rerase_preimage2) |
|
2179 apply(subgoal_tac "\<nexists>bs. (AONE bs) \<in> rset") |
|
2180 apply(subgoal_tac "ONE \<notin> erase ` rset") |
|
2181 |
|
2182 apply blast |
|
2183 sledgehammer |
|
2184 apply (metis erase_preimage1 image_iff) |
|
2185 apply (metis rerase.simps(2) rev_image_eqI) |
|
2186 apply (smt (verit, best) erase.simps(3) erase_preimage_char image_iff rerase.simps(3) rerase_preimage3) |
|
2187 (* apply simp |
|
2188 apply(subgoal_tac "(RSEQ (rerase r1) (rerase r2) \<in> rerase ` rset) \<Longrightarrow> (SEQ (erase r1) (erase r2) \<in> erase ` rset)") |
|
2189 prefer 2 |
|
2190 apply(subgoal_tac "\<exists>bs a1 a2. (ASEQ bs a1 a2) \<in> rset \<and> rerase a1 = rerase r1 \<and> rerase a2 = rerase r2") |
|
2191 prefer 2 |
|
2192 apply (metis (full_types) image_iff rerase_preimage4) |
|
2193 apply(erule exE)+ |
|
2194 apply(subgoal_tac "erase (ASEQ bs a1 a2) \<in> (erase ` rset) ") |
|
2195 apply(subgoal_tac "SEQ (erase a1) (erase a2) \<in> (erase ` rset)") |
|
2196 apply(subgoal_tac "SEQ (erase a1) (erase a2) = SEQ (erase r1) (erase r2)") |
|
2197 apply metis |
|
2198 apply(erule conjE)+*) |
|
2199 apply(drule_tac x = "rset" in meta_spec)+ |
|
2200 |
|
2201 |
|
2202 |
|
2203 |
|
2204 oops |
|
2205 |
|
2206 |
|
2207 lemma rerase_pushin1_general: |
|
2208 assumes "\<forall>r \<in> set rs. agood r" |
|
2209 shows "map rerase (distinctBy rs erase (erase ` rset)) = rdistinct (map rerase rs) (rerase ` rset)" |
|
2210 apply(induct rs arbitrary: rset) |
|
2211 apply simp+ |
|
2212 apply(case_tac "erase a \<in> erase ` rset") |
|
2213 apply simp |
|
2214 |
|
2215 |
|
2216 |
|
2217 oops |
|
2218 |
|
2219 lemma rerase_erase: |
|
2220 assumes "\<forall>r \<in> set as. agood r \<and> anonalt r" |
|
2221 shows "rdistinct (map rerase as) (rerase ` rset) = map rerase (distinctBy as erase (erase ` rset))" |
|
2222 using assms |
|
2223 apply(induct as) |
|
2224 apply simp+ |
|
2225 |
|
2226 sorry |
|
2227 |
|
2228 |
|
2229 lemma rerase_pushin1: |
|
2230 assumes "\<forall>r \<in> set rs. anonalt r \<and> agood r" |
|
2231 shows "map rerase (distinctBy rs erase {}) = rdistinct (map rerase rs) {}" |
|
2232 apply(insert rerase_erase) |
|
2233 by (metis assms image_empty) |
|
2234 |
|
2235 *) |
|
2236 |
2018 |
2237 |
2019 |
2238 |
2020 |
2239 |
2021 |
2240 |
2022 |