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

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

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)

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

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

lemma bitcode_agnostic_bsimp:

  shows  "bitcode_agnostic bsimp"

  by (simp add: bitcode_agnostic_def bsimp_rerase)

thm bsimp_rerase

lemma unsure_unchanging:

  assumes "bsimp a = bsimp b"

and "a ~1 b"

shows "a = b"

  using assms

  apply(induct rule: eq1.induct)

                      apply simp+

  oops

lemma eq1rerase:

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

  using eq1_rerase by presburger

thm contrapos_pp

lemma r_part_neq_whole:

  shows "RSEQ r1 r2 \<noteq> r2"

  apply simp

  done

lemma r_part_neq_whole2:

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

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

lemma arexpfiniteaux1:

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

  apply(erule contrapos_pp)

  apply simp

  apply(erule exE)

  apply simp

  by (metis bsimp_rerase r_part_neq_whole2 rerase_fuse)

lemma arexpfiniteaux2:

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

  apply(erule contrapos_pp)

  apply simp

  done

lemma arexpfiniteaux3:

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

  apply(erule contrapos_pp)

  apply simp

  done

lemma aux_aux_aux:

  shows "map rerase (flts (map bsimp rs)) = map rerase rs \<Longrightarrow> map rerase (map bsimp rs) = map rerase rs"

  oops

inductive leq1 ("_ \<le>1 _" [80, 80] 80) where  

  "r1 \<le>1 r1"

| "AZERO \<le>1 ASEQ bs AZERO r" 

| "AZERO \<le>1 ASEQ bs r AZERO"

| "fuse (bs @ bs1) r2 \<le>1 ASEQ bs (AONE bs1) r2"

| "AALTs bs (rs1 @ rs) \<le>1 AALTs bs (rs1 @( AZERO # rs))"

| "AALTs bs (rsa @ (map (fuse bs1) rs1) @ rsb) \<le>1 AALTs bs (rsa @ (AALTs bs1 rs1) # rsb)"

| "rerase a1 = rerase a2 \<Longrightarrow> AALTs bs (rsa @ [a1] @ rsb @ rsc) \<le>1 AALTs bs (rsa @ [a1] @ rsb @ [a2] @ rsc) "

| "r1 \<le>1 r2 \<Longrightarrow> r1  \<le>1 ASEQ bs (AONE bs1) r2"

| "r2 \<le>1 r1 \<Longrightarrow> AALTs bs (rs1 @ r2 # rs) \<le>1 AALTs bs (rs1 @ r1 # rs)"

| "r2 \<le>1 r1 \<Longrightarrow> ASEQ bs r  r2 \<le>1 ASEQ bs r r1"

| "r2 \<le>1 r1 \<Longrightarrow> ASEQ bs r2 r  \<le>1 ASEQ bs r1 r"

| "r \<le>1 r' \<Longrightarrow> ASTAR bs r \<le>1 ASTAR bs r'"

| "AZERO \<le>1 AALTs bs []"

| "fuse bs r \<le>1 AALTs bs [r]"

| "\<lbrakk>r1' \<le>1 r1;  r2' \<le>1 r2\<rbrakk> \<Longrightarrow> bsimp_ASEQ bs1 r1' r2' \<le>1 ASEQ bs1 r1 r2"

| "\<lbrakk>AALTs bs rs1 \<le>1 AALTs bs rs2; r1 \<le>1 r2 \<rbrakk> \<Longrightarrow> AALTs bs (r1 # rs1) \<le>1 AALTs bs (r2 # rs2)"

| "\<lbrakk>r1 \<le>1 r2; r2 \<le>1 r3 \<rbrakk> \<Longrightarrow> r1 \<le>1 r3"

lemma leq1_6_variant1:

  shows "AALTs bs ( (map (fuse bs1) rs1) @ rsb) \<le>1 AALTs bs ((AALTs bs1 rs1) # rsb)"

  by (metis leq1.intros(6) self_append_conv2)

lemma flts_leq1:

  shows "AALTs bs (flts rs) \<le>1 AALTs bs rs"

  apply(induct rule: flts.induct)

         apply (simp add: leq1.intros(1))

        apply simp

  apply (metis append_Nil leq1.intros(17) leq1.intros(5))

       apply simp

       apply(subgoal_tac "AALTs bs (map (fuse bsa) rs1 @ flts rs) \<le>1 AALTs bs (AALTs bsa rs1 # flts rs)")

        apply (meson leq1.intros(1) leq1.intros(16) leq1.intros(17))

  using leq1_6_variant1 apply presburger

  apply (simp add: leq1.intros(1) leq1.intros(16))

  using leq1.intros(1) leq1.intros(16) apply auto[1]

  using leq1.intros(1) leq1.intros(16) apply force

   apply (simp add: leq1.intros(1) leq1.intros(16))

  using leq1.intros(1) leq1.intros(16) by force

lemma dB_leq12:

  sorry

lemma dB_leq1:

  shows "AALTs bs (distinctWith rs eq1 {}) \<le>1 AALTs bs rs"

lemma stupid_leq1_1:

  shows " rerase  r2 \<noteq> RSEQ r (RSEQ RONE (rerase r2))"

  apply(induct r2)

        apply simp+

  done

lemma leq1_size:

  shows "r1 \<le>1 r2 \<Longrightarrow> asize r1 \<le> asize r2"

  apply (induct rule: leq1.induct)

               apply simp+

  apply (metis asize_rsize le_SucI le_add2 plus_1_eq_Suc rerase_fuse)

           apply simp

          apply simp

          apply (metis (mono_tags, lifting) asize_rsize comp_apply dual_order.eq_iff le_SucI map_eq_conv rerase_fuse)

  apply simp+

  apply (metis Suc_n_not_le_n asize_rsize linorder_le_cases rerase_fuse)

  apply(case_tac "r1' = AZERO")

   apply simp

  apply(case_tac "\<exists>bs1. r1' = AONE bs1")

   apply(erule exE)

   apply simp

  apply (metis asize_rsize le_SucI rerase_fuse trans_le_add2)

  apply (smt (verit, best) Suc_eq_plus1 ab_semigroup_add_class.add_ac(1) add.commute add.right_neutral add_cancel_right_right add_mono_thms_linordered_semiring(1) asize.simps(5) asize_rsize nat_add_left_cancel_le order.trans order_trans plus_1_eq_Suc rSEQ_mono rerase_bsimp_ASEQ rsize.simps(5))

  sorry

lemma size_deciding_equality:

  shows "asize r1 \<noteq> asize r2 \<Longrightarrow> r1 \<noteq> r2 "

  apply auto

  done

lemma size_deciding_equality2:

  shows "rerase r1 = rerase r2 \<Longrightarrow> asize r1 = asize r2"

  by (metis asize_rsize)

lemma size_deciding_equality3:

  shows "asize r1 \<noteq> asize r2 \<Longrightarrow> rerase r1 \<noteq> rerase r2"

  by (metis asize_rsize)

lemma size_deciding_equality4:

  shows "rerase a1 = r2 \<Longrightarrow> asize a1 = rsize r2"

  by (metis asize_rsize)

lemma size_deciding_equality5:

  shows "asize a1 \<noteq> rsize r2 \<Longrightarrow>rerase a1 \<noteq> r2"

  by (metis asize_rsize)

lemma leq1_trans1:

  shows " r1 \<le>1 r2 \<Longrightarrow>  rerase r1 \<noteq> RSEQ r (rerase r2)"

  apply(induct rule: leq1.induct)

               apply simp+

  using rerase_fuse stupid_leq1_1 apply presburger

           apply simp+

        apply(subgoal_tac "asize r1 \<noteq> rsize (RSEQ r (RSEQ RONE (rerase r2)))")

  using size_deciding_equality5 apply blast

  using asize_rsize leq1_size apply fastforce

       apply simp+

  apply(subgoal_tac "rsize (rerase (fuse bs ra)) \<noteq> rsize (RSEQ r (RALTS [rerase ra]))")

  apply force

  apply simp

  apply(simp add: asize_rsize)

  apply (simp add: rerase_fuse size_deciding_equality4)

  apply (metis Suc_n_not_le_n asize_rsize leq1.intros(15) leq1_size rsize.simps(5) trans_le_add2)

  sorry

lemma leq1_less_or_equal: shows

"r1 \<le>1 r2 \<Longrightarrow> r1 = r2 \<or> rerase r1 \<noteq> rerase r2"

  apply(induct rule: leq1.induct)

               apply simp

              apply simp

  apply simp

            apply (simp add: rerase_fuse)

           apply simp

  apply simp

  using r_finite1 rerase_fuse apply force

         apply simp

        apply simp

        apply(case_tac "r1 = r2")

         apply simp

        apply simp

  using leq1_trans1 apply presburger

       apply simp

      apply simp

     apply simp

    apply simp

   apply simp

   apply simp

  using r_finite1 rerase_fuse apply auto[1]

  apply (smt (verit, best) BlexerSimp.bsimp_ASEQ0 BlexerSimp.bsimp_ASEQ2 bsimp_ASEQ.simps(1) bsimp_ASEQ1 leq1_trans1 rerase.simps(5) rerase_bsimp_ASEQ rerase_fuse rrexp.inject(2) rsimp_SEQ.simps(22))

  sorry

lemma arexpfiniteaux4:

  shows"

       \<lbrakk>\<And>x. \<lbrakk>x \<in> set rs; rerase (bsimp x) = rerase x\<rbrakk> \<Longrightarrow> bsimp x = x;

        rerase (bsimp_AALTs bs1 (distinctWith (flts (map bsimp rs)) eq1 {})) = RALTS (map rerase rs)\<rbrakk>

       \<Longrightarrow> bsimp_AALTs bs1 (distinctWith (flts (map bsimp rs)) eq1 {}) = AALTs bs1 rs"

  apply(induct rs)

  apply simp

  sorry

lemma arexp_finite1:

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

  apply(induct rule: bsimp.induct)

        apply simp

        apply (smt (verit) arexpfiniteaux1 arexpfiniteaux2 arexpfiniteaux3 bsimp_ASEQ1 rerase.simps(5) rrexp.inject(2))

  apply simp

  using arexpfiniteaux4 apply blast

      apply simp+

  done

(*

  apply(induct b)

        apply simp+

         apply(case_tac "bsimp b2 = AZERO")

          apply simp

     apply (case_tac "bsimp b1 = AZERO")

      apply simp

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

  using arexpfiniteaux1 apply blast

     apply simp

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

  apply simp

  using bsimp_ASEQ1 apply presburger

  apply simp

  sorry

*)

lemma bitcodes_unchanging2:

  assumes "bsimp a = b"

and "a ~1 b"

shows "a = b"

  using assms

  apply(induct rule: eq1.induct)

                      apply simp

                      apply simp

                      apply simp

                      apply auto

  sorry

lemma bsimp_reduces:

  shows "bsimp r \<le>1 r"

  apply(induct rule: bsimp.induct)

        apply simp

        apply (simp add: leq1.intros(15))

       apply simp

  apply(case_tac rs)

        apply simp

  apply (simp add: leq1.intros(13))

       apply(case_tac list)

        apply simp

  sorry

lemma bitcodes_unchanging:

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

  apply(induction a arbitrary: b)

        apply simp+

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

      apply(erule exE)

      apply simp

      prefer 2

      apply(case_tac "bsimp a1 = AZERO")

       apply simp

      apply simp

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

  sorry

lemma bagnostic_shows_bsimp_idem:

  assumes "bitcode_agnostic bsimp"

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

and "rsimp r = rsimp (rsimp r)"

shows "bsimp a = bsimp (bsimp a)"

  oops

theorem bsimp_idem:

  shows "bsimp (bsimp a) = bsimp a"

  using bitcodes_unchanging bsimp_rerase rsimp_idem by auto

unused_thms

end