# HG changeset patch
# User Chengsong
# Date 1649493169 -3600
# Node ID 064f4920198c97947ed2686fed09b9562c8bc1be
# Parent  4bf2367e6e530b491a6469c72c81be0364b19c62
some

diff -r 4bf2367e6e53 -r 064f4920198c thys2/ClosedForms.thy
--- a/thys2/ClosedForms.thy	Fri Apr 08 21:45:32 2022 +0100
+++ b/thys2/ClosedForms.thy	Sat Apr 09 09:32:49 2022 +0100
@@ -1554,11 +1554,20 @@
 
   oops
 
+inductive softrewrite :: "rrexp \<Rightarrow> rrexp list \<Rightarrow> bool" ("_ \<leadsto>o _" [100, 100] 100) where
+  "RALTS rs  \<leadsto>o rs"
+| "r1 \<leadsto>o rs1 \<Longrightarrow> (RALT r1 r2) \<leadsto>o (rs1 @ [r2])"
+
+
 fun sflat :: "rrexp  \<Rightarrow> rrexp list " where
   "sflat (RALT r1 r2) = sflat r1 @ [r2]"
 | "sflat (RALTS rs) = rs"
 | "sflat r = [r]"
 
+lemma softrewrite_flat:
+  shows "r \<leadsto>o sflat r"
+  
+
 lemma seq_sflat0:
   shows "sflat (rders (RSEQ r1 r2) s) = sflat (RALTS ( (RSEQ (rders r1 s) r2) #
                                        (map (rders r2) (vsuf s r1))) )"
@@ -1580,10 +1589,62 @@
               ))  )"
   sorry
 
+lemma sflat_elemnum:
+  shows "sflat (RALTS [a1, a2, a3]) = [a1, a2, a3]"
+  sorry
+
+lemma sflat_emptyalts:
+  shows  "sflat (RALTS xs) = [] \<Longrightarrow> xs = []"
+  using sflat.elims by auto
+
+lemma ralt_sflat_gte2:
+  shows "\<exists>ra rb rsc. sflat (RALT r1 r2) = ra # rb # rsc"
+  apply(case_tac r1)
+       apply simp+
+  
+  oops
+
+lemma sflat_singleton:
+  shows "sflat (RALTS xs) = [a] \<Longrightarrow> xs = [a]"
+  apply(case_tac xs)
+   apply simp
+  apply(case_tac list)
+   apply simp
+  apply simp
+  oops
+
+thm sflat.elims
+
+
+lemma sflat_ralts: 
+  shows "sflat (RALTS xs) = sflat (RALTS xs') 
+     \<Longrightarrow> rsimp (RALTS xs) = rsimp (RALTS xs')"
+  apply(induct xs)
+
+  apply(case_tac xs)
+   apply simp
+   apply (metis list.simps(8) rdistinct.simps(1) rflts.simps(1) rsimp_ALTs.simps(1) sflat_emptyalts)
+  apply(case_tac list)
+   apply simp
+  apply 
+  sledgehammer
+  
+
 
 
 lemma sflat_rsimpeq:
   shows "sflat r1 = sflat r2 \<Longrightarrow> rsimp r1 = rsimp r2"
+  apply(cases r1 )
+       apply(cases r2)
+            apply simp+
+        apply(case_tac x5)
+  apply simp
+        apply(case_tac list)
+         apply simp
+        apply(case_tac lista)
+         apply simp
+
+
   sorry