--- a/thys2/BasicIdentities.thy Fri Apr 01 23:18:00 2022 +0100
+++ b/thys2/BasicIdentities.thy Sun Apr 03 22:12:27 2022 +0100
@@ -53,6 +53,14 @@
(if x \<in> acc then rdistinct xs acc
else x # (rdistinct xs ({x} \<union> acc)))"
+lemma rdistinct_does_the_job:
+ shows "distinct (rdistinct rs s)"
+ apply(induct rs arbitrary: s)
+ apply simp
+ apply simp
+ sorry
+
+
lemma rdistinct_concat:
shows "set rs \<subseteq> rset \<Longrightarrow> rdistinct (rs @ rsa) rset = rdistinct rsa rset"
apply(induct rs)
@@ -76,6 +84,38 @@
apply simp
done
+lemma rdistinct_on_distinct:
+ shows "distinct rs \<Longrightarrow> rdistinct rs {} = rs"
+ apply(induct rs)
+ apply simp
+ apply(subgoal_tac "rdistinct rs {} = rs")
+ prefer 2
+ apply simp
+ using distinct_not_exist by fastforce
+
+lemma distinct_rdistinct_append:
+ shows "distinct rs1 \<Longrightarrow> rdistinct (rs1 @ rsa) {} = rs1 @ (rdistinct rsa (set rs1))"
+ sorry
+
+lemma rdistinct_concat_general:
+ shows "rdistinct (rs1 @ rs2) {} = (rdistinct rs1 {}) @ (rdistinct rs2 (set rs1))"
+ sorry
+
+lemma rdistinct_set_equality:
+ shows "set (rdistinct rs {}) = set rs"
+ sorry
+
+lemma distinct_once_enough:
+ shows "rdistinct (rs @ rsa) {} = rdistinct (rdistinct rs {} @ rsa) {}"
+ apply(subgoal_tac "distinct (rdistinct rs {})")
+ apply(subgoal_tac
+" rdistinct (rdistinct rs {} @ rsa) {} = rdistinct rs {} @ (rdistinct rsa (set rs))")
+ apply(simp only:)
+ using rdistinct_concat_general apply blast
+ apply (simp add: distinct_rdistinct_append rdistinct_set_equality)
+ by (simp add: rdistinct_does_the_job)
+
+
fun rflts :: "rrexp list \<Rightarrow> rrexp list"
where
@@ -84,6 +124,29 @@
| "rflts ((RALTS rs1) # rs) = rs1 @ rflts rs"
| "rflts (r1 # rs) = r1 # rflts rs"
+lemma rflts_def_idiot:
+ shows "\<lbrakk> a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1\<rbrakk>
+ \<Longrightarrow> rflts (a # rs) = a # rflts rs"
+ apply(case_tac a)
+ apply simp_all
+ done
+
+lemma rflts_def_idiot2:
+ shows "\<lbrakk>a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1; a \<in> set rs\<rbrakk> \<Longrightarrow> a \<in> set (rflts rs)"
+ apply(induct rs)
+ apply simp
+ by (metis append.assoc in_set_conv_decomp insert_iff list.simps(15) rflts.simps(2) rflts.simps(3) rflts_def_idiot)
+
+
+
+lemma flts_append:
+ shows "rflts (rs1 @ rs2) = rflts rs1 @ rflts rs2"
+ apply(induct rs1)
+ apply simp
+ apply(case_tac a)
+ apply simp+
+ done
+
fun rsimp_ALTs :: " rrexp list \<Rightarrow> rrexp"
where
@@ -187,12 +250,7 @@
shows "rsize (RALTS rs) \<le> Suc ( sum_list (map rsize rs)) "
by simp
-lemma rflts_def_idiot:
- shows "\<lbrakk> a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1\<rbrakk>
- \<Longrightarrow> rflts (a # rs) = a # rflts rs"
- apply(case_tac a)
- apply simp_all
- done
+
lemma rflts_mono:
@@ -318,12 +376,7 @@
by force
-lemma rdistinct_does_the_job:
- shows "distinct (rdistinct rs s)"
- apply(induct rs arbitrary: s)
- apply simp
- apply simp
- sorry
+
lemma rders_simp_same_simpders:
shows "s \<noteq> [] \<Longrightarrow> rders_simp r s = rsimp (rders r s)"
@@ -417,17 +470,280 @@
+lemma idem_after_simp1:
+ shows "rsimp_ALTs (rdistinct (rflts [rsimp aa]) {}) = rsimp aa"
+ apply(case_tac "rsimp aa")
+ apply simp+
+ apply (metis no_alt_short_list_after_simp no_further_dB_after_simp)
+ by simp
+
+lemma identity_wwo0:
+ shows "rsimp (rsimp_ALTs (RZERO # rs)) = rsimp (rsimp_ALTs rs)"
+ by (metis idem_after_simp1 list.exhaust list.simps(8) list.simps(9) rflts.simps(2) rsimp.simps(2) rsimp.simps(3) rsimp_ALTs.simps(1) rsimp_ALTs.simps(2) rsimp_ALTs.simps(3))
+
+
+lemma distinct_removes_last:
+ shows "\<lbrakk>a \<in> set as\<rbrakk>
+ \<Longrightarrow> rdistinct as rset = rdistinct (as @ [a]) rset"
+and "rdistinct (ab # as @ [ab]) rset1 = rdistinct (ab # as) rset1"
+ apply(induct as arbitrary: rset ab rset1 a)
+ apply simp
+ apply simp
+ apply(case_tac "aa \<in> rset")
+ apply(case_tac "a = aa")
+ apply (metis append_Cons)
+ apply simp
+ apply(case_tac "a \<in> set as")
+ apply (metis append_Cons rdistinct.simps(2) set_ConsD)
+ apply(case_tac "a = aa")
+ prefer 2
+ apply simp
+ apply (metis append_Cons)
+ apply(case_tac "ab \<in> rset1")
+ prefer 2
+ apply(subgoal_tac "rdistinct (ab # (a # as) @ [ab]) rset1 =
+ ab # (rdistinct ((a # as) @ [ab]) (insert ab rset1))")
+ prefer 2
+ apply force
+ apply(simp only:)
+ apply(subgoal_tac "rdistinct (ab # a # as) rset1 = ab # (rdistinct (a # as) (insert ab rset1))")
+ apply(simp only:)
+ apply(subgoal_tac "rdistinct ((a # as) @ [ab]) (insert ab rset1) = rdistinct (a # as) (insert ab rset1)")
+ apply blast
+ apply(case_tac "a \<in> insert ab rset1")
+ apply simp
+ apply (metis insertI1)
+ apply simp
+ apply (meson insertI1)
+ apply simp
+ apply(subgoal_tac "rdistinct ((a # as) @ [ab]) rset1 = rdistinct (a # as) rset1")
+ apply simp
+ by (metis append_Cons insert_iff insert_is_Un rdistinct.simps(2))
+
+
+lemma distinct_removes_middle:
+ shows "\<lbrakk>a \<in> set as\<rbrakk>
+ \<Longrightarrow> rdistinct (as @ as2) rset = rdistinct (as @ [a] @ as2) rset"
+and "rdistinct (ab # as @ [ab] @ as3) rset1 = rdistinct (ab # as @ as3) rset1"
+ apply(induct as arbitrary: rset rset1 ab as2 as3 a)
+ apply simp
+ apply simp
+ apply(case_tac "a \<in> rset")
+ apply simp
+ apply metis
+ apply simp
+ apply (metis insertI1)
+ apply(case_tac "a = ab")
+ apply simp
+ apply(case_tac "ab \<in> rset")
+ apply simp
+ apply presburger
+ apply (meson insertI1)
+ apply(case_tac "a \<in> rset")
+ apply (metis (no_types, opaque_lifting) Un_insert_left append_Cons insert_iff rdistinct.simps(2) sup_bot_left)
+ apply(case_tac "ab \<in> rset")
+ apply simp
+ apply (meson insert_iff)
+ apply simp
+ by (metis insertI1)
+
+
+lemma distinct_removes_middle3:
+ shows "\<lbrakk>a \<in> set as\<rbrakk>
+ \<Longrightarrow> rdistinct (as @ a #as2) rset = rdistinct (as @ as2) rset"
+ using distinct_removes_middle(1) by fastforce
+
+lemma distinct_removes_last2:
+ shows "\<lbrakk>a \<in> set as\<rbrakk>
+ \<Longrightarrow> rdistinct as rset = rdistinct (as @ [a]) rset"
+ by (simp add: distinct_removes_last(1))
+
+lemma distinct_removes_middle2:
+ shows "a \<in> set as \<Longrightarrow> rdistinct (as @ [a] @ rs) {} = rdistinct (as @ rs) {}"
+ by (metis distinct_removes_middle(1))
+
+lemma distinct_removes_list:
+ shows "\<lbrakk> \<forall>r \<in> set rs. r \<in> set as\<rbrakk> \<Longrightarrow> rdistinct (as @ rs) {} = rdistinct as {}"
+ apply(induct rs)
+ apply simp+
+ apply(subgoal_tac "rdistinct (as @ a # rs) {} = rdistinct (as @ rs) {}")
+ prefer 2
+ apply (metis append_Cons append_Nil distinct_removes_middle(1))
+ by presburger
+
+
+lemma spawn_simp_rsimpalts:
+ shows "rsimp (rsimp_ALTs rs) = rsimp (rsimp_ALTs (map rsimp rs))"
+ apply(cases rs)
+ apply simp
+ apply(case_tac list)
+ apply simp
+ apply(subst rsimp_idem[symmetric])
+ apply simp
+ apply(subgoal_tac "rsimp_ALTs rs = RALTS rs")
+ apply(simp only:)
+ apply(subgoal_tac "rsimp_ALTs (map rsimp rs) = RALTS (map rsimp rs)")
+ apply(simp only:)
+ prefer 2
+ apply simp
+ prefer 2
+ using rsimp_ALTs.simps(3) apply presburger
+ apply auto
+ apply(subst rsimp_idem)+
+ by (metis comp_apply rsimp_idem)
+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_good1:
+ shows "rsimp r = r1 \<Longrightarrow> good1 r1"
+
+ sorry
+
+lemma rsimp_no_dup:
+ shows "rsimp r = RALTS rs \<Longrightarrow> distinct rs"
+ sorry
+
+
+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:
+ shows "rsimp (RALTS [RALTS rsa]) = rsimp (RALTS (rsa @ []))"
+ apply(induct rsa)
+ apply simp
+ apply simp
+ by (metis idem_after_simp1 list.simps(9) rsimp.simps(2))
+
+
+lemma good1_rsimpalts:
+ shows "rsimp r = RALTS rs \<Longrightarrow> rsimp_ALTs rs = RALTS rs"
+ 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:
+ shows "\<lbrakk> rsimp r = (RALTS rs1)\<rbrakk>
+ \<Longrightarrow> rflts (rsimp_ALTs rs1 # map rsimp rsb) = rflts (rs1 @ map rsimp rsb)"
+ apply(subst good1_rsimpalts)
+ 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
+
+lemma flatten_rsimpalts:
+ shows "rflts (rsimp_ALTs (rdistinct (rflts (map rsimp rsa)) {}) # map rsimp rsb) =
+ rflts ( (rdistinct (rflts (map rsimp rsa)) {}) @ map rsimp rsb)"
+ apply(case_tac "map rsimp rsa")
+ apply simp
+ apply(case_tac "list")
+ apply simp
+ 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
+
+ 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)
+
+
+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 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 simp_flatten:
shows "rsimp (RALTS ((RALTS rsa) # rsb)) = rsimp (RALTS (rsa @ rsb))"
+ 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
+lemma simp_flatten3:
+ shows "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = rsimp (RALTS (rsa @ rs @ rsb))"
sorry
@@ -455,7 +771,105 @@
| "star_updates (c # cs) r Ss = star_updates cs r (star_update c r Ss)"
+lemma distinct_flts_no0:
+ shows " rflts (map rsimp (rdistinct rs (insert RZERO rset))) =
+ rflts (map rsimp (rdistinct rs rset)) "
+
+ apply(induct rs arbitrary: rset)
+ apply simp
+ apply(case_tac a)
+ apply simp+
+ apply (smt (verit, ccfv_SIG) rflts.simps(2) rflts.simps(3) rflts_def_idiot)
+ prefer 2
+ apply simp
+ by (smt (verit, ccfv_threshold) Un_insert_right insert_iff list.simps(9) rdistinct.simps(2) rflts.simps(2) rflts.simps(3) rflts_def_idiot rrexp.distinct(7))
+lemma flts_removes0:
+ shows " rflts (rs @ [RZERO]) =
+ rflts rs"
+ apply(induct rs)
+ apply simp
+ by (metis append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
+
+
+lemma rflts_spills_last:
+ shows "a = RALTS rs \<Longrightarrow> rflts (rs1 @ [a]) = rflts rs1 @ rs"
+ apply (induct rs1)
+ apply simp
+ by (metis append.assoc append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
+
+lemma flts_keeps1:
+ shows " rflts (rs @ [RONE]) =
+ rflts rs @ [RONE] "
+ apply (induct rs)
+ apply simp
+ by (metis append.assoc append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
+
+lemma flts_keeps_others:
+ shows "\<lbrakk>a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1\<rbrakk> \<Longrightarrow>rflts (rs @ [a]) = rflts rs @ [a]"
+ apply(induct rs)
+ apply simp
+ apply (simp add: rflts_def_idiot)
+ apply(case_tac a)
+ apply simp
+ using flts_keeps1 apply blast
+ apply (metis append.assoc append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
+ apply (metis append.assoc append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
+ apply blast
+ by (metis append.assoc append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
+
+lemma spilled_alts_contained:
+ shows "\<lbrakk>a = RALTS rs ; a \<in> set rs1\<rbrakk> \<Longrightarrow> \<forall>r \<in> set rs. r \<in> set (rflts rs1)"
+ apply(induct rs1)
+ apply simp
+ apply(case_tac "a = aa")
+ apply simp
+ apply(subgoal_tac " a \<in> set rs1")
+ prefer 2
+ apply (meson set_ConsD)
+ apply(case_tac aa)
+ using rflts.simps(2) apply presburger
+ apply fastforce
+ apply fastforce
+ apply fastforce
+ apply fastforce
+ by fastforce
+
+
+lemma distinct_removes_duplicate_flts:
+ shows " a \<in> set rsa
+ \<Longrightarrow> rdistinct (rflts (map rsimp rsa @ [rsimp a])) {} =
+ rdistinct (rflts (map rsimp rsa)) {}"
+ apply(subgoal_tac "rsimp a \<in> set (map rsimp rsa)")
+ prefer 2
+ apply simp
+ apply(induct "rsimp a")
+ apply simp
+ using flts_removes0 apply presburger
+ apply(subgoal_tac " rdistinct (rflts (map rsimp rsa @ [rsimp a])) {} =
+ rdistinct (rflts (map rsimp rsa @ [RONE])) {}")
+ apply (simp only:)
+ apply(subst flts_keeps1)
+ apply (metis distinct_removes_last2 rflts_def_idiot2 rrexp.simps(20) rrexp.simps(6))
+ apply presburger
+ apply(subgoal_tac " rdistinct (rflts (map rsimp rsa @ [rsimp a])) {} =
+ rdistinct ((rflts (map rsimp rsa)) @ [RCHAR x]) {}")
+ apply (simp only:)
+ prefer 2
+ apply (metis flts_keeps_others rrexp.distinct(21) rrexp.distinct(3))
+ apply (metis distinct_removes_last2 rflts_def_idiot2 rrexp.distinct(21) rrexp.distinct(3))
+
+ apply (metis distinct_removes_last2 flts_keeps_others rflts_def_idiot2 rrexp.distinct(25) rrexp.distinct(5))
+ prefer 2
+ apply (metis distinct_removes_last2 flts_keeps_others flts_removes0 rflts_def_idiot2 rrexp.distinct(29))
+ apply(subgoal_tac "rflts (map rsimp rsa @ [rsimp a]) = rflts (map rsimp rsa) @ x")
+ prefer 2
+ apply (simp add: rflts_spills_last)
+ apply(simp only:)
+ apply(subgoal_tac "\<forall> r \<in> set x. r \<in> set (rflts (map rsimp rsa))")
+ prefer 2
+ using spilled_alts_contained apply presburger
+ using distinct_removes_list by blast