425 

   426 lemma good_singleton:

   427   shows "good a \<and> nonalt a  \<Longrightarrow> rflts [a] = [a]"

   428   using good.simps(1) k0b by blast

   429 

   430 

   431 

   432 

   433 

   434 

   435 

   436 lemma all_that_same_elem:

   437   shows "\<lbrakk> a \<in> rset; rdistinct rs {a} = []\<rbrakk>

   438        \<Longrightarrow> rdistinct (rs @ rsb) rset = rdistinct rsb rset"

   439   apply(induct rs)

   440    apply simp

   441   apply(subgoal_tac "aa = a")

   442    apply simp

   443   by (metis empty_iff insert_iff list.discI rdistinct.simps(2))

   444 

   445 lemma distinct_early_app1:

   446   shows "rset1 \<subseteq> rset \<Longrightarrow> rdistinct rs rset = rdistinct (rdistinct rs rset1) rset"

   447   apply(induct rs arbitrary: rset rset1)

   448    apply simp

   449   apply simp

   450   apply(case_tac "a \<in> rset1")

   451    apply simp

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

   453     apply simp+

   454   

   455    apply blast

   456   apply(case_tac "a \<in> rset1")

   457    apply simp+

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

   459    apply simp

   460    apply (metis insert_subsetI)

   461   apply simp

   462   by (meson insert_mono)

   463 

   464 

   465 lemma distinct_early_app:

   466   shows " rdistinct (rs @ rsb) rset = rdistinct (rdistinct rs {} @ rsb) rset"

   467   apply(induct rsb)

   468    apply simp

   469   using distinct_early_app1 apply blast

   470   by (metis distinct_early_app1 distinct_once_enough empty_subsetI)

   471 

   472 

   473 lemma distinct_eq_interesting1:

   474   shows "a \<in> rset \<Longrightarrow> rdistinct (rs @ rsb) rset = rdistinct (rdistinct (a # rs) {} @ rsb) rset"

   475   apply(subgoal_tac "rdistinct (rdistinct (a # rs) {} @ rsb) rset = rdistinct (rdistinct rs {} @ rsb) rset")

   476    apply(simp only:)

   477   using distinct_early_app apply blast 

   478   by (metis append_Cons distinct_early_app rdistinct.simps(2))

   479 

   480 

   481 

   482 lemma good_flatten_aux_aux1:

   483   shows "\<lbrakk> size rs \<ge>2; 

   484 \<forall>r \<in> set rs. good r \<and> r \<noteq> RZERO \<and> nonalt r; \<forall>r \<in> set rsb. good r \<and> r \<noteq> RZERO \<and> nonalt r \<rbrakk>

   485        \<Longrightarrow> rdistinct (rs @ rsb) rset =

   486            rdistinct (rflts [rsimp_ALTs (rdistinct rs {})] @ rsb) rset"

   487   apply(induct rs arbitrary: rset)

   488    apply simp

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

   490    apply simp

   491    apply(case_tac "rdistinct rs {a}")

   492     apply simp

   493     apply(subst good_singleton)

   494      apply force

   495   apply simp

   496     apply (meson all_that_same_elem)

   497    apply(subgoal_tac "rflts [rsimp_ALTs (a # rdistinct rs {a})] = a # rdistinct rs {a} ")

   498   prefer 2

   499   using k0a rsimp_ALTs.simps(3) apply presburger

   500   apply(simp only:)

   501   apply(subgoal_tac "rdistinct (rs @ rsb) rset = rdistinct ((rdistinct (a # rs) {}) @ rsb) rset ")

   502     apply (metis insert_absorb insert_is_Un insert_not_empty rdistinct.simps(2))

   503    apply (meson distinct_eq_interesting1)

   504   apply simp

   505   apply(case_tac "rdistinct rs {a}")

   506   prefer 2

   507    apply(subgoal_tac "rsimp_ALTs (a # rdistinct rs {a}) = RALTS (a # rdistinct rs {a})")

   508   apply(simp only:)

   509   apply(subgoal_tac "a # rdistinct (rs @ rsb) (insert a rset) =

   510            rdistinct (rflts [RALTS (a # rdistinct rs {a})] @ rsb) rset")

   511    apply simp

   512   apply (metis append_Cons distinct_early_app empty_iff insert_is_Un k0a rdistinct.simps(2))

   513   using rsimp_ALTs.simps(3) apply presburger

   514   by (metis Un_insert_left append_Cons distinct_early_app empty_iff good_singleton rdistinct.simps(2) rsimp_ALTs.simps(2) sup_bot_left)

   515 

   516 

   517 

   518   

   519 

   520 lemma good_flatten_aux_aux:

   521   shows "\<lbrakk>\<exists>a aa lista list. rs = a # list \<and> list = aa # lista; 

   522 \<forall>r \<in> set rs. good r \<and> r \<noteq> RZERO \<and> nonalt r; \<forall>r \<in> set rsb. good r \<and> r \<noteq> RZERO \<and> nonalt r \<rbrakk>

   523        \<Longrightarrow> rdistinct (rs @ rsb) rset =

   524            rdistinct (rflts [rsimp_ALTs (rdistinct rs {})] @ rsb) rset"

   525   apply(erule exE)+

   526   apply(subgoal_tac "size rs \<ge> 2")

   527    apply (metis good_flatten_aux_aux1)

   528   by (simp add: Suc_leI length_Cons less_add_Suc1)

   529 

   530 

   531 

   532 lemma good_flatten_aux:

   533   shows " \<lbrakk>\<forall>r\<in>set rs. good r; \<forall>r\<in>set rsa. good r; \<forall>r\<in>set rsb. good r;

   534      rsimp (RALTS (rsa @ rs @ rsb)) = rsimp_ALTs (rdistinct (rflts (rsa @ rs @ rsb)) {});

   535      rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) =

   536      rsimp_ALTs (rdistinct (rflts (rsa @ [rsimp (RALTS rs)] @ rsb)) {});

   537      map rsimp rsa = rsa; map rsimp rsb = rsb; map rsimp rs = rs;

   538      rdistinct (rflts rsa @ rflts rs @ rflts rsb) {} =

   539      rdistinct (rflts rsa) {} @ rdistinct (rflts rs @ rflts rsb) (set (rflts rsa));

   540      rdistinct (rflts rsa @ rflts [rsimp (RALTS rs)] @ rflts rsb) {} =

   541      rdistinct (rflts rsa) {} @ rdistinct (rflts [rsimp (RALTS rs)] @ rflts rsb) (set (rflts rsa))\<rbrakk>

   542     \<Longrightarrow>    rdistinct (rflts rs @ rflts rsb) rset =

   543            rdistinct (rflts [rsimp (RALTS rs)] @ rflts rsb) rset"

   544   apply simp

   545   apply(case_tac "rflts rs ")

   546    apply simp

   547   apply(case_tac "list")

   548    apply simp

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

   550     apply simp

   551   apply (metis append_Cons append_Nil flts_append list.set(1) list.simps(15) nonalt.simps(1) nonalt0_flts_keeps nonalt_flts_rd qqq1 rdistinct.simps(2) rdistinct_set_equality singleton_iff)

   552    apply simp

   553   apply (metis Un_insert_left append_Cons append_Nil ex_in_conv flts_single1 insertI1 list.simps(15) nonalt_flts_rd nonazero.elims(3) qqq1 rdistinct.simps(2) sup_bot_left)

   554   apply(subgoal_tac "\<forall>r \<in> set (rflts rs). good r \<and> r \<noteq> RZERO \<and> nonalt r")

   555   prefer 2  

   556   apply (metis flts3 nn1b nn1c qqq1 test)

   557   apply(subgoal_tac "\<forall>r \<in> set (rflts rsb). good r \<and> r \<noteq> RZERO \<and> nonalt r")

   558   prefer 2  

   559   apply (metis flts3 nn1b nn1c qqq1 test)

   560   by (smt (verit, ccfv_threshold) good_flatten_aux_aux)

   561 

   562   

   563 

   564 

   565 lemma good_flatten_middle:

   566   shows "\<lbrakk>\<forall>r \<in> set rs. good r; \<forall>r \<in> set rsa. good r; \<forall>r \<in> set rsb. good r\<rbrakk> \<Longrightarrow>

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

   568   apply(subgoal_tac "rsimp (RALTS (rsa @ rs @ rsb)) = rsimp_ALTs (rdistinct (rflts (map rsimp rsa @ 

   569 map rsimp rs @ map rsimp rsb)) {})")

   570   prefer 2

   571   apply simp

   572   apply(simp only:)

   573     apply(subgoal_tac "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = rsimp_ALTs (rdistinct (rflts (map rsimp rsa @ 

   574 [rsimp (RALTS rs)] @ map rsimp rsb)) {})")

   575   prefer 2

   576    apply simp

   577   apply(simp only:)

   578   apply(subgoal_tac "map rsimp rsa = rsa")

   579   prefer 2

   580   apply (simp add: map_idI test)

   581   apply(simp only:)

   582   apply(subgoal_tac "map rsimp rsb = rsb")

   583    prefer 2

   584   apply (meson map_idI test)

   585   apply(simp only:)

   586   apply(subst k00)+

   587   apply(subgoal_tac "map rsimp rs = rs")

   588    apply(simp only:)

   589    prefer 2

   590   apply (meson map_idI test)

   591   apply(subgoal_tac "rdistinct (rflts rsa @ rflts rs @ rflts rsb) {} = 

   592 rdistinct (rflts rsa) {} @ rdistinct  (rflts rs @ rflts rsb) (set (rflts rsa))")

   593    apply(simp only:)

   594   prefer 2

   595   using rdistinct_concat_general apply blast

   596   apply(subgoal_tac "rdistinct (rflts rsa @ rflts [rsimp (RALTS rs)] @ rflts rsb) {} = 

   597 rdistinct (rflts rsa) {} @ rdistinct  (rflts [rsimp (RALTS rs)] @ rflts rsb) (set (rflts rsa))")

   598    apply(simp only:)

   599   prefer 2

   600   using rdistinct_concat_general apply blast

   601   apply(subgoal_tac "rdistinct (rflts rs @ rflts rsb) (set (rflts rsa)) = 

   602                      rdistinct  (rflts [rsimp (RALTS rs)] @ rflts rsb) (set (rflts rsa))")

   603   apply presburger

   604   using good_flatten_aux by blast

   605 

   606 

   607 lemma simp_flatten3:

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

   609   apply(subgoal_tac "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = 

   610                      rsimp (RALTS (map rsimp rsa @ [rsimp (RALTS rs)] @ map rsimp rsb)) ")

   611   prefer 2

   612    apply (metis append.left_neutral append_Cons list.simps(9) map_append simp_flatten_aux0)

   613   apply (simp only:)

   614   apply(subgoal_tac "rsimp (RALTS (rsa @ rs @ rsb)) = 

   615 rsimp (RALTS (map rsimp rsa @ map rsimp rs @ map rsimp rsb))")

   616   prefer 2

   617    apply (metis map_append simp_flatten_aux0)

   618   apply(simp only:)

   619   apply(subgoal_tac "rsimp  (RALTS (map rsimp rsa @ map rsimp rs @ map rsimp rsb)) =

   620  rsimp (RALTS (map rsimp rsa @ [RALTS (map rsimp rs)] @ map rsimp rsb))")

   621   

   622    apply (metis (no_types, lifting) head_one_more_simp map_append simp_flatten_aux0)

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

   624    apply(subgoal_tac "\<forall>r \<in> set (map rsimp rs). good r")

   625     apply(subgoal_tac "\<forall>r \<in> set (map rsimp rsb). good r")

   626   

   627   using good_flatten_middle apply presburger

   628   

   629 

   630   sorry

   631 

   632 

   633 

   634