--- a/thys2/ClosedForms.thy Wed Mar 23 10:09:32 2022 +0000
+++ b/thys2/ClosedForms.thy Thu Mar 24 20:52:34 2022 +0000
@@ -2,15 +2,17 @@
"BasicIdentities"
begin
-lemma add0_isomorphic:
- shows "rsimp_ALTs (rdistinct (rflts [rsimp r, RZERO]) {}) = rsimp r"
- sorry
-
+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 distinct_removes_last:
- shows "\<lbrakk>(a::rrexp) \<in> set as\<rbrakk>
+ 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)
@@ -48,36 +50,61 @@
by (metis append_Cons insert_iff insert_is_Un rdistinct.simps(2))
-lemma distinct_removes_last2:
- shows "\<lbrakk>(a::rrexp) \<in> set as\<rbrakk>
- \<Longrightarrow> rdistinct as rset = rdistinct (as @ [a]) rset"
- using distinct_removes_last(1) by presburger
-
-lemma distinct_append_simp:
- shows " rsimp (rsimp_ALTs rs1) = rsimp (rsimp_ALTs rs2) \<Longrightarrow>
- rsimp (rsimp_ALTs (f a # rs1)) =
- rsimp (rsimp_ALTs (f a # rs2))"
- apply(case_tac rs1)
+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(case_tac rs2)
- apply simp
+ apply (metis insertI1)
+ apply(case_tac "a = ab")
apply simp
- prefer 2
- apply(case_tac list)
- apply(case_tac rs2)
- apply simp
- using add0_isomorphic apply blast
+ apply(case_tac "ab \<in> rset")
apply simp
- sorry
-
-(* apply (smt (z3) append.right_neutral empty_iff list.distinct(1) list.inject no_alt_short_list_after_simp no_further_dB_after_simp rdistinct.elims rflts.elims rflts.simps(2) rsimp_ALTs.simps(1) rsimp_ALTs.simps(2)))*)
+ 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>a \<in> set as; \<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 @ aa # rs) {} = rdistinct (as @ rs) {}")
+ prefer 2
+ apply (metis append_Cons append_Nil distinct_removes_middle(1))
+ by presburger
lemma simp_rdistinct_f: shows
-"f ` rset = frset \<Longrightarrow> rsimp (rsimp_ALTs (map f (rdistinct rs rset))) = rsimp (rsimp_ALTs (rdistinct (map f rs) frset)) "
+"f ` rset = frset \<Longrightarrow> rsimp (rsimp_ALTs (map f (rdistinct rs rset))) =
+ rsimp (rsimp_ALTs (rdistinct (map f rs) frset)) "
apply(induct rs arbitrary: rset)
apply simp
apply(case_tac "a \<in> rset")
@@ -209,14 +236,259 @@
oops
+lemma simp_more_distinct1:
+ shows "rsimp (rsimp_ALTs rs) = rsimp (rsimp_ALTs (rdistinct rs {}))"
+ apply(induct rs)
+ apply simp
+ apply simp
+ oops
+
+
+(*
+\<and>
+ rsimp (rsimp_ALTs (rsb @ (rdistinct rs (set rsb)))) =
+ rsimp (rsimp_ALTs (rsb @ (rdistinct (rflts rs) (set rsb))))
+*)
+lemma simp_removes_duplicate2:
+ shows "a "
+
+ oops
+
+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 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 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 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 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
+ by (metis append_self_conv distinct_removes_list in_set_conv_decomp rev_exhaust)
+
+lemma flts_middle0:
+ shows "rflts (rsa @ RZERO # rsb) = rflts (rsa @ rsb)"
+ apply(induct rsa)
+ apply simp
+ by (metis append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot)
+
+lemma flts_middle01:
+ shows "rflts (rsa @ [RZERO] @ rsb) = rflts (rsa @ rsb)"
+ by (simp add: flts_middle0)
+
+lemma flts_append1:
+ shows "\<lbrakk>a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1; a \<in> set rs\<rbrakk> \<Longrightarrow>
+ rflts (rsa @ [a] @ rsb) = rflts rsa @ [a] @ (rflts rsb)"
+ apply(induct rsa arbitrary: rsb)
+ apply simp
+ using rflts_def_idiot apply presburger
+ apply(case_tac aa)
+ apply simp+
+ done
+
+lemma flts_append:
+ shows "rflts (rs1 @ rs2) = rflts rs1 @ rflts rs2"
+ apply(induct rs1)
+ apply simp
+ apply(case_tac a)
+ apply simp+
+ done
+
+lemma simp_removes_duplicate1:
+ shows " a \<in> set rsa \<Longrightarrow> rsimp (RALTS (rsa @ [a])) = rsimp (RALTS (rsa))"
+and " rsimp (RALTS (a1 # rsa @ [a1])) = rsimp (RALTS (a1 # rsa))"
+ apply(induct rsa arbitrary: a1)
+ apply simp
+ apply simp
+ prefer 2
+ apply(case_tac "a = aa")
+ apply simp
+ apply simp
+ apply (metis Cons_eq_appendI Cons_eq_map_conv distinct_removes_duplicate_flts list.set_intros(2))
+ apply (metis append_Cons append_Nil distinct_removes_duplicate_flts list.set_intros(1) list.simps(8) list.simps(9))
+ by (metis (mono_tags, lifting) append_Cons distinct_removes_duplicate_flts list.set_intros(1) list.simps(8) list.simps(9) map_append rsimp.simps(2))
+
+lemma simp_removes_duplicate2:
+ shows "a \<in> set rsa \<Longrightarrow> rsimp (RALTS (rsa @ [a] @ rsb)) = rsimp (RALTS (rsa @ rsb))"
+ apply(induct rsb arbitrary: rsa)
+ apply simp
+ using distinct_removes_duplicate_flts apply auto[1]
+ by (metis append.assoc head_one_more_simp rsimp.simps(2) simp_flatten simp_removes_duplicate1(1))
+
+lemma simp_removes_duplicate3:
+ shows "a \<in> set rsa \<Longrightarrow> rsimp (RALTS (rsa @ a # rsb)) = rsimp (RALTS (rsa @ rsb))"
+ using simp_removes_duplicate2 by auto
+
+lemma distinct_removes_middle4:
+ shows "a \<in> set rsa \<Longrightarrow> rdistinct (rsa @ [a] @ rsb) rset = rdistinct (rsa @ rsb) rset"
+ using distinct_removes_middle(1) by fastforce
+
+lemma distinct_removes_middle_list:
+ shows "\<forall>a \<in> set x. a \<in> set rsa \<Longrightarrow> rdistinct (rsa @ x @ rsb) rset = rdistinct (rsa @ rsb) rset"
+ apply(induct x)
+ apply simp
+ by (simp add: distinct_removes_middle3)
+
+
+lemma distinct_removes_duplicate_flts2:
+ shows " a \<in> set rsa
+ \<Longrightarrow> rdistinct (rflts (rsa @ [a] @ rsb)) {} =
+ rdistinct (rflts (rsa @ rsb)) {}"
+ apply(induct a arbitrary: rsb)
+ using flts_middle01 apply presburger
+ apply(subgoal_tac "rflts (rsa @ [RONE] @ rsb) = rflts rsa @ [RONE] @ rflts rsb")
+ prefer 2
+ using flts_append1 apply blast
+ apply simp
+ apply(subgoal_tac "RONE \<in> set (rflts rsa)")
+ prefer 2
+ using rflts_def_idiot2 apply blast
+ apply(subst distinct_removes_middle3)
+ apply simp
+ using flts_append apply presburger
+ apply simp
+ apply (metis distinct_removes_middle3 flts_append in_set_conv_decomp rflts.simps(5))
+ apply (metis distinct_removes_middle(1) flts_append flts_append1 rflts_def_idiot2 rrexp.distinct(25) rrexp.distinct(5))
+ apply(subgoal_tac "rflts (rsa @ [RALTS x] @ rsb) = rflts rsa @ x @ rflts rsb")
+ prefer 2
+ apply (simp add: flts_append)
+ apply (simp only:)
+
+ apply(subgoal_tac "\<forall>r1 \<in> set x. r1 \<in> set (rflts rsa)")
+ prefer 2
+ using spilled_alts_contained apply blast
+ apply(subst flts_append)
+ using distinct_removes_middle_list apply blast
+ using distinct_removes_middle2 flts_append rflts_def_idiot2 by fastforce
+
+
+lemma simp_removes_duplicate:
+ shows "a \<in> set rsa \<Longrightarrow> rsimp (rsimp_ALTs (rsa @ a # rs)) = rsimp (rsimp_ALTs (rsa @ rs))"
+ apply(subgoal_tac "rsimp (rsimp_ALTs (rsa @ a # rs)) = rsimp (RALTS (rsa @ a # rs))")
+ prefer 2
+ apply (smt (verit, best) Cons_eq_append_conv append_is_Nil_conv empty_set equals0D list.distinct(1) rsimp_ALTs.elims)
+ apply(simp only:)
+ apply simp
+ apply(subgoal_tac "(rdistinct (rflts (map rsimp rsa @ rsimp a # map rsimp rs)) {}) = (rdistinct (rflts (map rsimp rsa @ map rsimp rs)) {})")
+ apply(simp only:)
+ prefer 2
+ apply(subgoal_tac "rsimp a \<in> set (map rsimp rsa)")
+ prefer 2
+ apply simp
+ using distinct_removes_duplicate_flts2 apply force
+ apply(case_tac rsa)
+ apply simp
+ apply(case_tac rs)
+ apply simp
+ apply(case_tac list)
+ apply simp
+ using idem_after_simp1 apply presburger
+ apply simp+
+ apply(subgoal_tac "rsimp_ALTs (aa # list @ aaa # lista) = RALTS (aa # list @ aaa # lista)")
+ apply simp
+ using rsimpalts_conscons by presburger
+
+lemma simp_der_pierce_flts:
+ shows " rsimp (rsimp_ALTs (rdistinct (map (rder x) (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs))) {})) =
+ rsimp (rsimp_ALTs (rdistinct (rflts (map (rder x) (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs))) {}))"
+ oops
+
lemma simp_more_distinct:
- shows "rsimp (rsimp_ALTs (rsa @ rs)) = rsimp (rsimp_ALTs (rsa @ (rdistinct rs (set rsa)))) \<and>
- rsimp (rsimp_ALTs (rsb @ (rdistinct rs (set rsb)))) =
- rsimp (rsimp_ALTs (rsb @ (rdistinct (rflts rs) (set rsb))))"
- apply(induct rs arbitrary: rsa rsb)
+ shows "rsimp (rsimp_ALTs (rsa @ rs)) = rsimp (rsimp_ALTs (rsa @ (rdistinct rs (set rsa)))) "
+and "a1 \<in> set rsb \<Longrightarrow> rsimp (rsimp_ALTs (rsb @ a1 # rs)) = rsimp (rsimp_ALTs (rsb @ rs))"
+ apply(induct rs arbitrary: rsa rsb a1)
+ apply simp
+ apply simp
+ apply(case_tac " a \<in> set rsa")
apply simp
+ prefer 2
+ apply simp
+ apply(drule_tac x = "rsa @ [a]" in meta_spec)
+ apply simp
+
sorry
@@ -316,9 +588,9 @@
done
lemma distinct_removes_last3:
- shows "\<lbrakk>(a::rrexp) \<in> set as\<rbrakk>
+ shows "\<lbrakk>a \<in> set as\<rbrakk>
\<Longrightarrow> rdistinct as {} = rdistinct (as @ [a]) {}"
- using distinct_removes_last2 by blast
+ by (simp add: distinct_removes_last2)
lemma set_inclusion_with_flts1:
shows " \<lbrakk>RONE \<in> set rs\<rbrakk> \<Longrightarrow> RONE \<in> set (rflts rs)"
@@ -367,6 +639,8 @@
\<Longrightarrow> rsimp_ALTs (rdistinct (rflts (map rsimp as @ [rsimp a])) {}) =
rsimp_ALTs (rdistinct (rflts (map rsimp as @ x5)) {})"
+ sorry
+
lemma last_elem_dup1:
shows " a \<in> set as \<Longrightarrow> rsimp (RALTS (as @ [a] )) = rsimp (RALTS (as ))"
@@ -461,6 +735,29 @@
rsimp_ALTs (rdistinct (rflts rs) {})"
by (metis map_idI rsimp.simps(2) rsimp_idem)
+
+lemma add0_isomorphic:
+ shows "rsimp_ALTs (rdistinct (rflts [rsimp r, RZERO]) {}) = rsimp r"
+ sorry
+
+
+lemma distinct_append_simp:
+ shows " rsimp (rsimp_ALTs rs1) = rsimp (rsimp_ALTs rs2) \<Longrightarrow>
+ rsimp (rsimp_ALTs (f a # rs1)) =
+ rsimp (rsimp_ALTs (f a # rs2))"
+ apply(case_tac rs1)
+ apply simp
+ apply(case_tac rs2)
+ apply simp
+ apply simp
+ prefer 2
+ apply(case_tac list)
+ apply(case_tac rs2)
+ apply simp
+ using add0_isomorphic apply blast
+ apply simp
+ sorry
+
lemma alts_closed_form: shows
"rsimp (rders_simp (RALTS rs) s) =
rsimp (RALTS (map (\<lambda>r. rders_simp r s) rs))"
@@ -501,12 +798,11 @@
apply(subst repeated_altssimp)
apply simp
apply fastforce
- apply (metis inside_simp_removal list.map_comp rder.simps(4) rsimp.simps(2) rsimp_idem)
-
-(* apply (metis head_one_more_simp list.inject list.map_comp list.simps(9) rders_simp_lambda rsimp.simps(2))
-*)
+ apply (metis inside_simp_removal list.map_comp rder.simps(4) rsimp.simps(2) rsimp_idem)
+ sledgehammer
+ (* by (metis inside_simp_removal rder_rsimp_ALTs_commute self_append_conv2 set_empty simp_more_distinct)
- sorry
+ *)
lemma alts_closed_form_variant: shows
"s \<noteq> [] \<Longrightarrow> rders_simp (RALTS rs) s =