
diff -r 51af5f882350 -r b2a8610cf110 thys2/ClosedForms.thy
--- 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
 
 
 




