--- a/thys2/BasicIdentities.thy Wed Apr 13 22:20:08 2022 +0100
+++ b/thys2/BasicIdentities.thy Fri Apr 15 19:35:29 2022 +0100
@@ -341,13 +341,8 @@
apply simp_all
done
-lemma no_alt_short_list_after_simp:
- shows "RALTS rs = rsimp r \<Longrightarrow> rsimp_ALTs rs = RALTS rs"
- sorry
-lemma no_further_dB_after_simp:
- shows "RALTS rs = rsimp r \<Longrightarrow> rdistinct rs {} = rs"
- sorry
+
lemma idiot2:
@@ -403,35 +398,454 @@
apply auto
done
-lemma rsimp_idem:
- shows "rsimp (rsimp r) = rsimp r"
- sorry
+
+
+fun nonalt :: "rrexp \<Rightarrow> bool"
+ where
+ "nonalt (RALTS rs) = False"
+| "nonalt r = True"
+
+
+fun good :: "rrexp \<Rightarrow> bool" where
+ "good RZERO = False"
+| "good (RONE) = True"
+| "good (RCHAR c) = True"
+| "good (RALTS []) = False"
+| "good (RALTS [r]) = False"
+| "good (RALTS (r1 # r2 # rs)) = ((distinct ( (r1 # r2 # rs))) \<and>(\<forall>r' \<in> set (r1 # r2 # rs). good r' \<and> nonalt r'))"
+| "good (RSEQ RZERO _) = False"
+| "good (RSEQ RONE _) = False"
+| "good (RSEQ _ RZERO) = False"
+| "good (RSEQ r1 r2) = (good r1 \<and> good r2)"
+| "good (RSTAR r) = True"
+
+
+lemma k0a:
+ shows "rflts [RALTS rs] = rs"
+ apply(simp)
+ done
+
+lemma bbbbs:
+ assumes "good r" "r = RALTS rs"
+ shows "rsimp_ALTs (rflts [r]) = RALTS rs"
+ using assms
+ by (metis good.simps(4) good.simps(5) k0a rsimp_ALTs.elims)
+
+lemma bbbbs1:
+ shows "nonalt r \<or> (\<exists> rs. r = RALTS rs)"
+ by (meson nonalt.elims(3))
+
+
+
+lemma good0:
+ assumes "rs \<noteq> Nil" "\<forall>r \<in> set rs. nonalt r" "distinct rs"
+ shows "good (rsimp_ALTs rs) \<longleftrightarrow> (\<forall>r \<in> set rs. good r)"
+ using assms
+ apply(induct rs rule: rsimp_ALTs.induct)
+ apply(auto)
+ done
-corollary rsimp_inner_idem1:
- shows "rsimp r = RSEQ r1 r2 \<Longrightarrow> rsimp r1 = r1 \<and> rsimp r2 = r2"
+lemma good0a:
+ assumes "rflts (map rsimp rs) \<noteq> Nil" "\<forall>r \<in> set (rflts (map rsimp rs)). nonalt r"
+ shows "good (rsimp (RALTS rs)) \<longleftrightarrow> (\<forall>r \<in> set (rflts (map rsimp rs)). good r)"
+ using assms
+ apply(simp)
+ apply(auto)
+ apply(subst (asm) good0)
- sorry
+ apply (metis rdistinct_set_equality set_empty)
+ apply(simp)
+ apply(auto)
+ apply (metis rdistinct_set_equality)
+ using rdistinct_does_the_job apply blast
+ apply (metis rdistinct_set_equality)
+ by (metis good0 rdistinct_does_the_job rdistinct_set_equality set_empty)
+
+
+lemma flts0:
+ assumes "r \<noteq> RZERO" "nonalt r"
+ shows "rflts [r] \<noteq> []"
+ using assms
+ apply(induct r)
+ apply(simp_all)
+ done
+
+lemma flts1:
+ assumes "good r"
+ shows "rflts [r] \<noteq> []"
+ using assms
+ apply(induct r)
+ apply(simp_all)
+ using good.simps(4) by blast
+
+lemma flts2:
+ assumes "good r"
+ shows "\<forall>r' \<in> set (rflts [r]). good r' \<and> nonalt r'"
+ using assms
+ apply(induct r)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ prefer 2
+ apply(simp)
+ apply(auto)[1]
+
+ apply (metis flts1 good.simps(5) good.simps(6) k0a neq_Nil_conv)
+ apply (metis flts1 good.simps(5) good.simps(6) k0a neq_Nil_conv)
+ apply fastforce
+ apply(simp)
+ done
+
-corollary rsimp_inner_idem2:
- shows "rsimp r = RALTS rs \<Longrightarrow> \<forall>r' \<in> (set rs). rsimp r' = r'"
- sorry
+
+lemma flts3:
+ assumes "\<forall>r \<in> set rs. good r \<or> r = RZERO"
+ shows "\<forall>r \<in> set (rflts rs). good r"
+ using assms
+ apply(induct rs arbitrary: rule: rflts.induct)
+ apply(simp_all)
+ by (metis UnE flts2 k0a)
+
+lemma flts3b:
+ assumes "\<exists>r\<in>set rs. good r"
+ shows "rflts rs \<noteq> []"
+ using assms
+ apply(induct rs arbitrary: rule: rflts.induct)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ apply(auto)
+ done
+
+lemma flts4:
+ assumes "rsimp_ALTs (rflts rs) = RZERO"
+ shows "\<forall>r \<in> set rs. \<not> good r"
+ using assms
+ apply(induct rs rule: rflts.induct)
+ apply(auto)
+ defer
+ 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))
+ using rsimp_ALTs.elims apply auto[1]
+ using rsimp_ALTs.elims apply auto[1]
+ using rsimp_ALTs.elims apply auto[1]
+ using rsimp_ALTs.elims apply auto[1]
+ using rsimp_ALTs.elims apply auto[1]
+ by (smt (verit, del_insts) append_Cons append_is_Nil_conv bbbbs k0a list.inject rrexp.distinct(7) rsimp_ALTs.elims)
+
+
+lemma k0:
+ shows "rflts (r # rs1) = rflts [r] @ rflts rs1"
+ apply(induct r arbitrary: rs1)
+ apply(auto)
+ done
-corollary rsimp_inner_idem3:
- shows "rsimp r = RALTS rs \<Longrightarrow> map rsimp rs = rs"
- by (meson map_idI rsimp_inner_idem2)
+lemma flts_nil2:
+ assumes "\<forall>y. rsize y < Suc (sum_list (map rsize rs)) \<longrightarrow>
+ good (rsimp y) \<or> rsimp y = RZERO"
+ and "rsimp_ALTs (rflts (map rsimp rs)) = RZERO"
+ shows "rflts (map rsimp rs) = []"
+ using assms
+ apply(induct rs)
+ apply(simp)
+ apply(simp)
+ apply(subst k0)
+ apply(simp)
+ apply(subst (asm) k0)
+ apply(auto)
+ apply (metis rflts.simps(1) rflts.simps(2) flts4 k0 less_add_Suc1 list.set_intros(1))
+ by (metis flts4 k0 less_add_Suc1 list.set_intros(1) rflts.simps(2))
+
-corollary rsimp_inner_idem4:
- shows "rsimp r = RALTS rs \<Longrightarrow> rflts rs = rs"
- sorry
+lemma good_SEQ:
+ assumes "r1 \<noteq> RZERO" "r2 \<noteq> RZERO" " r1 \<noteq> RONE"
+ shows "good (RSEQ r1 r2) = (good r1 \<and> good r2)"
+ using assms
+ apply(case_tac r1)
+ apply(simp_all)
+ apply(case_tac r2)
+ apply(simp_all)
+ apply(case_tac r2)
+ apply(simp_all)
+ apply(case_tac r2)
+ apply(simp_all)
+ apply(case_tac r2)
+ apply(simp_all)
+ done
+
+lemma rsize0:
+ shows "0 < rsize r"
+ apply(induct r)
+ apply(auto)
+ done
+
+
+fun nonnested :: "rrexp \<Rightarrow> bool"
+ where
+ "nonnested (RALTS []) = True"
+| "nonnested (RALTS ((RALTS rs1) # rs2)) = False"
+| "nonnested (RALTS (r # rs2)) = nonnested (RALTS rs2)"
+| "nonnested r = True"
+
+
+
+lemma k00:
+ shows "rflts (rs1 @ rs2) = rflts rs1 @ rflts rs2"
+ apply(induct rs1 arbitrary: rs2)
+ apply(auto)
+ by (metis append.assoc k0)
+
+
-lemma head_one_more_simp:
- shows "map rsimp (r # rs) = map rsimp (( rsimp r) # rs)"
- by (simp add: rsimp_idem)
+lemma k0b:
+ assumes "nonalt r" "r \<noteq> RZERO"
+ shows "rflts [r] = [r]"
+ using assms
+ apply(case_tac r)
+ apply(simp_all)
+ done
+
+lemma nn1:
+ assumes "nonnested (RALTS rs)"
+ shows "\<nexists> rs1. rflts rs = [RALTS rs1]"
+ using assms
+ apply(induct rs rule: rflts.induct)
+ apply(auto)
+ done
+
+lemma nn1q:
+ assumes "nonnested (RALTS rs)"
+ shows "\<nexists>rs1. RALTS rs1 \<in> set (rflts rs)"
+ using assms
+ apply(induct rs rule: rflts.induct)
+ apply(auto)
+ done
+
+lemma nn1qq:
+ assumes "nonnested (RALTS rs)"
+ shows "\<nexists> rs1. RALTS rs1 \<in> set rs"
+ using assms
+ apply(induct rs rule: rflts.induct)
+ apply(auto)
+ done
+
+
+
+lemma n0:
+ shows "nonnested (RALTS rs) \<longleftrightarrow> (\<forall>r \<in> set rs. nonalt r)"
+ apply(induct rs )
+ apply(auto)
+ apply (metis list.set_intros(1) nn1qq nonalt.elims(3))
+ apply (metis nonalt.elims(2) nonnested.simps(3) nonnested.simps(4) nonnested.simps(5) nonnested.simps(6) nonnested.simps(7))
+ using bbbbs1 apply fastforce
+ by (metis bbbbs1 list.set_intros(2) nn1qq)
+
+
+
+
+lemma nn1c:
+ assumes "\<forall>r \<in> set rs. nonnested r"
+ shows "\<forall>r \<in> set (rflts rs). nonalt r"
+ using assms
+ apply(induct rs rule: rflts.induct)
+ apply(auto)
+ using n0 by blast
+
+lemma nn1bb:
+ assumes "\<forall>r \<in> set rs. nonalt r"
+ shows "nonnested (rsimp_ALTs rs)"
+ using assms
+ apply(induct rs rule: rsimp_ALTs.induct)
+ apply(auto)
+ using nonalt.simps(1) nonnested.elims(3) apply blast
+ using n0 by auto
+
+lemma bsimp_ASEQ0:
+ shows "rsimp_SEQ r1 RZERO = RZERO"
+ apply(induct r1)
+ apply(auto)
+ done
+
+lemma nn1b:
+ shows "nonnested (rsimp r)"
+ apply(induct r)
+ apply(simp_all)
+ apply(case_tac "rsimp r1 = RZERO")
+ apply(simp)
+ apply(case_tac "rsimp r2 = RZERO")
+ apply(simp)
+ apply(subst bsimp_ASEQ0)
+ apply(simp)
+ apply(case_tac "\<exists>bs. rsimp r1 = RONE")
+ apply(auto)[1]
+ using idiot apply fastforce
+ using idiot2 nonnested.simps(11) apply presburger
+ by (metis (mono_tags, lifting) image_iff list.set_map nn1bb nn1c rdistinct_set_equality)
+
+
+lemma nn1d:
+ assumes "rsimp r = RALTS rs"
+ shows "\<forall>r1 \<in> set rs. \<forall> bs. r1 \<noteq> RALTS rs2"
+ using nn1b assms
+ by (metis nn1qq)
+
+lemma nn_flts:
+ assumes "nonnested (RALTS rs)"
+ shows "\<forall>r \<in> set (rflts rs). nonalt r"
+ using assms
+ apply(induct rs rule: rflts.induct)
+ apply(auto)
+ done
+
+lemma nonalt_flts_rd:
+ shows "\<lbrakk>xa \<in> set (rdistinct (rflts (map rsimp rs)) {})\<rbrakk>
+ \<Longrightarrow> nonalt xa"
+ by (metis ex_map_conv nn1b nn1c rdistinct_set_equality)
+
+lemma distinct_accLarge_empty:
+ shows "rset \<subseteq> rset' \<Longrightarrow> rdistinct rs rset = [] \<Longrightarrow> rdistinct rs rset' = []"
+ apply(induct rs arbitrary: rset rset')
+ apply simp+
+ by (metis list.distinct(1) subsetD)
+
+lemma rsimpalts_implies1:
+ shows " rsimp_ALTs (a # rdistinct rs {a}) = RZERO \<Longrightarrow> a = RZERO"
+ using rsimp_ALTs.elims by auto
+
+
+lemma rsimpalts_implies2:
+ shows "rsimp_ALTs (a # rdistinct rs rset) = RZERO \<Longrightarrow> rdistinct rs rset = []"
+ by (metis append_butlast_last_id rrexp.distinct(7) rsimpalts_conscons)
+
+lemma rsimpalts_implies21:
+ shows "rsimp_ALTs (a # rdistinct rs {a}) = RZERO \<Longrightarrow> rdistinct rs {a} = []"
+ using rsimpalts_implies2 by blast
+
-lemma head_one_more_dersimp:
- shows "map rsimp ((rder x (rders_simp r s) # rs)) = map rsimp ((rders_simp r (s@[x]) ) # rs)"
- using head_one_more_simp rders_simp_append rders_simp_one_char by presburger
+lemma hollow_removemore_hollow:
+ shows "rsimp_ALTs (rdistinct rs {}) = RZERO \<Longrightarrow>
+rsimp_ALTs (rdistinct rs rset) = RZERO "
+ apply(induct rs arbitrary: rset)
+ apply simp
+ apply simp
+ apply(case_tac " a \<in> rset")
+ apply simp
+ apply(drule_tac x = "rset" in meta_spec)
+ 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)
+ apply simp
+ apply(subgoal_tac "a = RZERO")
+ apply(subgoal_tac "rdistinct rs (insert a rset) = []")
+ using rsimp_ALTs.simps(2) apply presburger
+ apply(subgoal_tac "rdistinct rs {a} = []")
+ apply(subgoal_tac "{a} \<subseteq> insert a rset")
+ apply (meson distinct_accLarge_empty)
+ apply blast
+ using rsimpalts_implies21 apply blast
+ using rsimpalts_implies1 by blast
+
+lemma bsimp_ASEQ2:
+ shows "rsimp_SEQ RONE r2 = r2"
+ apply(induct r2)
+ apply(auto)
+ done
+
+lemma elem_smaller_than_set:
+ shows "xa \<in> set list \<Longrightarrow> rsize xa < Suc ( sum_list (map rsize list))"
+ apply(induct list)
+ apply simp
+ by (metis image_eqI le_imp_less_Suc list.set_map member_le_sum_list)
+
+
+lemma smaller_corresponding:
+ shows "xa \<in> set (map rsimp list) \<Longrightarrow> \<exists>xa' \<in> set list. rsize xa \<le> rsize xa'"
+ apply(induct list)
+ apply simp
+ by (metis list.set_intros(1) list.set_intros(2) list.simps(9) rsimp_mono set_ConsD)
+
+lemma simpelem_smaller_than_set:
+ shows "xa \<in> set (map rsimp list) \<Longrightarrow> rsize xa < Suc ( sum_list (map rsize ( list)))"
+ apply(subgoal_tac "\<exists>xa' \<in> set list. rsize xa \<le> rsize xa'")
+
+ using elem_smaller_than_set order_le_less_trans apply blast
+ using smaller_corresponding by presburger
+
+
+lemma rsimp_list_mono:
+ shows "sum_list (map rsize (map rsimp rs)) \<le> sum_list (map rsize rs)"
+ apply(induct rs)
+ apply simp+
+ by (simp add: add_mono_thms_linordered_semiring(1) rsimp_mono)
+
+lemma good1_obvious_but_isabelle_needs_clarification:
+ shows " \<lbrakk>\<forall>y. rsize y < Suc (rsize a + sum_list (map rsize list)) \<longrightarrow> good (rsimp y) \<or> rsimp y = RZERO;
+ rsimp_ALTs (rdistinct (rflts (map rsimp list)) {}) = RZERO; good (rsimp a);
+ xa \<in> set (rdistinct (rflts (rsimp a # map rsimp list)) {})\<rbrakk>
+ \<Longrightarrow> rsize xa < Suc (rsize a + sum_list (map rsize list))"
+ apply(subgoal_tac "rsize xa \<le>
+ sum_list (map rsize (rdistinct (rflts (rsimp a # map rsimp list)) {}))")
+ apply(subgoal_tac " sum_list (map rsize (rdistinct (rflts (rsimp a # map rsimp list)) {})) \<le>
+ sum_list (map rsize ( (rflts (rsimp a # map rsimp list))))")
+ apply(subgoal_tac " sum_list (map rsize ( (rflts (rsimp a # map rsimp list)))) \<le>
+ sum_list (map rsize (rsimp a # map rsimp list))")
+ apply(subgoal_tac " sum_list (map rsize (rsimp a # map rsimp list)) \<le>
+ sum_list (map rsize (a # list))")
+ apply simp
+ apply (metis Cons_eq_map_conv rsimp_list_mono)
+ using rflts_mono apply blast
+ using rdistinct_phi_smaller apply blast
+ using elem_smaller_than_set less_Suc_eq_le by blast
+
+(*says anything coming out of simp+flts+db will be good*)
+lemma good2_obv_simplified:
+ shows " \<lbrakk>\<forall>y. rsize y < Suc (sum_list (map rsize rs)) \<longrightarrow> good (rsimp y) \<or> rsimp y = RZERO;
+ xa \<in> set (rdistinct (rflts (map rsimp rs)) {}); good (rsimp xa) \<or> rsimp xa = RZERO\<rbrakk> \<Longrightarrow> good xa"
+ apply(subgoal_tac " \<forall>xa' \<in> set (map rsimp rs). good xa' \<or> xa' = RZERO")
+ prefer 2
+ apply (simp add: elem_smaller_than_set)
+ by (metis flts3 rdistinct_set_equality)
+
+
+
+
+lemma good2_obvious_but_isabelle_needs_clarification:
+ shows "\<And>a list xa.
+ \<lbrakk>\<forall>y. rsize y < Suc (rsize a + sum_list (map rsize list)) \<longrightarrow> good (rsimp y) \<or> rsimp y = RZERO;
+ rsimp_ALTs (rdistinct (rflts (map rsimp list)) {}) = RZERO; good (rsimp a);
+ xa \<in> set (rdistinct (rflts (rsimp a # map rsimp list)) {}); good (rsimp xa) \<or> rsimp xa = RZERO\<rbrakk>
+ \<Longrightarrow> good xa"
+ by (metis good2_obv_simplified list.simps(9) sum_list.Cons)
+
+
+
+lemma good1:
+ shows "good (rsimp a) \<or> rsimp a = RZERO"
+ apply(induct a taking: rsize rule: measure_induct)
+ apply(case_tac x)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ prefer 3
+ apply(simp)
+ prefer 2
+ apply(simp only:)
+ apply simp
+ 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)
+ apply simp
+ apply(subgoal_tac "good (rsimp x41) \<or> rsimp x41 = RZERO")
+ apply(subgoal_tac "good (rsimp x42) \<or> rsimp x42 = RZERO")
+ apply(case_tac "rsimp x41 = RZERO")
+ apply simp
+ apply(case_tac "rsimp x42 = RZERO")
+ apply simp
+ using bsimp_ASEQ0 apply blast
+ apply(subgoal_tac "good (rsimp x41)")
+ apply(subgoal_tac "good (rsimp x42)")
+ apply simp
+ apply (metis bsimp_ASEQ2 good_SEQ idiot2)
+ apply blast
+ apply fastforce
+ using less_add_Suc2 apply blast
+ using less_iff_Suc_add by blast
@@ -507,6 +921,229 @@
using RL_rder by force
+lemma good1a:
+ assumes "RL a \<noteq> {}"
+ shows "good (rsimp a)"
+ using good1 assms
+ by (metis RL.simps(1) RL_rsimp)
+
+
+
+lemma g1:
+ assumes "good (rsimp_ALTs rs)"
+ shows "rsimp_ALTs rs = RALTS rs \<or> (\<exists>r. rs = [r] \<and> rsimp_ALTs [r] = r)"
+using assms
+ apply(induct rs)
+ apply(simp)
+ apply(case_tac rs)
+ apply(simp only:)
+ apply(simp)
+ apply(case_tac list)
+ apply(simp)
+ by simp
+
+lemma flts_0:
+ assumes "nonnested (RALTS rs)"
+ shows "\<forall>r \<in> set (rflts rs). r \<noteq> RZERO"
+ using assms
+ apply(induct rs rule: rflts.induct)
+ apply(simp)
+ apply(simp)
+ defer
+ apply(simp)
+ apply(simp)
+ apply(simp)
+apply(simp)
+ apply(rule ballI)
+ apply(simp)
+ done
+
+lemma flts_0a:
+ assumes "nonnested (RALTS rs)"
+ shows "RZERO \<notin> set (rflts rs)"
+ using assms
+ using flts_0 by blast
+
+lemma qqq1:
+ shows "RZERO \<notin> set (rflts (map rsimp rs))"
+ by (metis ex_map_conv flts3 good.simps(1) good1)
+
+
+fun nonazero :: "rrexp \<Rightarrow> bool"
+ where
+ "nonazero RZERO = False"
+| "nonazero r = True"
+
+lemma flts_concat:
+ shows "rflts rs = concat (map (\<lambda>r. rflts [r]) rs)"
+ apply(induct rs)
+ apply(auto)
+ apply(subst k0)
+ apply(simp)
+ done
+
+lemma flts_single1:
+ assumes "nonalt r" "nonazero r"
+ shows "rflts [r] = [r]"
+ using assms
+ apply(induct r)
+ apply(auto)
+ done
+
+lemma flts_qq:
+ assumes "\<forall>y. rsize y < Suc (sum_list (map rsize rs)) \<longrightarrow> good y \<longrightarrow> rsimp y = y"
+ "\<forall>r'\<in>set rs. good r' \<and> nonalt r'"
+ shows "rflts (map rsimp rs) = rs"
+ using assms
+ apply(induct rs)
+ apply(simp)
+ apply(simp)
+ apply(subst k0)
+ apply(subgoal_tac "rflts [rsimp a] = [a]")
+ prefer 2
+ apply(drule_tac x="a" in spec)
+ apply(drule mp)
+ apply(simp)
+ apply(auto)[1]
+ using good.simps(1) k0b apply blast
+ apply(auto)[1]
+ done
+
+lemma sublist_distinct:
+ shows "distinct (rs1 @ rs2 ) \<Longrightarrow> distinct rs1 \<and> distinct rs2"
+ using distinct_append by blast
+
+lemma first2elem_distinct:
+ shows "distinct (a # b # rs) \<Longrightarrow> a \<noteq> b"
+ by force
+
+lemma rdistinct_does_not_remove:
+ shows "((\<forall>r \<in> rset. r \<notin> set rs) \<and> (distinct rs)) \<Longrightarrow> rdistinct rs rset = rs"
+ by (metis append.right_neutral distinct_rdistinct_append rdistinct.simps(1))
+
+lemma nonalt0_flts_keeps:
+ shows "(a \<noteq> RZERO) \<and> (\<forall>rs. a \<noteq> RALTS rs) \<Longrightarrow> rflts (a # xs) = a # rflts xs"
+ apply(case_tac a)
+ apply simp+
+ done
+
+
+lemma nonalt0_fltseq:
+ shows "\<forall>r \<in> set rs. r \<noteq> RZERO \<and> nonalt r \<Longrightarrow> rflts rs = rs"
+ apply(induct rs)
+ apply simp
+ apply(case_tac "a = RZERO")
+ apply fastforce
+ apply(case_tac "\<exists>rs1. a = RALTS rs1")
+ apply(erule exE)
+ apply simp+
+ using nonalt0_flts_keeps by presburger
+
+
+
+
+lemma goodalts_nonalt:
+ shows "good (RALTS rs) \<Longrightarrow> rflts rs = rs"
+ apply(induct x == "RALTS rs" arbitrary: rs rule: good.induct)
+ apply simp
+
+ using good.simps(5) apply blast
+ apply simp
+ apply(case_tac "r1 = RZERO")
+ using good.simps(1) apply force
+ apply(case_tac "r2 = RZERO")
+ using good.simps(1) apply force
+ apply(subgoal_tac "rflts (r1 # r2 # rs) = r1 # r2 # rflts rs")
+ prefer 2
+ apply (metis nonalt.simps(1) rflts_def_idiot)
+ apply(subgoal_tac "\<forall>r \<in> set rs. r \<noteq> RZERO \<and> nonalt r")
+ apply(subgoal_tac "rflts rs = rs")
+ apply presburger
+ using nonalt0_fltseq apply presburger
+ using good.simps(1) by blast
+
+
+
+
+
+lemma test:
+ assumes "good r"
+ shows "rsimp r = r"
+
+ using assms
+ apply(induct rule: good.induct)
+ apply simp
+ apply simp
+ apply simp
+ apply simp
+ apply simp
+ apply(subgoal_tac "distinct (r1 # r2 # rs)")
+ prefer 2
+ using good.simps(6) apply blast
+ apply(subgoal_tac "rflts (r1 # r2 # rs ) = r1 # r2 # rs")
+ prefer 2
+ using goodalts_nonalt apply blast
+
+ apply(subgoal_tac "r1 \<noteq> r2")
+ prefer 2
+ apply (meson distinct_length_2_or_more)
+ apply(subgoal_tac "r1 \<notin> set rs")
+ apply(subgoal_tac "r2 \<notin> set rs")
+ apply(subgoal_tac "\<forall>r \<in> set rs. rsimp r = r")
+ apply(subgoal_tac "map rsimp rs = rs")
+ apply simp
+ apply(subgoal_tac "\<forall>r \<in> {r1, r2}. r \<notin> set rs")
+ apply (metis distinct_not_exist rdistinct_on_distinct)
+
+ apply blast
+ apply (meson map_idI)
+ apply (metis good.simps(6) insert_iff list.simps(15))
+
+ apply (meson distinct.simps(2))
+ apply (simp add: distinct.simps(2) distinct_length_2_or_more)
+ apply simp+
+ done
+
+
+
+lemma rsimp_idem:
+ shows "rsimp (rsimp r) = rsimp r"
+ using test good1
+ by force
+
+
+
+
+
+corollary rsimp_inner_idem1:
+ shows "rsimp r = RSEQ r1 r2 \<Longrightarrow> rsimp r1 = r1 \<and> rsimp r2 = r2"
+ by (metis bsimp_ASEQ0 good.simps(7) good.simps(8) good1 good_SEQ rrexp.distinct(5) rsimp.simps(1) rsimp.simps(3) test)
+
+
+corollary rsimp_inner_idem2:
+ shows "rsimp r = RALTS rs \<Longrightarrow> \<forall>r' \<in> (set rs). rsimp r' = r'"
+ by (metis flts2 good1 k0a rrexp.simps(12) test)
+
+
+corollary rsimp_inner_idem3:
+ shows "rsimp r = RALTS rs \<Longrightarrow> map rsimp rs = rs"
+ by (meson map_idI rsimp_inner_idem2)
+
+corollary rsimp_inner_idem4:
+ shows "rsimp r = RALTS rs \<Longrightarrow> rflts rs = rs"
+ by (metis good1 goodalts_nonalt rrexp.simps(12))
+
+
+lemma head_one_more_simp:
+ shows "map rsimp (r # rs) = map rsimp (( rsimp r) # rs)"
+ by (simp add: rsimp_idem)
+
+lemma head_one_more_dersimp:
+ shows "map rsimp ((rder x (rders_simp r s) # rs)) = map rsimp ((rders_simp r (s@[x]) ) # rs)"
+ using head_one_more_simp rders_simp_append rders_simp_one_char by presburger
+
+
+
lemma der_simp_nullability:
shows "rnullable r = rnullable (rsimp r)"
using RL_rnullable RL_rsimp by auto
@@ -548,8 +1185,19 @@
+lemma no_alt_short_list_after_simp:
+ shows "RALTS rs = rsimp r \<Longrightarrow> rsimp_ALTs rs = RALTS rs"
+ by (metis bbbbs good1 k0a rrexp.simps(12))
+lemma no_further_dB_after_simp:
+ shows "RALTS rs = rsimp r \<Longrightarrow> rdistinct rs {} = rs"
+ apply(subgoal_tac "good (RALTS rs)")
+ apply(subgoal_tac "distinct rs")
+ using rdistinct_on_distinct apply blast
+ apply (metis distinct.simps(1) distinct.simps(2) empty_iff good.simps(6) list.exhaust set_empty2)
+ using good1 by fastforce
+
lemma idem_after_simp1:
shows "rsimp_ALTs (rdistinct (rflts [rsimp aa]) {}) = rsimp aa"
@@ -676,66 +1324,13 @@
-inductive good1 :: "rrexp \<Rightarrow> bool"
- where
-"\<lbrakk>RZERO \<notin> set rs; \<nexists>rs1. RALTS rs1 \<in> set rs\<rbrakk> \<Longrightarrow> good1 (RALTS rs)"
-|"good1 RZERO"
-|"good1 RONE"
-|"good1 (RCHAR c)"
-|"good1 (RSEQ r1 r2)"
-|"good1 (RSTAR r0)"
-inductive goods :: "rrexp list \<Rightarrow> bool"
- where
- "goods []"
-|"\<lbrakk>goods rs; r \<noteq> RZERO; \<nexists>rs1. RALTS rs1 = r\<rbrakk> \<Longrightarrow> goods (r # rs)"
-
-lemma goods_good1:
- shows "goods rs = good1 (RALTS rs)"
- apply(induct rs)
- apply (simp add: good1.intros(1) goods.intros(1))
- apply(case_tac "goods rs")
- apply(case_tac a)
- apply simp
- using good1.simps goods.cases apply auto[1]
- apply (simp add: good1.simps goods.intros(2))
- apply (simp add: good1.simps goods.intros(2))
- apply (simp add: good1.simps goods.intros(2))
- using good1.simps goods.cases apply auto[1]
- 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)
- apply simp
- 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))
-
-lemma rsimp_good10:
- shows "good1 (rsimp r)"
- apply(induct r)
- apply simp
-
- apply (simp add: good1.intros(2))
- apply simp
-
- apply (simp add: good1.intros(3))
-
- apply (simp add: good1.intros(4))
- sledgehammer
-
- sorry
-
-lemma rsimp_good1:
- shows "rsimp r = r1 \<Longrightarrow> good1 r1"
- using rsimp_good10 by blast
-
-
lemma rsimp_no_dup:
shows "rsimp r = RALTS rs \<Longrightarrow> distinct rs"
- sorry
+ by (metis no_further_dB_after_simp rdistinct_does_the_job)
-lemma rsimp_good1_2:
- shows "map rsimp rsa = [RALTS rs] \<Longrightarrow> good1 (RALTS rs)"
- by (metis Cons_eq_map_D rsimp_good1)
-
lemma simp_singlealt_flatten:
@@ -751,12 +1346,6 @@
by (metis no_alt_short_list_after_simp)
-lemma good1_flts:
- shows "good1 (RALTS rs1) \<Longrightarrow> rflts rs1 = rs1"
- apply(induct rs1)
- apply simp
- by (metis good1.cases good1.intros(1) list.set_intros(1) rflts_def_idiot rrexp.distinct(21) rrexp.distinct(25) rrexp.distinct(29) rrexp.inject(3) rsimp.simps(3) rsimp.simps(4) rsimp_inner_idem4 set_subset_Cons subsetD)
-
lemma good1_flatten:
@@ -766,11 +1355,9 @@
apply simp+
apply(subgoal_tac "rflts (rs1 @ map rsimp rsb) = rs1 @ rflts (map rsimp rsb)")
apply simp
- apply(subgoal_tac "good1 (RALTS rs1)")
- prefer 2
- using rsimp_good1 apply blast
- using flts_append good1_flts by presburger
+ using flts_append rsimp_inner_idem4 by presburger
+
lemma flatten_rsimpalts:
shows "rflts (rsimp_ALTs (rdistinct (rflts (map rsimp rsa)) {}) # map rsimp rsb) =
rflts ( (rdistinct (rflts (map rsimp rsa)) {}) @ map rsimp rsb)"
@@ -781,59 +1368,43 @@
apply(case_tac a)
apply simp+
apply(rename_tac rs1)
- apply(subgoal_tac "good1 (RALTS rs1)")
- apply(subgoal_tac "distinct rs1")
- apply(subst rdistinct_on_distinct)
- apply blast
- apply(subst rdistinct_on_distinct)
- apply blast
- using good1_flatten apply blast
-
- using rsimp_no_dup apply force
+ apply (metis good1_flatten map_eq_Cons_D no_further_dB_after_simp)
+
+ apply simp
- using rsimp_good1_2 apply presburger
-
- apply simp+
- apply(case_tac "rflts (a # aa # lista)")
- apply simp
- 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)
+ apply(subgoal_tac "\<forall>r \<in> set( rflts (map rsimp rsa)). good r")
+ apply(case_tac "rdistinct (rflts (map rsimp rsa)) {}")
+ apply simp
+ apply(case_tac "listb")
+ apply simp+
+ apply (metis Cons_eq_appendI good1_flatten rflts.simps(3) rsimp.simps(2) rsimp_ALTs.simps(3))
+ by (metis (mono_tags, lifting) flts3 good1 image_iff list.set_map)
-lemma flts_good_good:
- shows "\<forall>r \<in> set rs. good1 r \<Longrightarrow> good1 (RALTS (rflts rs ))"
- apply(induct rs)
- apply simp
- using goods.intros(1) goods_good1 apply auto[1]
- apply(case_tac "a")
- apply simp
- apply (metis goods.intros(2) goods_good1 list.set_intros(2) rflts.simps(4) rrexp.distinct(1) rrexp.distinct(15))
- apply simp
- using goods.intros(2) goods_good1 apply blast
- using goods.intros(2) goods_good1 apply auto[1]
- apply(subgoal_tac "good1 a")
- 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)
- apply simp
- by (metis goods.intros(2) goods_good1 list.set_intros(2) rflts.simps(7) rrexp.distinct(29) rrexp.distinct(9))
+lemma last_elem_out:
+ shows "\<lbrakk>x \<notin> set xs; x \<notin> rset \<rbrakk> \<Longrightarrow> rdistinct (xs @ [x]) rset = rdistinct xs rset @ [x]"
+ apply(induct xs arbitrary: rset)
+ apply simp+
+ done
-lemma simp_flatten_aux1:
- shows "\<forall>r \<in> set (map rsimp rsa). good1 r"
- apply(induct rsa)
- apply(simp add: goods.intros)
- using rsimp_good1 by auto
-
-
-
-lemma simp_flatten_aux:
- shows "\<forall>r \<in> set rs. good1 r \<Longrightarrow> rflts (rdistinct (rflts rs) {}) = (rdistinct (rflts rs) {})"
- sorry
-
lemma rdistinct_concat_general:
shows "rdistinct (rs1 @ rs2) {} = (rdistinct rs1 {}) @ (rdistinct rs2 (set rs1))"
+ apply(induct rs1 arbitrary: rs2 rule: rev_induct)
+ apply simp
+ apply(drule_tac x = "x # rs2" in meta_spec)
+ apply simp
+ apply(case_tac "x \<in> set xs")
+ apply simp
- sorry
+ apply (simp add: distinct_removes_middle3 insert_absorb)
+ apply simp
+ by (simp add: last_elem_out)
+
+
+
lemma distinct_once_enough:
shows "rdistinct (rs @ rsa) {} = rdistinct (rdistinct rs {} @ rsa) {}"
@@ -851,13 +1422,17 @@
apply simp
apply(subst flatten_rsimpalts)
apply(simp add: flts_append)
- apply(subgoal_tac "\<forall>r \<in> set (map rsimp rsa). good1 r")
- apply (metis distinct_once_enough simp_flatten_aux)
- using simp_flatten_aux1 by blast
+ by (metis distinct_once_enough nonalt0_fltseq nonalt_flts_rd qqq1 rdistinct_set_equality)
+
+lemma basic_rsimp_SEQ_property1:
+ shows "rsimp_SEQ RONE r = r"
+ by (simp add: idiot)
-lemma simp_flatten3:
- shows "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = rsimp (RALTS (rsa @ rs @ rsb))"
- sorry
+
+
+lemma basic_rsimp_SEQ_property3:
+ shows "rsimp_SEQ r RZERO = RZERO"
+ using rsimp_SEQ.elims by blast