
diff -r e6248d2c20c2 -r 2e7c7111c0be thys2/ClosedForms.thy
--- 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 = 




