1 

     2 theory FBound

     3   imports "BlexerSimp" "ClosedFormsBounds"

     4 begin

     5 

     6 fun distinctBy :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b set \<Rightarrow> 'a list"

     7   where

     8   "distinctBy [] f acc = []"

     9 | "distinctBy (x#xs) f acc = 

    10      (if (f x) \<in> acc then distinctBy xs f acc 

    11       else x # (distinctBy xs f ({f x} \<union> acc)))"

    12 

    13 fun rerase :: "arexp \<Rightarrow> rrexp"

    14 where

    15   "rerase AZERO = RZERO"

    16 | "rerase (AONE _) = RONE"

    17 | "rerase (ACHAR _ c) = RCHAR c"

    18 | "rerase (AALTs bs rs) = RALTS (map rerase rs)"

    19 | "rerase (ASEQ _ r1 r2) = RSEQ (rerase r1) (rerase r2)"

    20 | "rerase (ASTAR _ r) = RSTAR (rerase r)"

    21 | "rerase (ANTIMES _ r n) = RNTIMES (rerase r) n"

    22 

    23 lemma eq1_rerase:

    24   shows "x ~1 y \<longleftrightarrow> (rerase x) = (rerase y)"

    25   apply(induct x y rule: eq1.induct)

    26   apply(auto)

    27   done

    28 

    29 

    30 lemma distinctBy_distinctWith:

    31   shows "distinctBy xs f (f ` acc) = distinctWith xs (\<lambda>x y. f x = f y) acc"

    32   apply(induct xs arbitrary: acc)

    33   apply(auto)

    34   by (metis image_insert)

    35 

    36 lemma distinctBy_distinctWith2:

    37   shows "distinctBy xs rerase {} = distinctWith xs eq1 {}"

    38   apply(subst distinctBy_distinctWith[of _ _ "{}", simplified])

    39   using eq1_rerase by presburger

    40   

    41 lemma asize_rsize:

    42   shows "rsize (rerase r) = asize r"

    43   apply(induct r rule: rerase.induct)

    44   apply(auto)

    45   apply (metis (mono_tags, lifting) comp_apply map_eq_conv)

    46   done

    47 

    48 lemma rerase_fuse:

    49   shows "rerase (fuse bs r) = rerase r"

    50   apply(induct r)

    51        apply simp+

    52   done

    53 

    54 lemma rerase_bsimp_ASEQ:

    55   shows "rerase (bsimp_ASEQ x1 a1 a2) = rsimp_SEQ (rerase a1) (rerase a2)"

    56   apply(induct x1 a1 a2 rule: bsimp_ASEQ.induct)

    57   apply(auto)

    58   done

    59 

    60 lemma rerase_bsimp_AALTs:

    61   shows "rerase (bsimp_AALTs bs rs) = rsimp_ALTs (map rerase rs)"

    62   apply(induct bs rs rule: bsimp_AALTs.induct)

    63   apply(auto simp add: rerase_fuse)

    64   done

    65 

    66 fun anonalt :: "arexp \<Rightarrow> bool"

    67   where

    68   "anonalt (AALTs bs2 rs) = False"

    69 | "anonalt r = True"

    70 

    71 

    72 fun agood :: "arexp \<Rightarrow> bool" where

    73   "agood AZERO = False"

    74 | "agood (AONE cs) = True" 

    75 | "agood (ACHAR cs c) = True"

    76 | "agood (AALTs cs []) = False"

    77 | "agood (AALTs cs [r]) = False"

    78 | "agood (AALTs cs (r1#r2#rs)) = (distinct (map rerase (r1 # r2 # rs)) \<and>(\<forall>r' \<in> set (r1#r2#rs). agood r' \<and> anonalt r'))"

    79 | "agood (ASEQ _ AZERO _) = False"

    80 | "agood (ASEQ _ (AONE _) _) = False"

    81 | "agood (ASEQ _ _ AZERO) = False"

    82 | "agood (ASEQ cs r1 r2) = (agood r1 \<and> agood r2)"

    83 | "agood (ASTAR cs r) = True"

    84 

    85 

    86 fun anonnested :: "arexp \<Rightarrow> bool"

    87   where

    88   "anonnested (AALTs bs2 []) = True"

    89 | "anonnested (AALTs bs2 ((AALTs bs1 rs1) # rs2)) = False"

    90 | "anonnested (AALTs bs2 (r # rs2)) = anonnested (AALTs bs2 rs2)"

    91 | "anonnested r = True"

    92 

    93 

    94 lemma asize0:

    95   shows "0 < asize r"

    96   apply(induct  r)

    97   apply(auto)

    98   done

    99 

   100 lemma rnullable:

   101   shows "rnullable (rerase r) = bnullable r"

   102   apply(induct r rule: rerase.induct)

   103   apply(auto)

   104   done

   105 

   106 lemma rder_bder_rerase:

   107   shows "rder c (rerase r ) = rerase (bder c r)"

   108   apply (induct r)

   109   apply (auto)

   110   using rerase_fuse apply presburger

   111   using rnullable apply blast

   112   using rnullable by blast

   113 

   114 lemma rerase_map_bsimp:

   115   assumes "\<And> r. r \<in> set rs \<Longrightarrow> rerase (bsimp r) = (rsimp \<circ> rerase) r"

   116   shows "map rerase (map bsimp rs) =  map (rsimp \<circ> rerase) rs"

   117   using assms

   118   apply(induct rs)

   119   by simp_all

   120 

   121 

   122 lemma rerase_flts:

   123   shows "map rerase (flts rs) = rflts (map rerase rs)"

   124   apply(induct rs rule: flts.induct)

   125   apply(auto simp add: rerase_fuse)

   126   done

   127 

   128 lemma rerase_dB:

   129   shows "map rerase (distinctBy rs rerase acc) = rdistinct (map rerase rs) acc"

   130   apply(induct rs arbitrary: acc)

   131   apply simp+

   132   done

   133   

   134 lemma rerase_earlier_later_same:

   135   assumes " \<And>r. r \<in> set rs \<Longrightarrow> rerase (bsimp r) = rsimp (rerase r)"

   136   shows " (map rerase (distinctBy (flts (map bsimp rs)) rerase {})) =

   137           (rdistinct (rflts (map (rsimp \<circ> rerase) rs)) {})"

   138   apply(subst rerase_dB)

   139   apply(subst rerase_flts)

   140   apply(subst rerase_map_bsimp)

   141   apply auto

   142   using assms

   143   apply simp

   144   done

   145 

   146 lemma bsimp_rerase:

   147   shows "rerase (bsimp a) = rsimp (rerase a)"

   148   apply(induct a rule: bsimp.induct)

   149   apply(auto)

   150   using rerase_bsimp_ASEQ apply presburger

   151   using distinctBy_distinctWith2 rerase_bsimp_AALTs rerase_earlier_later_same by fastforce

   152 

   153 lemma rders_simp_size:

   154   shows "rders_simp (rerase r) s  = rerase (bders_simp r s)"

   155   apply(induct s rule: rev_induct)

   156   apply simp

   157   by (simp add: bders_simp_append rder_bder_rerase rders_simp_append bsimp_rerase)

   158 

   159 

   160 corollary aders_simp_finiteness:

   161   assumes "\<exists>N. \<forall>s. rsize (rders_simp (rerase r) s) \<le> N"

   162   shows " \<exists>N. \<forall>s. asize (bders_simp r s) \<le> N"

   163 proof - 

   164   from assms obtain N where "\<forall>s. rsize (rders_simp (rerase r) s) \<le> N"

   165     by blast

   166   then have "\<forall>s. rsize (rerase (bders_simp r s)) \<le> N"

   167     by (simp add: rders_simp_size) 

   168   then have "\<forall>s. asize (bders_simp r s) \<le> N"

   169     by (simp add: asize_rsize) 

   170   then show "\<exists>N. \<forall>s. asize (bders_simp r s) \<le> N" by blast

   171 qed

   172   

   173 theorem annotated_size_bound:

   174   shows "\<exists>N. \<forall>s. asize (bders_simp r s) \<le> N"

   175   apply(insert aders_simp_finiteness)

   176   by (simp add: rders_simp_bounded)

   177 

   178 definition bitcode_agnostic :: "(arexp \<Rightarrow> arexp ) \<Rightarrow> bool"

   179   where " bitcode_agnostic f = (\<forall>a1 a2. rerase a1 = rerase a2 \<longrightarrow> rerase (f a1) = rerase (f a2))  "

   180 

   181 lemma bitcode_agnostic_bsimp:

   182   shows  "bitcode_agnostic bsimp"

   183   by (simp add: bitcode_agnostic_def bsimp_rerase)

   184 

   185 thm bsimp_rerase

   186 

   187 lemma cant1:

   188   shows "\<lbrakk> bsimp a = b; rerase a = rerase b; a = ASEQ bs r1 r2 \<rbrakk> \<Longrightarrow>

   189         \<exists>bs' r1' r2'. b = ASEQ bs' r1' r2' \<and> rerase r1' = rerase r1 \<and> rerase r2' = rerase r2"

   190   sorry

   191 

   192 

   193 

   194 (*"part is less than whole" thm for rrexp, since rrexp is always finite*)

   195 lemma rrexp_finite1:

   196   shows "\<lbrakk> bsimp_ASEQ bs1 (bsimp ra1) (bsimp ra2) = ASEQ bs2 rb1 rb2; ra1 ~1 rb1; ra2 ~1 rb2 \<rbrakk> \<Longrightarrow> rerase ra1 = rerase (bsimp ra1) "

   197   apply(case_tac ra1 )

   198         apply simp+

   199      apply(case_tac rb1)

   200            apply simp+

   201 

   202   sorry

   203 

   204 lemma unsure_unchanging:

   205   assumes "bsimp a = bsimp b"

   206 and "a ~1 b"

   207 shows "a = b"

   208   using assms

   209   apply(induct rule: eq1.induct)

   210                       apply simp+

   211   oops

   212 

   213 lemma eq1rerase:

   214   shows "rerase r1 = rerase r2 \<longleftrightarrow> r1 ~1 r2"

   215   using eq1_rerase by presburger

   216 

   217 thm contrapos_pp

   218 

   219 lemma r_part_neq_whole:

   220   shows "RSEQ r1 r2 \<noteq> r2"

   221   apply simp

   222   done

   223 

   224 lemma r_part_neq_whole2:

   225   shows "RSEQ r1 r2 \<noteq> rsimp r2"

   226   by (metis good.simps(7) good.simps(8) good1 good_SEQ r_part_neq_whole rrexp.distinct(5) rsimp.simps(3) test)

   227 

   228 

   229 

   230 lemma arexpfiniteaux1:

   231   shows "rerase (bsimp_ASEQ x41 (bsimp x42) (bsimp x43)) = RSEQ (rerase x42) (rerase x43) \<Longrightarrow> \<forall>bs. bsimp x42 \<noteq> AONE bs"

   232   apply(erule contrapos_pp)

   233   apply simp

   234   apply(erule exE)

   235   apply simp

   236   by (metis bsimp_rerase r_part_neq_whole2 rerase_fuse)

   237 

   238 lemma arexpfiniteaux2:

   239   shows "rerase (bsimp_ASEQ x41 (bsimp x42) (bsimp x43)) = RSEQ (rerase x42) (rerase x43) \<Longrightarrow> bsimp x42 \<noteq> AZERO "

   240   apply(erule contrapos_pp)

   241   apply simp

   242   done

   243 

   244 lemma arexpfiniteaux3:

   245   shows "rerase (bsimp_ASEQ x41 (bsimp x42) (bsimp x43)) = RSEQ (rerase x42) (rerase x43) \<Longrightarrow> bsimp x43 \<noteq> AZERO "

   246   apply(erule contrapos_pp)

   247   apply simp

   248   done

   249 

   250 

   251 lemma arexp_finite1:

   252   shows "rerase (bsimp b) = rerase b \<Longrightarrow> bsimp b = b"

   253   apply(induct b)

   254         apply simp+

   255          apply(case_tac "bsimp b2 = AZERO")

   256           apply simp

   257      apply (case_tac "bsimp b1 = AZERO")

   258       apply simp

   259   apply(case_tac "\<exists>bs. bsimp b1 = AONE bs")

   260   using arexpfiniteaux1 apply blast

   261      apply simp

   262      apply(subgoal_tac "bsimp_ASEQ x1 (bsimp b1) (bsimp b2) = ASEQ x1 (bsimp b1) (bsimp b2)")

   263   apply simp

   264   using bsimp_ASEQ1 apply presburger

   265   apply simp

   266 

   267   sorry

   268 

   269 lemma bitcodes_unchanging2:

   270   assumes "bsimp a = b"

   271 and "a ~1 b"

   272 shows "a = b"

   273   using assms

   274   apply(induct rule: eq1.induct)

   275                       apply simp

   276                       apply simp

   277                       apply simp

   278 

   279                       apply auto

   280   

   281   sorry

   282 

   283 

   284 

   285 lemma bitcodes_unchanging:

   286   shows "\<lbrakk>bsimp a = b; rerase a = rerase b \<rbrakk> \<Longrightarrow> a = b"

   287   apply(induction a arbitrary: b)

   288         apply simp+

   289      apply(case_tac "\<exists>bs. bsimp a1 = AONE bs")

   290       apply(erule exE)

   291       apply simp

   292       prefer 2

   293       apply(case_tac "bsimp a1 = AZERO")

   294        apply simp

   295       apply simp

   296       apply (metis BlexerSimp.bsimp_ASEQ0 bsimp_ASEQ1 rerase.simps(1) rerase.simps(5) rrexp.distinct(5) rrexp.inject(2))

   297   

   298   sorry

   299 

   300 

   301 lemma bagnostic_shows_bsimp_idem:

   302   assumes "bitcode_agnostic bsimp"

   303 and "rerase (bsimp a) = rsimp (rerase a)"

   304 and "rsimp r = rsimp (rsimp r)"

   305 shows "bsimp a = bsimp (bsimp a)"

   306   

   307   oops

   308 

   309 theorem bsimp_idem:

   310   shows "bsimp (bsimp a) = bsimp a"

   311   using bitcodes_unchanging bsimp_rerase rsimp_idem by auto

   312 

   313 unused_thms

   314 

   315 end