theory FBound

  imports "BlexerSimp" "ClosedFormsBounds"

begin

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

  where

  "distinctBy [] f acc = []"

| "distinctBy (x#xs) f acc = 

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

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

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

where

  "rerase AZERO = RZERO"

| "rerase (AONE _) = RONE"

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

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

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

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

lemma eq1_rerase:

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

  apply(induct x y rule: eq1.induct)

  apply(auto)

  done

lemma distinctBy_distinctWith:

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

  apply(induct xs arbitrary: acc)

  apply(auto)

  by (metis image_insert)

lemma distinctBy_distinctWith2:

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

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

  using eq1_rerase by presburger

lemma asize_rsize:

  shows "rsize (rerase r) = asize r"

  apply(induct r rule: rerase.induct)

  apply(auto)

  apply (metis (mono_tags, lifting) comp_apply map_eq_conv)

  done

lemma rerase_fuse:

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

  apply(induct r)

       apply simp+

  done

lemma rerase_bsimp_ASEQ:

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

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

  apply(auto)

  done

lemma rerase_bsimp_AALTs:

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

  apply(induct bs rs rule: bsimp_AALTs.induct)

  apply(auto simp add: rerase_fuse)

  done

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

  where

  "anonalt (AALTs bs2 rs) = False"

| "anonalt r = True"

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

  "agood AZERO = False"

| "agood (AONE cs) = True" 

| "agood (ACHAR cs c) = True"

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

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

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

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

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

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

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

| "agood (ASTAR cs r) = True"

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

  where

  "anonnested (AALTs bs2 []) = True"

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

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

| "anonnested r = True"

lemma asize0:

  shows "0 < asize r"

  apply(induct  r)

  apply(auto)

  done

lemma rnullable:

  shows "rnullable (rerase r) = bnullable r"

  apply(induct r rule: rerase.induct)

  apply(auto)

  done

lemma rder_bder_rerase:

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

  apply (induct r)

  apply (auto)

  using rerase_fuse apply presburger

  using rnullable apply blast

  using rnullable by blast

lemma rerase_map_bsimp:

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

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

  using assms

  apply(induct rs)

  by simp_all

lemma rerase_flts:

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

  apply(induct rs rule: flts.induct)

  apply(auto simp add: rerase_fuse)

  done

lemma rerase_dB:

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

  apply(induct rs arbitrary: acc)

  apply simp+

  done

lemma rerase_earlier_later_same:

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

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

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

  apply(subst rerase_dB)

  apply(subst rerase_flts)

  apply(subst rerase_map_bsimp)

  apply auto

  using assms

  apply simp

  done

lemma bsimp_rerase:

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

  apply(induct a rule: bsimp.induct)

  apply(auto)

  using rerase_bsimp_ASEQ apply presburger

  using distinctBy_distinctWith2 rerase_bsimp_AALTs rerase_earlier_later_same by fastforce

lemma rders_simp_size:

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

  apply(induct s rule: rev_induct)

  apply simp

  by (simp add: bders_simp_append rder_bder_rerase rders_simp_append bsimp_rerase)

corollary aders_simp_finiteness:

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

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

proof - 

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

    by blast

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

    by (simp add: rders_simp_size) 

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

    by (simp add: asize_rsize) 

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

qed

theorem annotated_size_bound:

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

  apply(insert aders_simp_finiteness)

  by (simp add: rders_simp_bounded)

unused_thms

end