diff -r d68b9db4c9ec -r 26a5e640cdd7 thys2/ClosedForms.thy
--- a/thys2/ClosedForms.thy	Sat Mar 19 10:36:52 2022 +0000
+++ b/thys2/ClosedForms.thy	Sun Mar 20 23:32:08 2022 +0000
@@ -7,6 +7,52 @@
   sorry
 
 
+
+
+lemma distinct_removes_last:
+  shows "\<lbrakk>(a::rrexp) \<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)
+     apply simp
+    apply simp
+  apply(case_tac "aa \<in> rset")
+   apply(case_tac "a = aa")
+  apply (metis append_Cons)
+    apply simp
+   apply(case_tac "a \<in> set as")
+  apply (metis append_Cons rdistinct.simps(2) set_ConsD)
+   apply(case_tac "a = aa")
+    prefer 2
+    apply simp
+   apply (metis append_Cons)
+  apply(case_tac "ab \<in> rset1")
+  prefer 2
+   apply(subgoal_tac "rdistinct (ab # (a # as) @ [ab]) rset1 = 
+               ab # (rdistinct ((a # as) @ [ab]) (insert ab rset1))")
+  prefer 2
+  apply force
+  apply(simp only:)
+     apply(subgoal_tac "rdistinct (ab # a # as) rset1 = ab # (rdistinct (a # as) (insert ab rset1))")
+    apply(simp only:)
+    apply(subgoal_tac "rdistinct ((a # as) @ [ab]) (insert ab rset1) = rdistinct (a # as) (insert ab rset1)")
+     apply blast
+    apply(case_tac "a \<in> insert ab rset1")
+     apply simp
+     apply (metis insertI1)
+    apply simp
+    apply (meson insertI1)
+   apply simp
+  apply(subgoal_tac "rdistinct ((a # as) @ [ab]) rset1 = rdistinct (a # as) rset1")
+   apply simp
+  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)) =
@@ -84,10 +130,8 @@
   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
 
@@ -134,93 +178,8 @@
   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))"
@@ -263,19 +222,46 @@
 
 lemma non_empty_list:
   shows "a \<in> set as \<Longrightarrow> as \<noteq> []"
-  
   by (metis empty_iff empty_set)
 
+lemma distinct_comp:
+  shows "rdistinct (rs1@rs2) {} = (rdistinct rs1 {}) @ (rdistinct rs2 (set rs1))"
+  apply(induct rs2 arbitrary: rs1)
+   apply simp
+  apply(subgoal_tac "rs1 @ a # rs2 = (rs1 @ [a]) @ rs2")
+   apply(simp only:)
+   apply(case_tac "a \<in> set rs1")
+    apply simp
+  oops
 
-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)
+lemma instantiate1:
+  shows "\<lbrakk>\<And>ab rset1.  rdistinct (ab # as) rset1 = rdistinct (ab # as @ [ab]) rset1\<rbrakk> \<Longrightarrow>  
+rdistinct (aa # as) rset = rdistinct (aa # as @ [aa]) rset"
+  apply(drule_tac x = "aa" in meta_spec)
+  apply(drule_tac x = "rset" in meta_spec)
   apply simp
-  sorry
+  done
+  
+
+lemma not_head_elem:
+  shows " \<lbrakk>aa \<in> set (a # as); aa \<notin> (set as)\<rbrakk> \<Longrightarrow> a = aa"
+  
+  by fastforce
+
+(*
+  apply simp
+  apply (metis append_Cons)
+  apply(case_tac "ab \<in> rset1")
+  apply (metis (no_types, opaque_lifting) Un_insert_left append_Cons insert_iff rdistinct.simps(2) sup_bot_left)
+  apply(subgoal_tac "rdistinct (ab # (aa # as) @ [ab]) rset1 = 
+               ab # (rdistinct ((aa # as) @ [ab]) (insert ab rset1))")
+   apply(simp only:)
+   apply(subgoal_tac "rdistinct (ab # aa # as) rset1 = ab # (rdistinct (aa # as) (insert ab rset1))")
+  apply(simp only:)
+    apply(subgoal_tac "rdistinct ((aa # as) @ [ab]) (insert ab rset1) = rdistinct (aa # as) (insert ab rset1)")
+  apply blast
+*)
+  
 
 lemma flts_identity1:
   shows  "rflts (rs @ [RONE]) = rflts rs @ [RONE] "
@@ -319,7 +305,68 @@
   using flts_identity11 apply auto[1]
    apply blast
   using flts_identity12 by presburger
+
+lemma flts_identity3:
+  shows "a = RZERO  \<Longrightarrow> rflts (rs @ [a]) = rflts rs"
+  apply simp
+  apply(induct rs)
+   apply simp+
+  apply(case_tac aa)
+       apply simp+
+  done
+
+lemma distinct_removes_last3:
+  shows "\<lbrakk>(a::rrexp) \<in> set as\<rbrakk>
+    \<Longrightarrow> rdistinct as {} = rdistinct (as @ [a]) {}"
+  using distinct_removes_last2 by blast
+
+lemma set_inclusion_with_flts1:
+  shows " \<lbrakk>RONE \<in> set rs\<rbrakk> \<Longrightarrow> RONE  \<in> set (rflts rs)"
+  apply(induct rs)
+   apply simp
+  apply(case_tac " RONE \<in> set rs")
+   apply simp
+  apply (metis Un_upper2 insert_absorb insert_subset list.set_intros(2) rflts.simps(2) rflts.simps(3) rflts_def_idiot set_append)
+  apply(case_tac "RONE = a")
+   apply simp
+  apply simp
+  done
+
+lemma set_inclusion_with_flts10:
+  shows " \<lbrakk>RCHAR x \<in> set rs\<rbrakk> \<Longrightarrow> RCHAR x  \<in> set (rflts rs)"
+  apply(induct rs)
+   apply simp
+  apply(case_tac " RCHAR x \<in> set rs")
+   apply simp
+  apply (metis Un_upper2 insert_absorb insert_subset rflts.simps(2) rflts.simps(3) rflts_def_idiot set_append set_subset_Cons)
+  apply(case_tac "RCHAR x = a")
+   apply simp
+  apply fastforce
+  apply simp
+  done
+
+lemma set_inclusion_with_flts11:
+  shows " \<lbrakk>RSEQ r1 r2 \<in> set rs\<rbrakk> \<Longrightarrow> RSEQ r1 r2  \<in> set (rflts rs)"
+  apply(induct rs)
+   apply simp
+  apply(case_tac " RSEQ r1 r2 \<in> set rs")
+   apply simp
+  apply (metis Un_upper2 insert_absorb insert_subset rflts.simps(2) rflts.simps(3) rflts_def_idiot set_append set_subset_Cons)
+  apply(case_tac "RSEQ r1 r2 = a")
+   apply simp
+  apply fastforce
+  apply simp
+  done
+
+
+lemma set_inclusion_with_flts:
+  shows " \<lbrakk>a \<in> set as; rsimp a \<in> set (map rsimp as); rsimp a = RONE\<rbrakk> \<Longrightarrow> rsimp a \<in> set (rflts (map rsimp as))"
+  by (simp add: set_inclusion_with_flts1)
   
+lemma "\<And>x5. \<lbrakk>a \<in> set as; rsimp a \<in> set (map rsimp as); rsimp a = RALTS x5\<rbrakk>
+          \<Longrightarrow> rsimp_ALTs (rdistinct (rflts (map rsimp as @ [rsimp a])) {}) = 
+rsimp_ALTs (rdistinct (rflts (map rsimp as @ x5)) {})"
+
 
 lemma last_elem_dup1:
   shows " a \<in> set as \<Longrightarrow> rsimp (RALTS (as @ [a] )) = rsimp (RALTS (as ))"
@@ -327,7 +374,17 @@
   apply(subgoal_tac "rsimp a \<in> set (map rsimp as)")
   prefer 2
    apply simp
-
+  apply(case_tac "rsimp a")
+       apply simp
+  
+  using flts_identity3 apply presburger
+      apply(subst flts_identity2)
+  using rrexp.distinct(1) rrexp.distinct(15) apply presburger
+      apply(subst distinct_removes_last3[symmetric])
+  using set_inclusion_with_flts apply blast
+  apply simp
+  apply (metis distinct_removes_last3 flts_identity10 set_inclusion_with_flts10)
+  apply (metis distinct_removes_last3 flts_identity11 set_inclusion_with_flts11)
   sorry
 
 lemma last_elem_dup: