344 lemma no_alt_short_list_after_simp:

   344 

   345   shows "RALTS rs = rsimp r \<Longrightarrow> rsimp_ALTs rs = RALTS rs"

   345 

   346   sorry

   347 

   348 lemma no_further_dB_after_simp:

   349   shows "RALTS rs = rsimp r \<Longrightarrow> rdistinct rs {} = rs"

   350   sorry

   406 lemma rsimp_idem:

   401 

   407   shows "rsimp (rsimp r) = rsimp r"

   402 

   408   sorry

   403 fun nonalt :: "rrexp \<Rightarrow> bool"

   409 

   404   where

   410 corollary rsimp_inner_idem1:

   405   "nonalt (RALTS  rs) = False"

   411   shows "rsimp r = RSEQ r1 r2 \<Longrightarrow> rsimp r1 = r1 \<and> rsimp r2 = r2"

   406 | "nonalt r = True"

   412   

   407 

   413   sorry

   408 

   414 

   409 fun good :: "rrexp \<Rightarrow> bool" where

   415 corollary rsimp_inner_idem2:

   410   "good RZERO = False"

   416   shows "rsimp r = RALTS rs \<Longrightarrow> \<forall>r' \<in> (set rs). rsimp r' = r'"

   411 | "good (RONE) = True" 

   417   sorry

   412 | "good (RCHAR c) = True"

   418 

   413 | "good (RALTS []) = False"

   419 corollary rsimp_inner_idem3:

   414 | "good (RALTS [r]) = False"

   420   shows "rsimp r = RALTS rs \<Longrightarrow> map rsimp rs = rs"

   415 | "good (RALTS (r1 # r2 # rs)) = ((distinct ( (r1 # r2 # rs))) \<and>(\<forall>r' \<in> set (r1 # r2 # rs). good r' \<and> nonalt r'))"

   421   by (meson map_idI rsimp_inner_idem2)

   416 | "good (RSEQ RZERO _) = False"

   422 

   417 | "good (RSEQ RONE _) = False"

   423 corollary rsimp_inner_idem4:

   418 | "good (RSEQ  _ RZERO) = False"

   424   shows "rsimp r = RALTS rs \<Longrightarrow> rflts rs = rs"

   419 | "good (RSEQ r1 r2) = (good r1 \<and> good r2)"

   425   sorry

   420 | "good (RSTAR r) = True"

   426 

   421 

   427 

   422 

   428 lemma head_one_more_simp:

   423 lemma  k0a:

   429   shows "map rsimp (r # rs) = map rsimp (( rsimp r) # rs)"

   424   shows "rflts [RALTS rs] =   rs"

   430   by (simp add: rsimp_idem)

   425   apply(simp)

   431 

   426   done

   432 lemma head_one_more_dersimp:

   427 

   433   shows "map rsimp ((rder x (rders_simp r s) # rs)) = map rsimp ((rders_simp r (s@[x]) ) # rs)"

   428 lemma bbbbs:

   434   using head_one_more_simp rders_simp_append rders_simp_one_char by presburger

   429   assumes "good r" "r = RALTS rs"

   430   shows "rsimp_ALTs  (rflts [r]) = RALTS rs"

   431   using  assms

   432   by (metis good.simps(4) good.simps(5) k0a rsimp_ALTs.elims)

   433 

   434 lemma bbbbs1:

   435   shows "nonalt r \<or> (\<exists> rs. r  = RALTS  rs)"

   436   by (meson nonalt.elims(3))

   437 

   438 

   439 

   440 lemma good0:

   441   assumes "rs \<noteq> Nil" "\<forall>r \<in> set rs. nonalt r" "distinct rs"

   442   shows "good (rsimp_ALTs rs) \<longleftrightarrow> (\<forall>r \<in> set rs. good r)"

   443   using  assms

   444   apply(induct  rs rule: rsimp_ALTs.induct)

   445   apply(auto)

   446   done

   447 

   448 lemma good0a:

   449   assumes "rflts (map rsimp rs) \<noteq> Nil" "\<forall>r \<in> set (rflts (map rsimp rs)). nonalt r"

   450   shows "good (rsimp (RALTS rs)) \<longleftrightarrow> (\<forall>r \<in> set (rflts (map rsimp rs)). good r)"

   451   using  assms

   452   apply(simp)

   453   apply(auto)

   454    apply(subst (asm) good0)

   455   

   456   apply (metis rdistinct_set_equality set_empty)

   457    apply(simp)

   458     apply(auto)

   459      apply (metis rdistinct_set_equality)

   460   using rdistinct_does_the_job apply blast

   461   apply (metis rdistinct_set_equality)

   462   by (metis good0 rdistinct_does_the_job rdistinct_set_equality set_empty)

   463 

   464 

   465 lemma flts0:

   466   assumes "r \<noteq> RZERO" "nonalt r"

   467   shows "rflts [r] \<noteq> []"

   468   using  assms

   469   apply(induct r)

   470        apply(simp_all)

   471   done

   472 

   473 lemma flts1:

   474   assumes "good r" 

   475   shows "rflts [r] \<noteq> []"

   476   using  assms

   477   apply(induct r)

   478        apply(simp_all)

   479   using good.simps(4) by blast

   480 

   481 lemma flts2:

   482   assumes "good r" 

   483   shows "\<forall>r' \<in> set (rflts [r]). good r' \<and> nonalt r'"

   484   using  assms

   485   apply(induct r)

   486        apply(simp)

   487       apply(simp)

   488      apply(simp)

   489     prefer 2

   490     apply(simp)

   491     apply(auto)[1]

   492   

   493      apply (metis flts1 good.simps(5) good.simps(6) k0a neq_Nil_conv)

   494     apply (metis flts1 good.simps(5) good.simps(6) k0a neq_Nil_conv)

   495    apply fastforce

   496   apply(simp)

   497   done  

   498 

   499 

   500 

   501 lemma flts3:

   502   assumes "\<forall>r \<in> set rs. good r \<or> r = RZERO" 

   503   shows "\<forall>r \<in> set (rflts rs). good r"

   504   using  assms

   505   apply(induct rs arbitrary: rule: rflts.induct)

   506         apply(simp_all)

   507   by (metis UnE flts2 k0a)

   508 

   509 lemma flts3b:

   510   assumes "\<exists>r\<in>set rs. good r"

   511   shows "rflts rs \<noteq> []"

   512   using  assms

   513   apply(induct rs arbitrary: rule: rflts.induct)

   514         apply(simp)

   515        apply(simp)

   516       apply(simp)

   517       apply(auto)

   518   done

   519 

   520 lemma flts4:

   521   assumes "rsimp_ALTs (rflts rs) = RZERO"

   522   shows "\<forall>r \<in> set rs. \<not> good r"

   523   using assms

   524   apply(induct rs  rule: rflts.induct)

   525         apply(auto)

   526         defer

   527   apply (metis (no_types, lifting) Nil_is_append_conv append_self_conv2 rsimp_ALTs.elims butlast.simps(2) butlast_append flts3b nonalt.simps(1) nonalt.simps(2))

   528   using rsimp_ALTs.elims apply auto[1]

   529   using rsimp_ALTs.elims apply auto[1]

   530   using rsimp_ALTs.elims apply auto[1]

   531   using rsimp_ALTs.elims apply auto[1]

   532   using rsimp_ALTs.elims apply auto[1]

   533   by (smt (verit, del_insts) append_Cons append_is_Nil_conv bbbbs k0a list.inject rrexp.distinct(7) rsimp_ALTs.elims)

   534 

   535 

   536 lemma  k0:

   537   shows "rflts (r # rs1) = rflts [r] @ rflts rs1"

   538   apply(induct r arbitrary: rs1)

   539    apply(auto)

   540   done

   541 

   542 lemma flts_nil2:

   543   assumes "\<forall>y. rsize y < Suc (sum_list (map rsize rs)) \<longrightarrow>

   544             good (rsimp y) \<or> rsimp y = RZERO"

   545   and "rsimp_ALTs  (rflts (map rsimp rs)) = RZERO"

   546   shows "rflts (map rsimp rs) = []"

   547   using assms

   548   apply(induct rs)

   549    apply(simp)

   550   apply(simp)

   551   apply(subst k0)

   552   apply(simp)

   553   apply(subst (asm) k0)

   554   apply(auto)

   555   apply (metis rflts.simps(1) rflts.simps(2) flts4 k0 less_add_Suc1 list.set_intros(1))

   556   by (metis flts4 k0 less_add_Suc1 list.set_intros(1) rflts.simps(2))

   557 

   558 

   559 lemma good_SEQ:

   560   assumes "r1 \<noteq> RZERO" "r2 \<noteq> RZERO" " r1 \<noteq> RONE"

   561   shows "good (RSEQ r1 r2) = (good r1 \<and> good r2)"

   562   using assms

   563   apply(case_tac r1)

   564        apply(simp_all)

   565   apply(case_tac r2)

   566           apply(simp_all)

   567   apply(case_tac r2)

   568          apply(simp_all)

   569   apply(case_tac r2)

   570         apply(simp_all)

   571   apply(case_tac r2)

   572        apply(simp_all)

   573   done

   574 

   575 lemma rsize0:

   576   shows "0 < rsize r"

   577   apply(induct  r)

   578        apply(auto)

   579   done

   580 

   581 

   582 fun nonnested :: "rrexp \<Rightarrow> bool"

   583   where

   584   "nonnested (RALTS []) = True"

   585 | "nonnested (RALTS ((RALTS rs1) # rs2)) = False"

   586 | "nonnested (RALTS (r # rs2)) = nonnested (RALTS rs2)"

   587 | "nonnested r = True"

   588 

   589 

   590 

   591 lemma  k00:

   592   shows "rflts (rs1 @ rs2) = rflts rs1 @ rflts rs2"

   593   apply(induct rs1 arbitrary: rs2)

   594    apply(auto)

   595   by (metis append.assoc k0)

   596 

   597 

   598 

   599 

   600 lemma k0b:

   601   assumes "nonalt r" "r \<noteq> RZERO"

   602   shows "rflts [r] = [r]"

   603   using assms

   604   apply(case_tac  r)

   605   apply(simp_all)

   606   done

   607 

   608 lemma nn1:

   609   assumes "nonnested (RALTS rs)"

   610   shows "\<nexists> rs1. rflts rs = [RALTS rs1]"

   611   using assms

   612   apply(induct rs rule: rflts.induct)

   613   apply(auto)

   614   done

   615 

   616 lemma nn1q:

   617   assumes "nonnested (RALTS rs)"

   618   shows "\<nexists>rs1. RALTS rs1 \<in> set (rflts rs)"

   619   using assms

   620   apply(induct rs rule: rflts.induct)

   621   apply(auto)

   622   done

   623 

   624 lemma nn1qq:

   625   assumes "nonnested (RALTS rs)"

   626   shows "\<nexists> rs1. RALTS rs1 \<in> set rs"

   627   using assms

   628   apply(induct rs rule: rflts.induct)

   629   apply(auto)

   630   done

   631 

   632  

   633 

   634 lemma n0:

   635   shows "nonnested (RALTS rs) \<longleftrightarrow> (\<forall>r \<in> set rs. nonalt r)"

   636   apply(induct rs )

   637    apply(auto)

   638     apply (metis list.set_intros(1) nn1qq nonalt.elims(3))

   639   apply (metis nonalt.elims(2) nonnested.simps(3) nonnested.simps(4) nonnested.simps(5) nonnested.simps(6) nonnested.simps(7))

   640   using bbbbs1 apply fastforce

   641   by (metis bbbbs1 list.set_intros(2) nn1qq)

   642 

   643   

   644   

   645 

   646 lemma nn1c:

   647   assumes "\<forall>r \<in> set rs. nonnested r"

   648   shows "\<forall>r \<in> set (rflts rs). nonalt r"

   649   using assms

   650   apply(induct rs rule: rflts.induct)

   651         apply(auto)

   652   using n0 by blast

   653 

   654 lemma nn1bb:

   655   assumes "\<forall>r \<in> set rs. nonalt r"

   656   shows "nonnested (rsimp_ALTs  rs)"

   657   using assms

   658   apply(induct  rs rule: rsimp_ALTs.induct)

   659     apply(auto)

   660   using nonalt.simps(1) nonnested.elims(3) apply blast

   661   using n0 by auto

   662 

   663 lemma bsimp_ASEQ0:

   664   shows "rsimp_SEQ  r1 RZERO = RZERO"

   665   apply(induct r1)

   666   apply(auto)

   667   done

   668 

   669 lemma nn1b:

   670   shows "nonnested (rsimp r)"

   671   apply(induct r)

   672        apply(simp_all)

   673   apply(case_tac "rsimp r1 = RZERO")

   674     apply(simp)

   675  apply(case_tac "rsimp r2 = RZERO")

   676    apply(simp)

   677     apply(subst bsimp_ASEQ0)

   678   apply(simp)

   679   apply(case_tac "\<exists>bs. rsimp r1 = RONE")

   680     apply(auto)[1]

   681   using idiot apply fastforce

   682   using idiot2 nonnested.simps(11) apply presburger

   683   by (metis (mono_tags, lifting) image_iff list.set_map nn1bb nn1c rdistinct_set_equality)

   684 

   685   

   686 lemma nn1d:

   687   assumes "rsimp r = RALTS rs"

   688   shows "\<forall>r1 \<in> set rs. \<forall>  bs. r1 \<noteq> RALTS  rs2"

   689   using nn1b assms

   690   by (metis nn1qq)

   691 

   692 lemma nn_flts:

   693   assumes "nonnested (RALTS rs)"

   694   shows "\<forall>r \<in>  set (rflts rs). nonalt r"

   695   using assms

   696   apply(induct rs rule: rflts.induct)

   697         apply(auto)

   698   done

   699 

   700 lemma nonalt_flts_rd:

   701   shows "\<lbrakk>xa \<in> set (rdistinct (rflts (map rsimp rs)) {})\<rbrakk>

   702        \<Longrightarrow> nonalt xa"

   703   by (metis ex_map_conv nn1b nn1c rdistinct_set_equality)

   704 

   705 lemma distinct_accLarge_empty:

   706   shows "rset \<subseteq> rset' \<Longrightarrow> rdistinct rs rset = [] \<Longrightarrow> rdistinct rs rset' = []"

   707   apply(induct rs arbitrary: rset rset')

   708    apply simp+

   709   by (metis list.distinct(1) subsetD)

   710 

   711 lemma rsimpalts_implies1:

   712   shows " rsimp_ALTs (a # rdistinct rs {a}) = RZERO \<Longrightarrow> a = RZERO"

   713   using rsimp_ALTs.elims by auto

   714 

   715 

   716 lemma rsimpalts_implies2:

   717   shows "rsimp_ALTs (a # rdistinct rs rset) = RZERO \<Longrightarrow> rdistinct rs rset = []"

   718   by (metis append_butlast_last_id rrexp.distinct(7) rsimpalts_conscons)

   719 

   720 lemma rsimpalts_implies21:

   721   shows "rsimp_ALTs (a # rdistinct rs {a}) = RZERO \<Longrightarrow> rdistinct rs {a} = []"

   722   using rsimpalts_implies2 by blast

   723 

   724 

   725 lemma hollow_removemore_hollow:

   726   shows "rsimp_ALTs (rdistinct rs {}) = RZERO \<Longrightarrow> 

   727 rsimp_ALTs (rdistinct rs rset) = RZERO "

   728   apply(induct rs arbitrary: rset)

   729    apply simp

   730   apply simp

   731   apply(case_tac " a \<in> rset")

   732    apply simp

   733    apply(drule_tac x = "rset" in meta_spec)

   734   apply (smt (verit, best) Un_insert_left empty_iff rdistinct.elims rdistinct.simps(2) rrexp.distinct(7) rsimp_ALTs.simps(1) rsimp_ALTs.simps(3) singletonD sup_bot_left)

   735   apply simp

   736   apply(subgoal_tac "a = RZERO")

   737   apply(subgoal_tac "rdistinct rs (insert a rset) = []")

   738   using rsimp_ALTs.simps(2) apply presburger

   739    apply(subgoal_tac "rdistinct rs {a} = []")

   740   apply(subgoal_tac "{a} \<subseteq> insert a rset")

   741   apply (meson distinct_accLarge_empty)

   742     apply blast

   743   using rsimpalts_implies21 apply blast

   744   using rsimpalts_implies1 by blast

   745 

   746 lemma bsimp_ASEQ2:

   747   shows "rsimp_SEQ RONE r2 =  r2"

   748   apply(induct r2)

   749   apply(auto)

   750   done

   751 

   752 lemma elem_smaller_than_set:

   753   shows "xa \<in> set  list \<Longrightarrow> rsize xa < Suc ( sum_list (map rsize list))"

   754   apply(induct list)

   755    apply simp

   756   by (metis image_eqI le_imp_less_Suc list.set_map member_le_sum_list)

   757 

   758 

   759 lemma smaller_corresponding:

   760   shows "xa \<in> set (map rsimp list) \<Longrightarrow> \<exists>xa' \<in> set list. rsize xa \<le> rsize xa'"

   761   apply(induct list)

   762    apply simp

   763   by (metis list.set_intros(1) list.set_intros(2) list.simps(9) rsimp_mono set_ConsD)

   764 

   765 lemma simpelem_smaller_than_set:

   766   shows "xa \<in> set (map rsimp list) \<Longrightarrow> rsize xa < Suc ( sum_list (map rsize ( list)))"

   767   apply(subgoal_tac "\<exists>xa' \<in> set list. rsize xa \<le> rsize xa'")

   768    

   769   using elem_smaller_than_set order_le_less_trans apply blast

   770   using smaller_corresponding by presburger

   771 

   772 

   773 lemma rsimp_list_mono:

   774   shows "sum_list (map rsize (map rsimp rs)) \<le> sum_list (map rsize rs)"

   775   apply(induct rs)

   776    apply simp+

   777   by (simp add: add_mono_thms_linordered_semiring(1) rsimp_mono)

   778 

   779 lemma good1_obvious_but_isabelle_needs_clarification:

   780   shows "       \<lbrakk>\<forall>y. rsize y < Suc (rsize a + sum_list (map rsize list)) \<longrightarrow> good (rsimp y) \<or> rsimp y = RZERO;

   781         rsimp_ALTs (rdistinct (rflts (map rsimp list)) {}) = RZERO; good (rsimp a);

   782         xa \<in> set (rdistinct (rflts (rsimp a # map rsimp list)) {})\<rbrakk>

   783        \<Longrightarrow> rsize xa < Suc (rsize a + sum_list (map rsize list))"

   784   apply(subgoal_tac "rsize xa \<le> 

   785           sum_list (map rsize (rdistinct (rflts (rsimp a # map rsimp list)) {}))")

   786   apply(subgoal_tac "  sum_list (map rsize (rdistinct (rflts (rsimp a # map rsimp list)) {})) \<le>

   787                        sum_list (map rsize ( (rflts (rsimp a # map rsimp list))))")

   788   apply(subgoal_tac " sum_list (map rsize ( (rflts (rsimp a # map rsimp list)))) \<le>

   789                       sum_list (map rsize  (rsimp a # map rsimp list))")

   790   apply(subgoal_tac " sum_list (map rsize (rsimp a # map rsimp list)) \<le>

   791                       sum_list (map rsize (a # list))")

   792   apply simp

   793   apply (metis Cons_eq_map_conv rsimp_list_mono)

   794   using rflts_mono apply blast

   795   using rdistinct_phi_smaller apply blast

   796   using elem_smaller_than_set less_Suc_eq_le by blast

   797 

   798 (*says anything coming out of simp+flts+db will be good*)

   799 lemma good2_obv_simplified:

   800   shows " \<lbrakk>\<forall>y. rsize y < Suc (sum_list (map rsize rs)) \<longrightarrow> good (rsimp y) \<or> rsimp y = RZERO;

   801            xa \<in> set (rdistinct (rflts (map rsimp rs)) {}); good (rsimp xa) \<or> rsimp xa = RZERO\<rbrakk> \<Longrightarrow> good xa"

   802   apply(subgoal_tac " \<forall>xa' \<in> set (map rsimp rs). good xa' \<or> xa' = RZERO")

   803   prefer 2

   804   apply (simp add: elem_smaller_than_set)

   805   by (metis flts3 rdistinct_set_equality)

   806 

   807   

   808 

   809 

   810 lemma good2_obvious_but_isabelle_needs_clarification:

   811   shows "\<And>a list xa.

   812        \<lbrakk>\<forall>y. rsize y < Suc (rsize a + sum_list (map rsize list)) \<longrightarrow> good (rsimp y) \<or> rsimp y = RZERO;

   813         rsimp_ALTs (rdistinct (rflts (map rsimp list)) {}) = RZERO; good (rsimp a);

   814         xa \<in> set (rdistinct (rflts (rsimp a # map rsimp list)) {}); good (rsimp xa) \<or> rsimp xa = RZERO\<rbrakk>

   815        \<Longrightarrow> good xa"

   816   by (metis good2_obv_simplified list.simps(9) sum_list.Cons)

   817 

   818   

   819 

   820 lemma good1:

   821   shows "good (rsimp a) \<or> rsimp a = RZERO"

   822   apply(induct a taking: rsize rule: measure_induct)

   823   apply(case_tac x)

   824   apply(simp)

   825   apply(simp)

   826   apply(simp)

   827   prefer 3

   828     apply(simp)

   829    prefer 2

   830    apply(simp only:)

   831    apply simp

   832   apply (smt (verit, ccfv_threshold) add_mono_thms_linordered_semiring(1) elem_smaller_than_set good0 good2_obv_simplified le_eq_less_or_eq nonalt_flts_rd order_less_trans plus_1_eq_Suc rdistinct_does_the_job rdistinct_phi_smaller rflts_mono rsimp_ALTs.simps(1) rsimp_list_mono)

   833   apply simp

   834   apply(subgoal_tac "good (rsimp x41) \<or> rsimp x41 = RZERO")

   835    apply(subgoal_tac "good (rsimp x42) \<or> rsimp x42 = RZERO")

   836     apply(case_tac "rsimp x41 = RZERO")

   837      apply simp

   838     apply(case_tac "rsimp x42 = RZERO")

   839      apply simp

   840   using bsimp_ASEQ0 apply blast

   841     apply(subgoal_tac "good (rsimp x41)")

   842      apply(subgoal_tac "good (rsimp x42)")

   843       apply simp

   844   apply (metis bsimp_ASEQ2 good_SEQ idiot2)

   845   apply blast

   846   apply fastforce

   847   using less_add_Suc2 apply blast  

   848   using less_iff_Suc_add by blast

   551 

  1188 lemma no_alt_short_list_after_simp:

  1189   shows "RALTS rs = rsimp r \<Longrightarrow> rsimp_ALTs rs = RALTS rs"

  1190   by (metis bbbbs good1 k0a rrexp.simps(12))

  1191 

  1192 

  1193 lemma no_further_dB_after_simp:

  1194   shows "RALTS rs = rsimp r \<Longrightarrow> rdistinct rs {} = rs"

  1195   apply(subgoal_tac "good (RALTS rs)")

  1196   apply(subgoal_tac "distinct rs")

  1197   using rdistinct_on_distinct apply blast

  1198   apply (metis distinct.simps(1) distinct.simps(2) empty_iff good.simps(6) list.exhaust set_empty2)

  1199   using good1 by fastforce

   679 inductive good1 :: "rrexp \<Rightarrow> bool"

  1327 

   680   where

   681 "\<lbrakk>RZERO \<notin> set rs; \<nexists>rs1. RALTS rs1 \<in> set rs\<rbrakk> \<Longrightarrow> good1 (RALTS rs)"

   682 |"good1 RZERO"

   683 |"good1 RONE"

   684 |"good1 (RCHAR c)"

   685 |"good1 (RSEQ r1 r2)"

   686 |"good1 (RSTAR r0)"

   687 

   688 inductive goods :: "rrexp list \<Rightarrow> bool"

   689   where

   690  "goods []"

   691 |"\<lbrakk>goods rs; r \<noteq> RZERO; \<nexists>rs1. RALTS rs1 = r\<rbrakk> \<Longrightarrow> goods (r # rs)"

   692 

   693 lemma goods_good1:

   694   shows "goods rs = good1 (RALTS rs)"

   695   apply(induct rs)

   696   apply (simp add: good1.intros(1) goods.intros(1))

   697   apply(case_tac "goods rs")

   698    apply(case_tac a)

   699         apply simp

   700   using good1.simps goods.cases apply auto[1]

   701   apply (simp add: good1.simps goods.intros(2))

   702   apply (simp add: good1.simps goods.intros(2))

   703      apply (simp add: good1.simps goods.intros(2))

   704   using good1.simps goods.cases apply auto[1]

   705   apply (metis good1.cases good1.intros(1) goods.intros(2) rrexp.distinct(15) rrexp.distinct(21) rrexp.distinct(25) rrexp.distinct(29) rrexp.distinct(7) rrexp.distinct(9) rrexp.inject(3) set_ConsD)

   706   apply simp

   707   by (metis good1.cases good1.intros(1) goods.cases list.distinct(1) list.inject list.set_intros(2) rrexp.distinct(15) rrexp.distinct(29) rrexp.distinct(7) rrexp.inject(3) rrexp.simps(26) rrexp.simps(30))

   708 

   709 lemma rsimp_good10:

   710   shows "good1 (rsimp r)"

   711   apply(induct r)

   712        apply simp

   713   

   714        apply (simp add: good1.intros(2))

   715       apply simp

   716 

   717       apply (simp add: good1.intros(3))

   718   

   719   apply (simp add: good1.intros(4))

   720   sledgehammer

   721 

   722   sorry

   723 

   724 lemma rsimp_good1:

   725   shows "rsimp r = r1 \<Longrightarrow> good1 r1"

   726   using rsimp_good10 by blast

   727 

   728   

   732   sorry

  1331   by (metis no_further_dB_after_simp rdistinct_does_the_job)

   733 

  1332 

   734 

  1333 

   735 lemma rsimp_good1_2:

   736   shows "map rsimp rsa = [RALTS rs] \<Longrightarrow> good1 (RALTS rs)"

   737   by (metis Cons_eq_map_D rsimp_good1)

   738   

   769   apply(subgoal_tac "good1 (RALTS rs1)")

  1358   using flts_append rsimp_inner_idem4 by presburger

   770   prefer 2

  1359 

   771   using rsimp_good1 apply blast

  1360   

   772   using flts_append good1_flts by presburger

   773 

   784     apply(subgoal_tac "good1 (RALTS rs1)")

  1371     apply (metis good1_flatten map_eq_Cons_D no_further_dB_after_simp)

   785      apply(subgoal_tac "distinct rs1")

  1372   

   786   apply(subst rdistinct_on_distinct)

  1373   apply simp

   787   apply blast

  1374   

   788   apply(subst rdistinct_on_distinct)

  1375   apply(subgoal_tac "\<forall>r \<in> set( rflts (map rsimp rsa)). good r")

   789        apply blast

  1376    apply(case_tac "rdistinct (rflts (map rsimp rsa)) {}")

   790   using good1_flatten apply blast

  1377     apply simp

   791  

  1378    apply(case_tac "listb")

   792   using rsimp_no_dup apply force

  1379     apply simp+

   793   

  1380   apply (metis Cons_eq_appendI good1_flatten rflts.simps(3) rsimp.simps(2) rsimp_ALTs.simps(3))

   794   using rsimp_good1_2 apply presburger

  1381   by (metis (mono_tags, lifting) flts3 good1 image_iff list.set_map)

   795 

  1382 

   796    apply simp+

  1383 

   797   apply(case_tac "rflts (a # aa # lista)")

  1384 lemma last_elem_out:

   798    apply simp

  1385   shows "\<lbrakk>x \<notin> set xs; x \<notin> rset \<rbrakk> \<Longrightarrow> rdistinct (xs @ [x]) rset = rdistinct xs rset @ [x]"

   799   by (smt (verit) append_Cons append_Nil empty_iff good1_flatten list.distinct(1) rdistinct.simps(2) rsimp.simps(2) rsimp_ALTs.elims rsimp_good1)

  1386   apply(induct xs arbitrary: rset)

   800 

  1387   apply simp+

   801 

  1388   done

   802 lemma flts_good_good:

  1389 

   803   shows "\<forall>r \<in> set rs. good1 r \<Longrightarrow> good1 (RALTS (rflts rs ))"

   804   apply(induct rs)

   805    apply simp

   806   using goods.intros(1) goods_good1 apply auto[1]

   807   apply(case_tac  "a")

   808   apply simp

   809   apply (metis goods.intros(2) goods_good1 list.set_intros(2) rflts.simps(4) rrexp.distinct(1) rrexp.distinct(15))

   810      apply simp

   811   using goods.intros(2) goods_good1 apply blast

   812   using goods.intros(2) goods_good1 apply auto[1]

   813    apply(subgoal_tac "good1 a")

   814   apply (metis Un_iff good1.cases good1.intros(1) list.set_intros(2) rflts.simps(3) rrexp.distinct(15) rrexp.distinct(21) rrexp.distinct(25) rrexp.distinct(29) rrexp.distinct(7) rrexp.inject(3) set_append)

   815   apply simp

   816   by (metis goods.intros(2) goods_good1 list.set_intros(2) rflts.simps(7) rrexp.distinct(29) rrexp.distinct(9))

   817 

   818 

   819 lemma simp_flatten_aux1:

   820   shows "\<forall>r \<in> set (map rsimp rsa). good1 r"

   821   apply(induct rsa)

   822    apply(simp add: goods.intros)

   823   using rsimp_good1 by auto

   824 

   825 

   826 

   827 lemma simp_flatten_aux:

   828   shows "\<forall>r \<in> set rs. good1 r \<Longrightarrow> rflts (rdistinct (rflts rs) {}) = (rdistinct (rflts rs) {})"

   829   sorry

   835   

  1395   apply(induct rs1 arbitrary: rs2 rule: rev_induct)

   836   sorry

  1396    apply simp

  1397   apply(drule_tac x = "x # rs2" in meta_spec)

  1398   apply simp

  1399   apply(case_tac "x \<in> set xs")

  1400    apply simp

  1401   

  1402    apply (simp add: distinct_removes_middle3 insert_absorb)

  1403   apply simp

  1404   by (simp add: last_elem_out)

  1405 

  1406 

  1407   

   854   apply(subgoal_tac "\<forall>r \<in> set (map rsimp rsa). good1 r")

  1425   by (metis distinct_once_enough nonalt0_fltseq nonalt_flts_rd qqq1 rdistinct_set_equality)

   855   apply (metis distinct_once_enough simp_flatten_aux)

  1426 

   856   using simp_flatten_aux1 by blast

  1427 lemma basic_rsimp_SEQ_property1:

   857 

  1428   shows "rsimp_SEQ RONE r = r"

   858 lemma simp_flatten3:

  1429   by (simp add: idiot)

   859   shows "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = rsimp (RALTS (rsa @ rs @ rsb))"

  1430 

   860   sorry

  1431 

  1432 

  1433 lemma basic_rsimp_SEQ_property3:

  1434   shows "rsimp_SEQ r RZERO = RZERO"  

  1435   using rsimp_SEQ.elims by blast