
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


  thm asize.simps
fun s_complexity:: "arexp \<Rightarrow> nat" where
    "s_complexity AZERO = 1"
  | "s_complexity (AONE _) = 1"
  | "s_complexity (ASTAR bs r) = Suc (s_complexity r)"
  | "s_complexity (AALTs bs rs) = Suc (Suc (sum_list (map s_complexity rs)))"
  | "s_complexity (ASEQ bs r1 r2) = Suc (s_complexity r1 + s_complexity r2)"
  | "s_complexity (ACHAR _ _) = 1"
  | "s_complexity (ANTIMES _ r _) = Suc (s_complexity r)"



















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"
| "AALTs bs (rs1 @ distinctWith rs2 eq1 (set rs1)) \<le>1 AALTs bs (rs1 @ rs2)"
| "bsimp_AALTs bs rs \<le>1 AALTs bs rs"






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_leq1:
  shows "AALTs bs (distinctWith rs eq1 {}) \<le>1 AALTs bs rs"
  by (metis append_Nil empty_set leq1.intros(18))

lemma leq1_list:
  shows "
       \<lbrakk>\<And>x2aa. x2aa \<in> set x2a \<Longrightarrow> bsimp x2aa \<le>1 x2aa;
        bsimp_AALTs x1 (distinctWith (flts (map bsimp x2a)) eq1 {}) \<le>1 AALTs x1 (distinctWith (flts (map bsimp x2a)) eq1 {});
        AALTs x1 (distinctWith (flts (map bsimp x2a)) eq1 {}) \<le>1 AALTs x1 (flts (map bsimp x2a));
        AALTs x1 (flts (map bsimp x2a)) \<le>1 AALTs x1 (map bsimp x2a)\<rbrakk>
       \<Longrightarrow> AALTs x1 (map bsimp x2a) \<le>1 AALTs x1 x2a"
  apply(induct x2a)
   apply simp
  by (simp add: dB_leq1 flts_leq1 leq1.intros(16) leq1.intros(19))



lemma bsimp_leq1:
  shows "bsimp r \<le>1 r"
  apply(induct r)
        apply simp
  
  apply (simp add: leq1.intros(1))
  
  using leq1.intros(1) apply force
  
  apply (simp add: leq1.intros(1))

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

  apply (simp add: leq1.intros(1))
   prefer 2
  
  apply (simp add: leq1.intros(1))
  apply simp
  apply(subgoal_tac " bsimp_AALTs x1 (distinctWith (flts (map bsimp x2a)) eq1 {}) \<le>1  AALTs x1 (distinctWith (flts (map bsimp x2a)) eq1 {})")
  apply(subgoal_tac " AALTs x1 (distinctWith (flts (map bsimp x2a)) eq1 {}) \<le>1  AALTs x1 ( (flts (map bsimp x2a)) )")
    apply(subgoal_tac " AALTs x1 ( (flts (map bsimp x2a)) ) \<le>1  AALTs x1 ( ( (map bsimp x2a)) )")

    apply(subgoal_tac " AALTs x1 ( map bsimp x2a ) \<le>1  AALTs x1   x2a ")
  
  apply (meson leq1.intros(17))
  
  using leq1_list apply blast

  using flts_leq1 apply presburger
  
  using dB_leq1 apply blast
  
  using leq1.intros(19) by blast




lemma stupid_leq1_1:
  shows " rerase  r2 \<noteq> RSEQ r (RSEQ RONE (rerase r2))"
  apply(induct r2)
        apply simp+
  done


lemma rerase_arexp_additional1:
  shows " asize (AALTs bs (rs1 @ rs2)) = rsize (RALTS (map rerase rs1 @ map rerase rs2))"
  apply simp
  by (metis (mono_tags, lifting) asize_rsize comp_apply map_eq_conv)

  


lemma rerase2:
  shows "rsizes (map rerase (distinctWith rs2 eq1 (set rs1))) \<le> rsizes (map rerase rs2)"
  apply(induct rs2 arbitrary: rs1)
   apply simp+
  by (metis List.set_insert trans_le_add2)

lemma rerase3:
  shows "rsize (RALTS (map rerase rs1 @ map rerase (distinctWith rs2 eq1 (set rs1)))) \<le> rsize (RALTS (map rerase rs1 @ map rerase rs2))"
  using rerase2 by force


lemma bsimpalts_size:
  shows "asize (bsimp_AALTs bs rs) \<le> asize (AALTs bs rs)"
  apply(case_tac rs)
   apply simp
  apply(case_tac list)
   apply auto
  by (metis asize_rsize dual_order.refl le_SucI rerase_fuse)
  


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))
     apply simp
  
  using dual_order.trans apply blast
  
  using rerase3 rerase_arexp_additional1 apply force
  using bsimpalts_size by blast
  



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)
  apply simp
  
  apply (metis asize_rsize leq1_size lessI nle_le not_add_less2 plus_1_eq_Suc rsize.simps(5) trans_le_add2)
   apply simp
  by (metis Suc_n_not_le_n bsimpalts_size rsize.simps(5) size_deciding_equality5 trans_le_add2)

lemma leq1_neq:
  shows "\<lbrakk>r1 \<le>1 r2 ; r1 \<noteq> r2\<rbrakk> \<Longrightarrow> asize r1 < asize r2"
  apply(induct rule : leq1.induct)
                    apply simp+
                 apply (metis asize_rsize lessI less_SucI rerase_fuse)
  apply simp+
  
               apply (metis (mono_tags, lifting) comp_apply less_SucI map_eq_conv not_less_less_Suc_eq rerase_fuse size_deciding_equality3)
  apply simp
  
  apply (simp add: asize0)
  
  using less_Suc_eq apply auto[1]
            apply simp
           apply simp
          apply simp
         apply simp

  oops

lemma leq1_leq_case1:
  shows " \<lbrakk>r1 \<le>1 r2; r1 = r2 \<or> rerase r1 \<noteq> rerase r2; r2 \<le>1 r3; r2 = r3 \<or> rerase r2 \<noteq> rerase r3\<rbrakk> \<Longrightarrow> r1 = r3 \<or> rerase r1 \<noteq> rerase r3"
  apply(induct rule: leq1.induct)
                    apply simp+
  
  apply (metis rerase.elims rrexp.distinct(1) rrexp.distinct(11) rrexp.distinct(3) rrexp.distinct(5) rrexp.distinct(7) rrexp.distinct(9))
                  apply simp

                  apply (metis leq1_trans1 rerase.simps(1) rerase.simps(5))

                 apply (metis leq1_trans1 rerase.simps(5) rerase_fuse)
                apply simp
                apply auto
 
  oops



lemma scomp_rerase3:
  shows "r1 ~1 r2 \<Longrightarrow> s_complexity r1 = s_complexity r2"
  apply(induct rule: eq1.induct)
                      apply simp+
  done

  


lemma scomp_rerase2:
  shows "rerase r1 = rerase r2 \<Longrightarrow> s_complexity r1 = s_complexity r2"  
  using eq1rerase scomp_rerase3 by blast





lemma scomp_rerase:
  shows "s_complexity r1 < s_complexity r2 \<Longrightarrow>rerase  r1 \<noteq> rerase r2"
  by (metis nat_neq_iff scomp_rerase2)

thm bsimp_ASEQ.simps

lemma scomp_bsimpalts:
  shows "s_complexity (bsimp_ASEQ bs1 r1' r2') \<le> s_complexity (ASEQ bs1 r1' r2')"
  apply(case_tac "r1' = AZERO")
   apply simp
  apply(case_tac "r2' = AZERO")
  apply simp
  apply(case_tac "\<exists>bs2. r1' = AONE bs2")
   apply(erule exE)
 
   apply simp
  
  apply (metis le_SucI le_add2 plus_1_eq_Suc rerase_fuse scomp_rerase2)
  apply(subgoal_tac "bsimp_ASEQ bs1 r1' r2' = ASEQ bs1 r1' r2'")
   apply simp
  using bsimp_ASEQ1 by presburger
  

lemma scompsize_aux:
  shows "s_complexity (AALTs bs (rs1 @ distinctWith rs2 eq1 (set rs1))) \<le> s_complexity (AALTs bs (rs1 @ rs2))"
  apply(induct rs2 arbitrary: rs1)
   apply simp
  apply simp
  apply(case_tac "\<exists>x \<in> set rs1. a ~1 x")
  using trans_le_add2 apply blast
  apply simp
  
  by (metis List.set_insert)

  



lemma scomp_size_reduction:
  shows "r1 \<le>1 r2 \<Longrightarrow> s_complexity r1 \<le> s_complexity r2"
  apply(induct rule: leq1.induct)
                    apply simp+
                 apply (metis le_SucI le_add2 plus_1_eq_Suc rerase_fuse scomp_rerase2)
  apply simp+
  
  apply (smt (verit) comp_apply dual_order.eq_iff map_eq_conv plus_1_eq_Suc rerase_fuse scomp_rerase2 trans_le_add2)
              apply simp+
  
       apply (metis le_SucI le_add2 plus_1_eq_Suc rerase_fuse scomp_rerase2)


  
  apply (smt (verit, del_insts) add_mono_thms_linordered_semiring(1) dual_order.trans le_numeral_extra(4) plus_1_eq_Suc s_complexity.simps(5) scomp_bsimpalts)
     apply simp
    apply simp
  
  using scompsize_aux apply auto[1]
  apply(case_tac rs)
   apply simp
  apply(case_tac "list")
   apply auto
  by (metis eq_imp_le le_imp_less_Suc less_imp_le_nat rerase_fuse scomp_rerase2)

lemma prf22:
  shows "\<lbrakk>r1 \<le>1 r2; \<not> r1 ~1 r2\<rbrakk> \<Longrightarrow> s_complexity r1 \<noteq> s_complexity r2"
  apply(induct rule:eq1.induct)
                      apply simp+
                      apply auto

  sorry



lemma compl_rrewrite_down1:
  shows "r1 \<le>1 r2 \<Longrightarrow> r1 ~1 r2 \<or> s_complexity r1 < s_complexity r2"
    apply(subgoal_tac "s_complexity r1 \<le> s_complexity r2")
  apply(case_tac "r1 ~1 r2")
    apply simp
   apply(subgoal_tac "s_complexity r1 \<noteq> s_complexity r2")
    apply simp
  using prf22 apply blast
  by (simp add: scomp_size_reduction)
  
lemma leq1_eq1_equal:
  shows "\<lbrakk>r1 \<le>1 r2; bsimp r2 = r1 \<rbrakk> \<Longrightarrow> r1 = r2 \<or> s_complexity r1 < s_complexity r2"
  sorry






lemma compl_rrewrite_down:
  shows "r1 \<le>1 r2 \<Longrightarrow>r1 = r2 \<or> s_complexity r1 < s_complexity r2"
  apply(subgoal_tac "s_complexity r1 \<le> s_complexity r2")
  
  apply(induct rule: leq1.induct)
                    apply simp
                   apply simp
                  apply simp
  apply (smt (verit) fuse.elims lessI less_Suc_eq plus_1_eq_Suc s_complexity.simps(2) s_complexity.simps(3) s_complexity.simps(4) s_complexity.simps(5) s_complexity.simps(6) s_complexity.simps(7))
                apply simp
  sorry


lemma compl_rrewrite_down1_1:
  shows "\<lbrakk>r1 \<le>1 r2; s_complexity r1 = s_complexity r2 \<rbrakk> \<Longrightarrow> r1 = r2"
  using compl_rrewrite_down nat_less_le by auto



lemma leq1_less_or_equal: shows
"r1 \<le>1 r2 \<Longrightarrow> r1 = r2 \<or> rerase r1 \<noteq> rerase r2"
  using compl_rrewrite_down scomp_rerase by blast











lemma arexp_finite1:
  shows "rerase (bsimp b) = rerase b \<Longrightarrow> bsimp b = b"
  using bsimp_leq1 leq1_less_or_equal by blast
  
lemma bsimp_idem:
  shows "bsimp (bsimp r ) = bsimp r"
  using arexp_finite1 bsimp_rerase rsimp_idem by presburger





end
