--- a/thys2/ClosedForms.thy Sun Apr 03 22:12:27 2022 +0100
+++ b/thys2/ClosedForms.thy Mon Apr 04 23:56:40 2022 +0100
@@ -534,13 +534,31 @@
by simp
-lemma grewrites_middle_distinct:
- shows "RALTS rs \<in> set rsb \<Longrightarrow>
- rsb @
- rdistinct ( rs @ rsa)
- (set rsb) \<leadsto>g* rsb @ rdistinct rsa (set rsb)"
+lemma alts_g_can_flts:
+ shows "RALTS rs \<in> set rsb \<Longrightarrow> \<exists>rs1 rs2.( rflts rsb = rs1 @ rs @ rs2)"
+ by (metis flts_append rflts.simps(3) split_list_last)
+
+lemma flts_gstar:
+ shows "rs \<leadsto>g* rflts rs"
+ sorry
+
+lemma create_nonexistent_distinct_set:
+ shows "a \<in> set rs1 \<Longrightarrow> rs1 @ (rdistinct rs (insert a rset)) \<leadsto>g* rs1 @ (rdistinct rs (rset))"
sorry
+lemma grewrites_in_distinct0:
+ shows "a \<in> set rs1 \<Longrightarrow> rs1 @ (rdistinct (a # rs) rset) \<leadsto>g* rs1 @ (rdistinct rs rset)"
+ apply(case_tac "a \<in> rset")
+ apply simp
+ apply simp
+ oops
+
+
+
+
+
+
+
lemma frewrite_rd_grewrites_aux:
@@ -552,9 +570,7 @@
sorry
-lemma flts_gstar:
- shows "rs \<leadsto>g* rflts rs"
- sorry
+
lemma list_dlist_union:
shows "set rs \<subseteq> set rsb \<union> set (rdistinct rs (set rsb))"
@@ -655,35 +671,12 @@
lemma impossible_grewrite2:
shows "\<not> ([RALTS rs] \<leadsto>g (RALTS rs) # a # rs)"
-
using grewrite_singleton by blast
-thm grewrite.cases
-lemma impossible_grewrite3:
- shows "\<not> (RALTS rs # rs1 \<leadsto>g (RALTS rs) # a # rs1)"
- oops
-
-
-lemma grewrites_singleton:
- shows "[r] \<leadsto>g* r # rs \<Longrightarrow> rs = []"
- apply(induct "[r]" "r # rs" rule: grewrites.induct)
- apply simp
-
- oops
-
-lemma grewrite_nonequal_elem:
- shows "r # rs2 \<leadsto>g r # rs3 \<Longrightarrow> rs2 \<leadsto>g rs3"
- oops
-
-lemma grewrites_nonequal_elem:
- shows "r # rs2 \<leadsto>g* r # rs3 \<Longrightarrow> rs2 \<leadsto>g* rs3"
- apply(induct r)
-
- oops
-lemma :
+lemma wront_sublist_grewrites:
shows "rs1 @ rs2 \<leadsto>g* rs1 @ rs3 \<Longrightarrow> rs2 \<leadsto>g* rs3"
apply(induct rs1 arbitrary: rs2 rs3 rule: rev_induct)
apply simp
@@ -695,87 +688,34 @@
-lemma grewrites_shape3_aux:
- shows "rs @ (rdistinct rsa (insert (RALTS rs) rsc)) \<leadsto>g* rs @ rdistinct (rflts (rdistinct rsa rsc)) (set rs)"
- apply(induct rsa arbitrary: rsc rs)
- apply simp
- apply(case_tac "a \<in> rsc")
- apply simp
- apply(case_tac "a = RALTS rs")
- apply simp
- apply(subgoal_tac " rdistinct (rs @ rflts (rdistinct rsa (insert (RALTS rs) rsc))) (set rs) \<leadsto>g*
- rdistinct (rflts (rdistinct rsa (insert (RALTS rs) rsc))) (set rs)")
- apply (metis insertI1 insert_absorb rdistinct_concat2)
- apply (simp add: rdistinct_concat)
- apply simp
- apply(case_tac "a = RZERO")
- apply (metis gmany_steps_later grewrite.intros(1) grewrite_append rflts.simps(2))
- apply(case_tac "\<exists>rs1. a = RALTS rs1")
- prefer 2
+lemma concat_rdistinct_equality1:
+ shows "rdistinct (rs @ rsa) rset = rdistinct rs rset @ rdistinct rsa (rset \<union> (set rs))"
+ apply(induct rs arbitrary: rsa rset)
apply simp
- apply(subgoal_tac "rflts (a # rdistinct rsa (insert a rsc)) = a # rflts (rdistinct rsa (insert a rsc))")
- apply (simp only:)
- apply(case_tac "a \<notin> set rs")
- apply simp
- apply(drule_tac x = "insert a rsc" in meta_spec)
- apply(drule_tac x = "rs " in meta_spec)
-
- apply(erule exE)
- apply simp
- apply(subgoal_tac "RALTS rs1 #
- rdistinct rsa
- (insert (RALTS rs)
- (insert (RALTS rs1)
- rsc)) \<leadsto>g* rs1 @
- rdistinct rsa
- (insert (RALTS rs)
- (insert (RALTS rs1)
- rsc)) ")
- apply(subgoal_tac " rs1 @
- rdistinct rsa
- (insert (RALTS rs)
- (insert (RALTS rs1)
- rsc)) \<leadsto>g*
- rs1 @
- rdistinct rsa
- (insert (RALTS rs)
- (insert (RALTS rs1)
- rsc))")
-
- apply(case_tac "a \<in> set rs")
-
+ apply(case_tac "a \<in> rset")
+ apply simp
+ apply (simp add: insert_absorb)
+ by auto
+lemma ends_removal:
+ shows " rsb @ rdistinct rs (set rsb) @ RALTS rs # rsc \<leadsto>g* rsb @ rdistinct rs (set rsb) @ rsc"
sorry
+lemma grewrites_rev_append:
+ shows "rs1 \<leadsto>g* rs2 \<Longrightarrow> rs1 @ [x] \<leadsto>g* rs2 @ [x]"
+ using grewritess_concat by auto
-lemma grewrites_shape3:
- shows " RALTS rs \<notin> set rsb \<Longrightarrow>
- rsb @
- RALTS rs #
- rdistinct rsa
- (insert (RALTS rs)
- (set rsb)) \<leadsto>g* rsb @
- rdistinct rs (set rsb) @
- rdistinct (rflts (rdistinct rsa (set rsb \<union> set rs))) (set rs)"
- apply(subgoal_tac "rsb @ RALTS rs # rdistinct rsa (insert (RALTS rs) (set rsb)) \<leadsto>g*
- rsb @ rs @ rdistinct rsa (insert (RALTS rs) (set rsb))")
- prefer 2
- using gr_in_rstar grewrite.intros(2) grewrites_append apply presburger
- apply(subgoal_tac "rsb @ rs @ rdistinct rsa (insert (RALTS rs) (set rsb )) \<leadsto>g*
- rsb @ rs @ rdistinct rsa (insert (RALTS rs) (set rsb \<union> set rs))")
- prefer 2
- apply (metis Un_insert_left grewrite_rdistinct_aux grewrites_append)
+lemma grewrites_inclusion:
+ shows "set rs \<subseteq> set rs1 \<Longrightarrow> rs1 @ rs \<leadsto>g* rs1"
+ apply(induct rs arbitrary: rs1)
+ apply simp
+ by (meson gmany_steps_later grewrite_variant1 list.set_intros(1) set_subset_Cons subset_code(1))
- apply(subgoal_tac "rsb @ rs @ rdistinct rsa (insert (RALTS rs) (set rsb \<union> set rs)) \<leadsto>g*
-rsb @ rs @ rdistinct (rflts (rdistinct rsa (set rsb \<union> set rs))) (set rs)")
- prefer 2
- using grewrites_append grewrites_shape3_aux apply presburger
- apply(subgoal_tac "rsb @ rs \<leadsto>g* rsb @ rdistinct rs (set rsb)")
- apply (smt (verit, ccfv_SIG) append_eq_appendI greal_trans grewrites.simps grewritess_concat)
- using gstar_rdistinct_general by blast
-
+lemma distinct_keeps_last:
+ shows "\<lbrakk>x \<notin> rset; x \<notin> set xs \<rbrakk> \<Longrightarrow> rdistinct (xs @ [x]) rset = rdistinct xs rset @ [x]"
+ by (simp add: concat_rdistinct_equality1)
lemma grewrites_shape2:
shows " RALTS rs \<notin> set rsb \<Longrightarrow>
@@ -783,12 +723,76 @@
rdistinct (rs @ rsa)
(set rsb) \<leadsto>g* rsb @
rdistinct rs (set rsb) @
- rdistinct (rflts (rdistinct rsa (set rsb \<union> set rs))) (set rs)"
+ rdistinct rsa (set rs \<union> set rsb \<union> {RALTS rs})"
+ apply(subgoal_tac " rdistinct (rs @ rsa) (set rsb) = rdistinct rs (set rsb) @ rdistinct rsa (set rs \<union> set rsb)")
+ apply (simp only:)
+ prefer 2
+ apply (simp add: Un_commute concat_rdistinct_equality1)
+ apply(induct rsa arbitrary: rs rsb rule: rev_induct)
+ apply simp
+ apply(case_tac "x \<in> set rs")
+ apply (simp add: distinct_removes_middle3)
+ apply(case_tac "x = RALTS rs")
+ apply simp
+ apply(case_tac "x \<in> set rsb")
+ apply simp
+ apply (simp add: concat_rdistinct_equality1)
+ apply (simp add: concat_rdistinct_equality1)
+ apply simp
+ apply(drule_tac x = "rs " in meta_spec)
+ apply(drule_tac x = rsb in meta_spec)
+ apply simp
+ apply(subgoal_tac " rsb @ rdistinct rs (set rsb) @ rdistinct xs (set rs \<union> set rsb) \<leadsto>g* rsb @ rdistinct rs (set rsb) @ rdistinct xs (insert (RALTS rs) (set rs \<union> set rsb))")
+ prefer 2
+ apply (simp add: concat_rdistinct_equality1)
+ apply(case_tac "x \<in> set xs")
+ apply simp
+ apply (simp add: distinct_removes_last2)
+ apply(case_tac "x \<in> set rsb")
+ apply (smt (verit, ccfv_threshold) Un_iff append.right_neutral concat_rdistinct_equality1 insert_is_Un rdistinct.simps(2))
+ apply(subgoal_tac "rsb @ rdistinct rs (set rsb) @ rdistinct (xs @ [x]) (set rs \<union> set rsb) = rsb @ rdistinct rs (set rsb) @ rdistinct xs (set rs \<union> set rsb) @ [x]")
+ apply(simp only:)
+ apply(case_tac "x = RALTS rs")
+ apply(subgoal_tac "rsb @ rdistinct rs (set rsb) @ rdistinct xs (set rs \<union> set rsb) @ [x] \<leadsto>g* rsb @ rdistinct rs (set rsb) @ rdistinct xs (set rs \<union> set rsb) @ rs")
+ apply(subgoal_tac "rsb @ rdistinct rs (set rsb) @ rdistinct xs (set rs \<union> set rsb) @ rs \<leadsto>g* rsb @ rdistinct rs (set rsb) @ rdistinct xs (set rs \<union> set rsb) ")
+ apply (smt (verit, ccfv_SIG) Un_insert_left append.right_neutral concat_rdistinct_equality1 greal_trans insert_iff rdistinct.simps(2))
+ apply(subgoal_tac "set rs \<subseteq> set ( rsb @ rdistinct rs (set rsb) @ rdistinct xs (set rs \<union> set rsb))")
+ apply (metis append.assoc grewrites_inclusion)
+ apply (metis Un_upper1 append.assoc dual_order.trans list_dlist_union set_append)
+ apply (metis append_Nil2 gr_in_rstar grewrite.intros(2) grewrite_append)
+ apply(subgoal_tac " rsb @ rdistinct rs (set rsb) @ rdistinct (xs @ [x]) (insert (RALTS rs) (set rs \<union> set rsb)) = rsb @ rdistinct rs (set rsb) @ rdistinct (xs) (insert (RALTS rs) (set rs \<union> set rsb)) @ [x]")
+ apply(simp only:)
+ apply (metis append.assoc grewrites_rev_append)
+ apply (simp add: insert_absorb)
+ apply (simp add: distinct_keeps_last)+
+ done
- (* by (smt (z3) append.assoc distinct_3list flts_gstar greal_trans grewrites_append rdistinct_concat_general same_append_eq set_append)
-*)
- sorry
+lemma rdistinct_add_acc:
+ shows "rset2 \<subseteq> set rsb \<Longrightarrow> rsb @ rdistinct rs rset \<leadsto>g* rsb @ rdistinct rs (rset \<union> rset2)"
+ apply(induct rs arbitrary: rsb rset rset2)
+ apply simp
+ apply (case_tac "a \<in> rset")
+ apply simp
+ apply(case_tac "a \<in> rset2")
+ apply simp
+ apply (meson create_nonexistent_distinct_set gr_in_rstar greal_trans grewrite_variant1 in_mono)
+ apply simp
+ apply(drule_tac x = "rsb @ [a]" in meta_spec)
+ by (metis Un_insert_left append.assoc append_Cons append_Nil set_append sup.coboundedI1)
+
+lemma frewrite_fun1:
+ shows " RALTS rs \<in> set rsb \<Longrightarrow>
+ rsb @ rdistinct rsa (set rsb) \<leadsto>g* rflts rsb @ rdistinct rsa (set rsb \<union> set rs)"
+ apply(subgoal_tac "rsb @ rdistinct rsa (set rsb) \<leadsto>g* rflts rsb @ rdistinct rsa (set rsb)")
+ apply(subgoal_tac " set rs \<subseteq> set (rflts rsb)")
+ prefer 2
+ using spilled_alts_contained apply blast
+ apply(subgoal_tac "rflts rsb @ rdistinct rsa (set rsb) \<leadsto>g* rflts rsb @ rdistinct rsa (set rsb \<union> set rs)")
+ using greal_trans apply blast
+ using rdistinct_add_acc apply presburger
+ using flts_gstar grewritess_concat by auto
+
@@ -813,24 +817,21 @@
apply simp
apply(case_tac "RALTS rs \<in> set rsb")
apply simp
- apply(rule_tac x = "rflts rsb @ rdistinct rsa (set rsb)" in exI)
+ apply(rule_tac x = "rflts rsb @ rdistinct rsa (set rsb \<union> set rs)" in exI)
apply(rule conjI)
- apply (simp add: flts_gstar grewritess_concat)
- apply (meson flts_gstar greal_trans grewrites.intros(1) grewrites_middle_distinct grewritess_concat)
+ using frewrite_fun1 apply force
+ apply (metis frewrite_fun1 rdistinct_concat sup_ge2)
apply(simp)
apply(rule_tac x =
-"rsb @ (rdistinct rs (set rsb)) @
- (rdistinct (rflts (rdistinct rsa ( (set rsb \<union> set rs)) ) ) (set rs))" in exI)
+ "rsb @
+ rdistinct rs (set rsb) @
+ rdistinct rsa (set rs \<union> set rsb \<union> {RALTS rs})" in exI)
apply(rule conjI)
prefer 2
using grewrites_shape2 apply force
- using grewrites_shape3 by auto
-
+ by (metis Un_insert_left frewrite_rd_grewrites_aux inf_sup_aci(5) insert_is_Un rdistinct.simps(2))
-lemma frewrite_simprd:
- shows "rs1 \<leadsto>f rs2 \<Longrightarrow> rsimp (RALTS rs1) = rsimp (RALTS rs2)"
- by (meson frewrite_simpeq)
lemma frewrites_rd_grewrites:
@@ -838,16 +839,16 @@
rsimp (RALTS rs1) = rsimp (RALTS rs2)"
apply(induct rs1 rs2 rule: frewrites.induct)
apply simp
- using frewrite_simprd by presburger
-
-
-
+ using frewrite_simpeq by presburger
lemma frewrite_simpeq2:
shows "rs1 \<leadsto>f rs2 \<Longrightarrow> rsimp (RALTS (rdistinct rs1 {})) = rsimp (RALTS (rdistinct rs2 {}))"
apply(subgoal_tac "\<exists> rs3. (rdistinct rs1 {} \<leadsto>g* rs3) \<and> (rdistinct rs2 {} \<leadsto>g* rs3)")
using grewrites_equal_rsimp apply fastforce
- using frewrite_rd_grewrites by presburger
+ by (metis append_self_conv2 frewrite_rd_grewrites list.set(1))
+
+
+
(*a more refined notion of \<leadsto>* is needed,
this lemma fails when rs1 contains some RALTS rs where elements
@@ -902,10 +903,7 @@
sorry
*)
-lemma "rsimp (rsimp_ALTs (RZERO # rdistinct (map (rder x) (rflts rs)) {RZERO})) =
- rsimp (rsimp_ALTs (rdistinct (map (rder x) (rflts rs)) {})) "
- sorry