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 

    22 lemma eq1_rerase:

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

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

    25   apply(auto)

    26   done

    27 

    28 

    29 lemma distinctBy_distinctWith:

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

    31   apply(induct xs arbitrary: acc)

    32   apply(auto)

    33   by (metis image_insert)

    34 

    35 lemma distinctBy_distinctWith2:

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

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

    38   using eq1_rerase by presburger

    39   

    40 lemma asize_rsize:

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

    42   apply(induct r rule: rerase.induct)

    43   apply(auto)

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

    45   done

    46 

    47 lemma rerase_fuse:

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

    49   apply(induct r)

    50        apply simp+

    51   done

    52 

    53 lemma rerase_bsimp_ASEQ:

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

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

    56   apply(auto)

    57   done

    58 

    59 lemma rerase_bsimp_AALTs:

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

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

    62   apply(auto simp add: rerase_fuse)

    63   done

    64 

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

    66   where

    67   "anonalt (AALTs bs2 rs) = False"

    68 | "anonalt r = True"

    69 

    70 

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

    72   "agood AZERO = False"

    73 | "agood (AONE cs) = True" 

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

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

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

    77 | "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'))"

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

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

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

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

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

    83 

    84 

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

    86   where

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

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

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

    90 | "anonnested r = True"

    91 

    92 

    93 lemma asize0:

    94   shows "0 < asize r"

    95   apply(induct  r)

    96   apply(auto)

    97   done

    98 

    99 lemma rnullable:

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

   101   apply(induct r rule: rerase.induct)

   102   apply(auto)

   103   done

   104 

   105 lemma rder_bder_rerase:

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

   107   apply (induct r)

   108   apply (auto)

   109   using rerase_fuse apply presburger

   110   using rnullable apply blast

   111   using rnullable by blast

   112 

   113 lemma rerase_map_bsimp:

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

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

   116   using assms

   117   apply(induct rs)

   118   by simp_all

   119 

   120 

   121 lemma rerase_flts:

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

   123   apply(induct rs rule: flts.induct)

   124   apply(auto simp add: rerase_fuse)

   125   done

   126 

   127 lemma rerase_dB:

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

   129   apply(induct rs arbitrary: acc)

   130   apply simp+

   131   done

   132   

   133 lemma rerase_earlier_later_same:

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

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

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

   137   apply(subst rerase_dB)

   138   apply(subst rerase_flts)

   139   apply(subst rerase_map_bsimp)

   140   apply auto

   141   using assms

   142   apply simp

   143   done

   144 

   145 lemma bsimp_rerase:

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

   147   apply(induct a rule: bsimp.induct)

   148   apply(auto)

   149   using rerase_bsimp_ASEQ apply presburger

   150   using distinctBy_distinctWith2 rerase_bsimp_AALTs rerase_earlier_later_same by fastforce

   151 

   152 lemma rders_simp_size:

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

   154   apply(induct s rule: rev_induct)

   155   apply simp

   156   by (simp add: bders_simp_append rder_bder_rerase rders_simp_append bsimp_rerase)

   157 

   158 

   159 corollary aders_simp_finiteness:

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

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

   162 proof - 

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

   164     by blast

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

   166     by (simp add: rders_simp_size) 

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

   168     by (simp add: asize_rsize) 

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

   170 qed

   171   

   172 theorem annotated_size_bound:

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

   174   apply(insert aders_simp_finiteness)

   175   by (simp add: rders_simp_bounded)

   176 

   177 

   178 unused_thms

   179 

   180 end