--- a/ChengsongPhdThesis/ChengsongPhDThesis.tex	Sat Mar 19 09:53:48 2022 +0000
+++ b/ChengsongPhdThesis/ChengsongPhDThesis.tex	Sat Mar 19 10:36:52 2022 +0000
@@ -1,13 +1,13 @@
 \documentclass[a4paper,UKenglish]{lipics}
 \usepackage{graphic}
 \usepackage{data}
-\usepackage{tikz-cd}
+
 %\usepackage{algorithm}
 \usepackage{amsmath}
 \usepackage[noend]{algpseudocode}
 \usepackage{enumitem}
 \usepackage{nccmath}
-
+\usepackage{tikz-cd}
 \usetikzlibrary{positioning}
 
 \definecolor{darkblue}{rgb}{0,0,0.6}

--- a/thys2/ClosedForms.thy	Sat Mar 19 09:53:48 2022 +0000
+++ b/thys2/ClosedForms.thy	Sat Mar 19 10:36:52 2022 +0000
@@ -2,6 +2,32 @@
 "BasicIdentities"
 begin
 
+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
+
+(*  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)))*)
+
+
+
 
 
 lemma simp_rdistinct_f: shows 
@@ -18,16 +44,365 @@
   prefer 2
   apply (meson image_insert)
   
+  oops
 
+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)
+
+lemma spawn_simp_distinct:
+  shows "rsimp (rsimp_ALTs (rsa @ (rdistinct rs (set rsa)))) = rsimp (rsimp_ALTs (rsa @ rs))
+\<and> (a1 \<in> set rsa1 \<longrightarrow> rsimp (rsimp_ALTs (rsa1 @ rs)) = rsimp (rsimp_ALTs (rsa1 @ a1 # rs)))
+\<and> rsimp  (rsimp_ALTs (rsc @ rs)) = rsimp (rsimp_ALTs (rsc @ (rdistinct rs (set rsc))))"
+  apply(induct rs arbitrary: rsa rsa1 a1 rsc)
+   apply simp
+   apply(subgoal_tac "rsimp (rsimp_ALTs (rsa1 @ [a1])) = rsimp (rsimp_ALTs (rsa1 @ (rdistinct [a1] (set rsa1))))")
+  prefer 2
+  
+
+
+
+  oops
+
+lemma inv_one_derx:
+  shows " RONE = rder xa r2 \<Longrightarrow> r2 = RCHAR xa"
+  apply(case_tac r2)
+       apply simp+
+  
+  using rrexp.distinct(1) apply presburger
+    apply (metis rder.simps(5) rrexp.distinct(13) rrexp.simps(20))
+  
+   apply simp+
+  done
+
+lemma shape_of_derseq:
+  shows "rder x (RSEQ r1 r2) = RSEQ (rder x r1) r2 \<or> rder x (RSEQ r1 r2) = (RALT (RSEQ (rder x r1) r2) (rder x r2))"
+  using rder.simps(5) by presburger
+lemma shape_of_derseq2:
+  shows "rder x (RSEQ r11 r12) = RSEQ x41 x42 \<Longrightarrow> x41 = rder x r11"
+  by (metis rrexp.distinct(25) rrexp.inject(2) shape_of_derseq)
+
+lemma alts_preimage_case1:
+  shows "rder x r = RALTS [r] \<Longrightarrow> \<exists>ra. r = RALTS [ra]"
+  apply(case_tac r)
+       apply simp+
+  apply (metis rrexp.simps(12) rrexp.simps(20))
+  apply (metis rrexp.inject(3) rrexp.simps(30) rsimp_ALTs.simps(2) rsimp_ALTs.simps(3) shape_of_derseq)
+   apply auto[1]
+  by auto
+
+lemma alts_preimage_case2:
+  shows "rder x r = RALT r1 r2 \<Longrightarrow> \<exists>ra rb. (r = RSEQ ra rb \<or> r = RALT ra rb)"
+  apply(case_tac r)
+       apply simp+
+  apply (metis rrexp.distinct(15) rrexp.distinct(7))
+    apply simp
+  apply auto[1]
+  by auto
+
+lemma alts_preimage_case2_2:
+  shows "rder x r = RALT r1 r2 \<Longrightarrow> (\<exists>ra rb. r = RSEQ ra rb) \<or> (\<exists>rc rd. r = RALT rc rd)"
+  using alts_preimage_case2 by blast
+
+lemma alts_preimage_case3:
+  shows "rder x r = RALT r1 r2 \<Longrightarrow>  (\<exists>ra rb. r = RSEQ ra rb) \<or> (\<exists>rcs rc rd. r = RALTS rcs \<and> rcs = [rc, rd])"
+  using alts_preimage_case2 by blast
+
+lemma star_seq:
+  shows "rder x (RSEQ (RSTAR a) b) = RALT (RSEQ (RSEQ (rder x a) (RSTAR a)) b) (rder x b)"
+  using rder.simps(5) rder.simps(6) rnullable.simps(6) by presburger
+
+lemma language_equality_id1:
+  shows "\<not>rnullable a \<Longrightarrow> rder x (RSEQ (RSTAR a) b) = rder x (RALT (RSEQ (RSEQ a (RSTAR a)) b) b)"
+  apply (subst star_seq)
+  apply simp
+  done
+
+  
+
+
+lemma alts_preimage_cases:
+  shows "rder x r = RALT (RSEQ r1 r2) r3 \<Longrightarrow> (\<exists>ra rb. r = RSEQ ra rb) \<or> (\<exists>rc rd re. r = RALT (RSEQ rc rd) re)"
+  apply(case_tac r)
+       apply simp+
+  
+  apply (metis rrexp.simps(12) rrexp.simps(20))
+    prefer 3
+  apply simp
+  apply blast
+  apply(frule alts_preimage_case2_2)
+  apply(case_tac "(\<exists>ra rb. r = RSEQ ra rb)")
+   apply blast
+  apply(subgoal_tac " (\<exists> rc rd. r = RALT rc rd )")
+  prefer 2
+   apply blast
+  apply(erule exE)+
+  apply(subgoal_tac "rder x r = RALT (rder x rc) (rder x rd)")
+  prefer 2
+  apply force
+  apply(subgoal_tac "rder x rc = RSEQ r1 r2")
+  oops
+
+
+lemma der_seq_eq_case:
+  shows "\<lbrakk>r1 \<noteq> r2 ; r1 = RSEQ ra rb; rder x r1 = rder x r2\<rbrakk> \<Longrightarrow> rsimp (rder x r1) =  RZERO \<and> rsimp (rder x r2) = RZERO"
+  apply(case_tac "rnullable ra")
+  apply simp
+  oops
+
+  
+  
+
+lemma der_map_unequal_to_equal_zero_only:
+  shows "\<lbrakk>r1 \<noteq> r2 ; rder x r1 = rder x r2 \<rbrakk> \<Longrightarrow> rsimp (rder x r1) = RZERO"
+  apply(induct r1)
+       apply simp
+      apply simp
+     apply simp
+     apply(case_tac "x = xa")
+      apply simp
+      apply(subgoal_tac "r2 = RCHAR xa")
+  prefer 2
+  using inv_one_derx apply blast
+      apply simp
+  using rsimp.simps(3) apply presburger
+    apply(case_tac "rder x (RSEQ r11 r12)")
+         apply simp
+        apply (metis inv_one_derx)
+       apply (metis rrexp.distinct(21) rrexp.simps(24) shape_of_derseq)
+      apply(subgoal_tac "rder x r2 = RSEQ x41 x42")
+  prefer 2
+       apply presburger
+      apply(subgoal_tac "x41 = rder x r11")
+       prefer 2
+       apply (meson shape_of_derseq2)
+      apply(case_tac r2)
+           apply simp+
+  apply (metis rrexp.distinct(13) rrexp.simps(10))
+        apply(subgoal_tac "x42a = x42")
+  prefer 2
+  apply (metis rrexp.inject(2) rrexp.simps(30) shape_of_derseq)
+  apply(subgoal_tac "rder x x41a =  x41")
+        prefer 2 
+  apply (metis shape_of_derseq2)
+        apply(simp)
+        apply(subgoal_tac "\<not> rnullable r11")
+  prefer 2
+  apply force
+        apply simp
+        apply(subgoal_tac "\<not> rnullable x41a")
+  prefer 2
+         apply force
+        apply simp
+  
+  oops
+
+
+
+lemma der_maps_1to1_except0:
+  shows "\<lbrakk>rder x ` rset = dset; a \<notin> rset; rder x a \<in> dset\<rbrakk> \<Longrightarrow> rsimp (rder x a) = RZERO"
+  
+
+  sorry
+
+lemma distinct_der_set:
+  shows "(rder x) ` rset = dset \<Longrightarrow>
+rsimp (rsimp_ALTs (map (rder x) (rdistinct rs rset))) = rsimp ( rsimp_ALTs (rdistinct (map (rder x) rs) dset))"
+  apply(induct rs arbitrary: rset dset)
+   apply simp
+  apply(case_tac "a \<in> rset")
+   apply(subgoal_tac "rder x a \<in> dset")
+  prefer 2
+    apply blast
+   apply simp
+  apply(case_tac "rder x a \<notin> dset")
+   prefer 2
+   apply simp
+ 
+  oops
+
+lemma map_concat_cons:
+  shows "map f rsa @ f a # rs = map f (rsa @ [a]) @ rs"
+  by simp
+
+lemma neg_removal_element_of:
+  shows " \<not> a \<notin> aset \<Longrightarrow> a \<in> aset"
+  by simp
+
+lemma simp_more_flts:
+  shows "rsimp (rsimp_ALTs (rdistinct rs {})) = rsimp (rsimp_ALTs (rdistinct (rflts 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)
+   apply simp
+
+  sorry
+
+lemma non_empty_list:
+  shows "a \<in> set as \<Longrightarrow> as \<noteq> []"
+  
+  by (metis empty_iff empty_set)
+
+
+lemma distinct_removes_last:
+  shows "\<lbrakk>a \<in> set as; rsimp a \<in> set (map rsimp as)\<rbrakk>
+    \<Longrightarrow> rsimp_ALTs (rdistinct (rflts (map rsimp as @ [rsimp a])) {}) =
+        rsimp_ALTs (rdistinct (rflts (map rsimp as)) {})"
+  apply(induct "rsimp a" arbitrary: as)
+       apply(simp)
+       apply (metis append.right_neutral append_self_conv2 empty_set list.simps(9) map_append rflts.simps(2) rsimp.simps(2) rsimp_idem simp_more_distinct spawn_simp_rsimpalts)
+  apply simp
+  sorry
+
+lemma flts_identity1:
+  shows  "rflts (rs @ [RONE]) = rflts rs @ [RONE] "
+  apply(induct rs)
+   apply simp+
+  apply(case_tac a)
+       apply simp
+      apply simp+
+  done
+
+lemma flts_identity10:
+  shows " rflts (rs @ [RCHAR c]) = rflts rs @ [RCHAR c]"
+  apply(induct rs)
+   apply simp+
+  apply(case_tac a)
+       apply simp+
+  done
+
+lemma flts_identity11:
+  shows " rflts (rs @ [RSEQ r1 r2]) = rflts rs @ [RSEQ r1 r2]"
+  apply(induct rs)
+   apply simp+
+  apply(case_tac a)
+       apply simp+
+  done
+
+lemma flts_identity12:
+  shows " rflts (rs @ [RSTAR r0]) = rflts rs @ [RSTAR r0]"
+  apply(induct rs)
+   apply simp+
+  apply(case_tac a)
+       apply simp+
+  done
+
+lemma flts_identity2:
+  shows "a \<noteq> RZERO \<and> (\<forall>rs. a \<noteq> RALTS rs) \<Longrightarrow>  rflts (rs @ [a]) = rflts rs @ [a]"
+  apply(case_tac a)
+       apply simp
+  using flts_identity1 apply auto[1]
+  using flts_identity10 apply blast
+  using flts_identity11 apply auto[1]
+   apply blast
+  using flts_identity12 by presburger
+  
+
+lemma last_elem_dup1:
+  shows " a \<in> set as \<Longrightarrow> rsimp (RALTS (as @ [a] )) = rsimp (RALTS (as ))"
+  apply simp
+  apply(subgoal_tac "rsimp a \<in> set (map rsimp as)")
+  prefer 2
+   apply simp
+
+  sorry
+
+lemma last_elem_dup:
+  shows " a \<in> set as \<Longrightarrow> rsimp (rsimp_ALTs (as @ [a] )) = rsimp (rsimp_ALTs (as ))"
+  apply(induct as rule: rev_induct)
+   apply simp
+  apply simp
+  apply(subgoal_tac "xs \<noteq> []")
+  prefer 2
+  
+
+  
+
+  sorry
+
+lemma appeared_before_remove_later:
+  shows "a \<in>  set as \<Longrightarrow> rsimp (rsimp_ALTs ( as @ a # rs)) = rsimp (rsimp_ALTs (as @ rs))"
+and "a \<in> set as \<Longrightarrow> rsimp (rsimp_ALTs as ) = rsimp (rsimp_ALTs (as @ [a]))"
+  apply(induct rs arbitrary: as)
+   apply simp
+  
+
+  sorry
+
+lemma distinct_remove_later:
+  shows "\<lbrakk>rder x a \<in> rder x ` set rsa\<rbrakk>
+       \<Longrightarrow> rsimp (rsimp_ALTs (map (rder x) rsa @ rder x a # map (rder x) (rdistinct rs (insert a (set rsa))))) =
+           rsimp (rsimp_ALTs (map (rder x) rsa @ map (rder x) (rdistinct rs (set rsa))))"
   
   sorry
 
 
+lemma distinct_der_general:
+  shows "rsimp (rsimp_ALTs (map (rder x) (rsa @ (rdistinct rs (set rsa))))) =
+ rsimp ( rsimp_ALTs ((map (rder x) rsa)@(rdistinct (map (rder x) rs) (set (map (rder x) rsa)))) )"
+  apply(induct rs arbitrary: rsa)
+   apply simp
+  apply(case_tac "a \<in> set rsa")
+   apply(subgoal_tac "rder x a \<in> set (map (rder x) rsa)")
+  apply simp
+   apply simp
+  apply(case_tac "rder x a \<notin> set (map (rder x) rsa)")
+   apply(simp)
+  apply(subst map_concat_cons)+
+  apply(drule_tac x = "rsa @ [a]" in meta_spec)
+   apply simp
+  apply(drule neg_removal_element_of)
+  apply simp
+  apply(subst distinct_remove_later)
+   apply simp
+  apply(drule_tac x = "rsa" in meta_spec)
+  by blast
+
+  
+
+
 lemma distinct_der:
   shows "rsimp (rsimp_ALTs (map (rder x) (rdistinct rs {}))) = rsimp ( rsimp_ALTs (rdistinct (map (rder x) rs) {}))"
+  by (metis distinct_der_general list.simps(8) self_append_conv2 set_empty)
 
-  sorry
+  
+
+
+lemma rders_simp_lambda:
+  shows " rsimp \<circ> rder x \<circ> (\<lambda>r. rders_simp r xs) = (\<lambda>r. rders_simp r (xs @ [x]))"
+  using rders_simp_append by auto
 
+lemma rders_simp_nonempty_simped:
+  shows "xs \<noteq> [] \<Longrightarrow> rsimp \<circ> (\<lambda>r. rders_simp r xs) = (\<lambda>r. rders_simp r xs)"
+  using rders_simp_same_simpders rsimp_idem by auto
+
+lemma repeated_altssimp:
+  shows "\<forall>r \<in> set rs. rsimp r = r \<Longrightarrow> rsimp (rsimp_ALTs (rdistinct (rflts rs) {})) =
+           rsimp_ALTs (rdistinct (rflts rs) {})"
+  by (metis map_idI rsimp.simps(2) rsimp_idem)
 
 lemma alts_closed_form: shows 
 "rsimp (rders_simp (RALTS rs) s) = 
@@ -54,6 +429,25 @@
   
   using distinct_der apply presburger
   apply(simp only:)
+  apply(subgoal_tac " 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)))) {}))")
+   apply(simp only:)
+  apply(subgoal_tac " rsimp (rsimp_ALTs (rdistinct (rflts (map (rder x) (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs))) {})) = 
+                      rsimp (rsimp_ALTs (rdistinct (rflts ( (map (rsimp \<circ> (rder x) \<circ> (\<lambda>r. rders_simp r xs)) rs))) {}))")
+    apply(simp only:)
+  apply(subst rders_simp_lambda)
+    apply(subst rders_simp_nonempty_simped)
+     apply simp
+    apply(subgoal_tac "\<forall>r \<in> set  (map (\<lambda>r. rders_simp r (xs @ [x])) rs). rsimp r = r")
+  prefer 2
+     apply (simp add: rders_simp_same_simpders rsimp_idem)
+    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))
+*)
 
   sorry