# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1557866591 -3600
# Node ID 22e34f93cd5d08c0e37909c55f68fb10be6a2033
# Parent  72f54acfb976c29a4dbb4a3da3498e5b5d38ad6e
updaed good

diff -r 72f54acfb976 -r 22e34f93cd5d exps/bit-test.scala
--- a/exps/bit-test.scala	Fri May 10 17:23:28 2019 +0100
+++ b/exps/bit-test.scala	Tue May 14 21:43:11 2019 +0100
@@ -419,7 +419,7 @@
   (result, (end - start))
 }
 
-//size: of a Aregx for testing purposes 
+//size: of a Rrexp and ARexp for testing purposes 
 def size(r: Rexp) : Int = r match {
   case ZERO => 1
   case ONE => 1
@@ -690,6 +690,30 @@
 enum(2, "abc").map(tests_ders_bsimp(strs(1, "abc"))).
   flatten.toSet.flatten.minBy(a => asize(a._1))
 
+// tests about good
+def good (a: ARexp) : Boolean = a match {
+  case AZERO => false
+  case AONE(_) => true
+  case APRED(_, _, _) => true
+  case AALTS(_, Nil) => false
+  case AALTS(_, rs) => rs.forall(good(_))
+  case ASEQ(_, r1, r2) => good(r1) & good(r2)
+  case ASTAR(_, _) => true
+}
+
+def tests_good(r: Rexp) = {
+  val a = bsimp(internalise(r))
+  if  (! good(a) & a != AZERO) {
+        println(s"Counter-example on ${astring(a)}")
+        Some(a)  
+  } else None 
+}
+
+enum(2, "abc").map(tests_good).toSet
+
+val g1 = AALTS(Nil, Nil)
+good(g1)
+good(bsimp(g1))
 
 
 //tests retrieve and lexing
diff -r 72f54acfb976 -r 22e34f93cd5d thys/BitCoded.thy
--- a/thys/BitCoded.thy	Fri May 10 17:23:28 2019 +0100
+++ b/thys/BitCoded.thy	Tue May 14 21:43:11 2019 +0100
@@ -106,6 +106,34 @@
 | "asize (ASEQ cs r1 r2) = Suc (asize r1 + asize r2)"
 | "asize (ASTAR cs r) = Suc (asize r)"
 
+fun 
+  erase :: "arexp \<Rightarrow> rexp"
+where
+  "erase AZERO = ZERO"
+| "erase (AONE _) = ONE"
+| "erase (ACHAR _ c) = CHAR c"
+| "erase (AALTs _ []) = ZERO"
+| "erase (AALTs _ [r]) = (erase r)"
+| "erase (AALTs bs (r#rs)) = ALT (erase r) (erase (AALTs bs rs))"
+| "erase (ASEQ _ r1 r2) = SEQ (erase r1) (erase r2)"
+| "erase (ASTAR _ r) = STAR (erase r)"
+
+fun nonalt :: "arexp \<Rightarrow> bool"
+  where
+  "nonalt (AALTs bs2 rs) = False"
+| "nonalt r = True"
+
+
+fun good :: "arexp \<Rightarrow> bool" where
+  "good AZERO = False"
+| "good (AONE cs) = True" 
+| "good (ACHAR cs c) = True"
+| "good (AALTs cs []) = False"
+| "good (AALTs cs (r#rs)) = (\<forall>r' \<in> set (r#rs). good r')"
+| "good (ASEQ cs r1 r2) = (good r1 \<and> good r2)"
+| "good (ASTAR cs r) = True"
+
+
 
 
 fun fuse :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp" where
@@ -144,17 +172,7 @@
 | "retrieve (ASTAR bs r) (Stars (v#vs)) = 
      bs @ [Z] @ retrieve r v @ retrieve (ASTAR [] r) (Stars vs)"
 
-fun 
-  erase :: "arexp \<Rightarrow> rexp"
-where
-  "erase AZERO = ZERO"
-| "erase (AONE _) = ONE"
-| "erase (ACHAR _ c) = CHAR c"
-| "erase (AALTs _ []) = ZERO"
-| "erase (AALTs _ [r]) = (erase r)"
-| "erase (AALTs bs (r#rs)) = ALT (erase r) (erase (AALTs bs rs))"
-| "erase (ASEQ _ r1 r2) = SEQ (erase r1) (erase r2)"
-| "erase (ASTAR _ r) = STAR (erase r)"
+
 
 fun
  bnullable :: "arexp \<Rightarrow> bool"
@@ -559,6 +577,10 @@
 | "bsimp (AALTs bs1 rs) = bsimp_AALTs bs1 (flts (map bsimp rs))"
 | "bsimp r = r"
 
+value "good (AALTs [] [AALTs [] [AONE []]])"
+value "bsimp (AALTs [] [AONE [], AALTs [] [AONE []]])"
+
+
 fun 
   bders_simp :: "arexp \<Rightarrow> string \<Rightarrow> arexp"
 where
@@ -570,9 +592,6 @@
                 decode (bmkeps (bders_simp (intern r) s)) r else None"
 
 
-
-
-
 lemma asize0:
   shows "0 < asize r"
   apply(induct  r)
@@ -611,7 +630,8 @@
   apply(induct rs rule: bsimp_AALTs.induct)
   apply(auto simp add: fuse_size)
   done
-  
+
+
 lemma bsimp_size:
   shows "asize (bsimp r) \<le> asize r"
   apply(induct r)
@@ -624,10 +644,13 @@
    apply(rule flts_size)
   by (simp add: sum_list_mono)
 
-fun nonalt :: "arexp \<Rightarrow> bool"
-  where
-  "nonalt (AALTs bs2 rs) = False"
-| "nonalt r = True"
+lemma bsimp_asize0:
+  shows "(\<Sum>x\<leftarrow>rs. asize (bsimp x)) \<le> sum_list (map asize rs)"
+  apply(induct rs)
+   apply(auto)
+  by (simp add: add_mono bsimp_size)
+  
+
 
 
 
@@ -1057,8 +1080,241 @@
    apply(simp_all)
   done
 
+lemma good_fuse:
+  shows "good (fuse bs r) = good r"
+  apply(induct r)
+       apply(auto)
+  apply (metis arexp.distinct(25) arexp.distinct(7) arexp.inject(4) good.elims(3) good.simps(4) good.simps(5))
+  by (metis good.simps(4) good.simps(5) neq_Nil_conv)
+
+lemma good0:
+  assumes "rs \<noteq> Nil"
+  shows "good (bsimp_AALTs bs rs) \<longleftrightarrow> (\<forall>r \<in> set rs. good r)"
+  using  assms
+  apply(induct bs rs rule: bsimp_AALTs.induct)
+  apply(auto simp add: good_fuse)
+  done
+
+lemma good0a:
+  assumes "flts (map bsimp rs) \<noteq> Nil"
+  shows "good (bsimp (AALTs bs rs)) \<longleftrightarrow> (\<forall>r \<in> set (flts (map bsimp rs)). good r)"
+  using  assms
+  apply(simp)
+  apply(rule good0)
+  apply(simp)
+  done
+
+lemma flts0:
+  assumes "r \<noteq> AZERO" "nonalt r"
+  shows "flts [r] \<noteq> []"
+  using  assms
+  apply(induct r)
+       apply(simp_all)
+  done
+
+lemma flts1:
+  assumes "good r" 
+  shows "flts [r] \<noteq> []"
+  using  assms
+  apply(induct r)
+       apply(simp_all)
+  apply(case_tac x2a)
+   apply(simp)
+  apply(simp)
+  done
+
+lemma flts2:
+  assumes "good r" 
+  shows "\<forall>r' \<in> set (flts [r]). good r'"
+  using  assms
+  apply(induct r)
+       apply(simp)
+      apply(simp)
+     apply(simp)
+    prefer 2
+    apply(simp)
+    apply(auto)[1]
+  apply (metis good.simps(5) good_fuse in_set_insert insert_Nil list.exhaust)
+   prefer 2
+   apply(simp)
+  by fastforce
+
+lemma flts3a:
+  assumes "good r" 
+  shows "good (AALTs bs (flts [r]))"
+  using  assms
+  by (metis flts1 flts2 good.simps(5) neq_Nil_conv)
+
+
+lemma flts3:
+  assumes "\<forall>r \<in> set rs. good r \<or> r = AZERO" 
+  shows "\<forall>r \<in> set (flts rs). good r"
+  using  assms
+  apply(induct rs arbitrary: rule: flts.induct)
+        apply(simp_all)
+  by (metis UnE flts2 k0a set_map)
+
+lemma flts3b:
+  assumes "\<exists>r\<in>set rs. good r"
+  shows "flts rs \<noteq> []"
+  using  assms
+  apply(induct rs arbitrary: rule: flts.induct)
+        apply(simp)
+       apply(simp)
+      apply(simp)
+      apply(auto)
+  done
+
+lemma flts4:
+  assumes "bsimp_AALTs bs (flts rs) = AZERO"
+  shows "\<forall>r \<in> set rs. \<not> good r"
+  using assms
+  apply(induct rs arbitrary: bs rule: flts.induct)
+        apply(auto)
+        defer
+  apply (metis (no_types, lifting) Nil_is_append_conv append_self_conv2 bsimp_AALTs.elims butlast.simps(2) butlast_append flts3b nonalt.simps(1) nonalt.simps(2))
+  apply (metis arexp.distinct(7) bsimp_AALTs.elims flts2 good.simps(1) good.simps(2) good0 k0b list.distinct(1) list.inject nonalt.simps(3))
+  apply (metis arexp.distinct(3) arexp.distinct(7) bsimp_AALTs.elims fuse.simps(3) list.distinct(1) list.inject)
+  apply (metis arexp.distinct(7) bsimp_AALTs.elims good.simps(1) good.simps(6) good_fuse list.distinct(1) list.inject)
+  apply (metis arexp.distinct(7) bsimp_AALTs.elims list.distinct(1) list.inject)
+  apply (metis arexp.distinct(7) bsimp_AALTs.simps(2) bsimp_AALTs.simps(3) flts.simps(1) flts.simps(2) flts1 good.simps(7) good_fuse neq_Nil_conv)
+  by (metis (no_types, lifting) Nil_is_append_conv append_Nil2 arexp.distinct(7) bsimp_AALTs.elims butlast.simps(2) butlast_append flts1 flts2 good.simps(1) good0 k0a)
+
+lemma flts_nil:
+  assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow>
+            good (bsimp y) \<or> bsimp y = AZERO"
+  and "\<forall>r\<in>set rs. \<not> good (bsimp r)"
+  shows "flts (map bsimp rs) = []"
+  using assms
+  apply(induct rs)
+   apply(simp)
+  apply(simp)
+  apply(subst k0)
+  apply(simp)
+  by force
+  
+
+lemma good1:
+  shows "good (bsimp a) \<or> bsimp a = AZERO"
+  apply(induct a taking: asize rule: measure_induct)
+  apply(case_tac x)
+       apply(simp)
+      apply(simp)
+  apply(simp)
+  prefer 3
+    apply(simp)
+   prefer 2
+  apply(simp only:)
+   apply(case_tac "x52")
+    apply(simp)
+   apply(simp only: good0a)
+  apply(frule_tac x="a" in spec)
+   apply(drule mp)
+  apply(simp)
+    apply(erule disjE)
+     prefer 2
+     apply(simp)
+   apply(frule_tac x="AALTs x51 list" in spec)
+   apply(drule mp)
+  apply(simp add: asize0)
+    apply(auto)[1]
+  apply(frule_tac x="AALTs x51 list" in spec)
+   apply(drule mp)
+    apply(simp add: asize0)
+   apply(erule disjE)
+    apply(rule disjI1)
+  apply(simp add: good0)
+    apply(subst good0)
+     apply (metis Nil_is_append_conv flts1 k0)
+  apply(simp)
+    apply(subst k0)
+    apply(simp)
+    apply(auto)[1]
+  using flts2 apply blast
+    apply (metis good0 in_set_member member_rec(2))
+   apply(simp) 
+   apply(rule disjI1)
+   apply(drule flts4)
+   apply(subst k0)
+   apply(subst good0)
+    apply (metis append_is_Nil_conv flts1 k0)
+   apply(auto)[1]
+  using flts2 apply blast
+  apply (metis add.commute add_lessD1 flts_nil list.distinct(1) list.set_cases not_less_eq)
+  (* SEQ case *)
+  apply(simp)
+  apply(case_tac "bsimp x42 = AZERO")
+    apply(simp)
+ apply(case_tac "bsimp x43 = AZERO")
+   apply(simp)
+    apply(subst (2) bsimp_ASEQ0)
+  apply(simp)
+  apply(case_tac "\<exists>bs. bsimp x42 = AONE bs")
+    apply(auto)[1]
+   apply(subst bsimp_ASEQ2)
+  using good_fuse apply force
+   apply(subst bsimp_ASEQ1)
+     apply(auto)
+  using less_add_Suc1 apply blast
+  using less_add_Suc2 by blast
+
+lemma flts_append:
+  "flts (xs1 @ xs2) = flts xs1 @ flts xs2"
+  apply(induct xs1  arbitrary: xs2  rule: rev_induct)
+   apply(auto)
+  apply(case_tac xs)
+   apply(auto)
+   apply(case_tac x)
+        apply(auto)
+  apply(case_tac x)
+        apply(auto)
+  done
+
+lemma g1:
+  assumes "good (bsimp_AALTs bs rs)"
+  shows "bsimp_AALTs bs rs = AALTs bs rs \<or> (\<exists>r. rs = [r] \<and> bsimp_AALTs bs [r] = fuse bs r)"
+using assms
+    apply(induct rs arbitrary: bs)
+  apply(simp)
+  apply(case_tac rs)
+  apply(simp only:)
+  apply(simp)
+  apply(case_tac  list)
+  apply(simp)
+  by simp
+
 lemma flts_idem:
-  assumes "\<forall>r \<in> set rs. bsimp (bsimp r) = bsimp r"
+  assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow>
+            bsimp (bsimp y) = bsimp y"
+  shows "map bsimp (flts (map bsimp rs)) = flts (map bsimp rs)"
+  using assms
+  apply(induct rs)
+   apply(simp)
+  apply(simp)
+  apply(subst k0)
+  apply(subst (2) k0) 
+  apply(simp add: flts_append)
+  using good1
+  apply -
+  apply(drule_tac x="a" in meta_spec)
+  apply(erule disjE)
+  prefer 2
+   apply(simp)
+  using flts.simps
+  apply(case_tac a)
+       apply(simp_all)
+   defer
+   apply(drule g1)
+   apply(erule disjE)
+    apply(simp)
+    defer
+    apply(auto)[1]
+    
+
+
+lemma flts_idem:
+  assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow>
+            bsimp (bsimp y) = bsimp y"
   shows "flts (map bsimp (flts (map bsimp rs))) = flts (map bsimp rs)"
   using assms
   apply(induct rs)
@@ -1066,6 +1322,31 @@
   apply(simp)
   apply(subst k0)
   apply(subst (2) k0) 
+  apply(simp add: flts_append)
+  using good1
+  apply -
+  apply(drule_tac x="a" in meta_spec)
+  apply(erule disjE)
+  prefer 2
+   apply(simp)
+  using flts.simps
+  apply(case_tac a)
+       apply(simp_all)
+   defer
+   apply(drule g1)
+   apply(erule disjE)
+    apply(simp)
+    defer
+    apply(auto)[1]
+  
+   apply(subst g1)
+    apply(simp)
+   apply(simp)
+  apply (me tis (full_types) arexp.inject(4) bsimp_AALTs.simps(2) flts3a fuse_empty g1 list.distinct(1))
+  
+  
+
+
   apply(case_tac "bsimp a = AZERO")
    apply(simp)
   apply(case_tac "nonalt (bsimp a)")
@@ -1093,91 +1374,6 @@
   apply(simp_all)
   oops
 
-lemma bsimp_AALTs_idem:
-  (*assumes "\<forall>r \<in> set rs. bsimp (bsimp r) = bsimp r \<and> nonalt (bsimp r)" *)
-  (*assumes "\<forall>r \<in> set rs. bsimp (bsimp r) = bsimp r" *)
-  shows "bsimp (bsimp_AALTs bs rs) = bsimp_AALTs bs (flts (map bsimp rs))"
-  apply(induct rs arbitrary: bs taking: "\<lambda>rs. sum_list (map asize rs)" rule: measure_induct)
-  apply(case_tac x)
-  apply(simp)
-  apply(simp)
-  apply(case_tac "\<exists>bs'  rs'. a = AALTs bs' rs'")
-   apply(clarify)
-  apply(case_tac list)
-        apply(simp)
-       apply(simp) 
-
-  apply(drule_tac x="flts (rs' @ list)" in spec)
-  apply(erule impE)
-  prefer 2
-  apply(case_tac a)
-       apply(simp)
-       apply(case_tac list)
-        apply(simp)
-       apply(simp) 
-   apply(case_tac list)
-        apply(simp)
-      apply(simp) 
-   apply(case_tac list)
-        apply(simp)
-     apply(simp) 
-  prefer 3
-   apply(case_tac list)
-        apply(simp)
-       apply(simp) 
-   apply(case_tac list)
-    apply(simp)
-      
-
-       apply(simp) 
-
-      apply(case_tac "flts (map bsimp list)")
-       apply(simp)
-      apply(simp)
-  
-  
-
-   prefer 2
-   apply(simp)
-  
-   apply(subst k0)
-   apply(subst (2) k0)
-  
-  apply(case_tac a)
-       apply(simp_all)
-  
-  prefer 2
-   apply(simp)
-  apply(case_tac r)
-       apply(auto)
-   apply(case_tac "bsimp x42 = AZERO")
-    apply(simp)
- apply(case_tac "bsimp x43 = AZERO")
-   apply(simp)
-   apply(subst bsimp_ASEQ0)
-   apply(subst bsimp_ASEQ0)
-  apply(simp)
-  apply(case_tac "\<exists>bs. bsimp x42 = AONE bs")
-    apply(auto)[1]
-    apply(subst bsimp_ASEQ2)
-   apply(subst bsimp_ASEQ2)
-  prefer 2
-      apply(subst bsimp_ASEQ1)
-      apply(auto)
-  apply(subst bsimp_ASEQ1)
-      apply(auto)
-  apply(subst (asm) bsimp_ASEQ2)
-   apply(subst (asm) bsimp_ASEQ2)
-  using flts_fuse bsimp_fuse bsimp_fuse_AALTs bsimp_fuse_AALTs2 bsimp_AALTs.simps flts.simps
-    
-   apply(case_tac x43)
-        apply(simp_all)
-    prefer 3
-  oops
-
-lemma ww:
-  shows "bsimp_AALTs bs [r] = fuse bs r"
-  by simp
 
 lemma flts_0:
   assumes "nonnested (AALTs bs  rs)"
@@ -1194,15 +1390,17 @@
   apply(rule ballI)
   apply(simp)
   done
+
+lemma flts_0a:
+  assumes "nonnested (AALTs bs  rs)"
+  shows "AZERO \<notin> set (flts rs)"
+  using assms
+  using flts_0 by blast 
   
-lemma q1:
+lemma qqq1:
   shows "AZERO \<notin> set (flts (map bsimp rs))"
-  apply(induct rs)
-   apply(simp)
-  apply(simp)
-  apply(case_tac rs)
-  apply(simp)
-
+  by (metis ex_map_conv flts3 good.simps(1) good1)
+  
 lemma cc:
   assumes "bsimp (fuse bs' r) = (AALTs bs rs)" 
   shows "\<forall>r \<in> set  rs. r \<noteq> AZERO"
@@ -1290,7 +1488,7 @@
   apply(case_tac "\<exists>bs'. bsimp r1 = AONE bs'")
     apply(auto)
     apply (simp add: bsimp_ASEQ2)
-  using bsimp_fuse apply fastforce
+  using bsimp_fuse apply fast force
    apply (simp add: bsimp_ASEQ1)
   
   
@@ -1340,6 +1538,13 @@
    apply(subst bsimp_AALTs_qq)
     apply(auto)[1]
    apply(simp)
+   apply(subst k0)
+   apply(simp)
+   apply(simp add: flts_append)
+   apply(subst (2) k0)
+  
+   apply(simp add: flts_append)
+
    prefer 2
   apply(subgoal_tac "length (flts (bsimp a # map bsimp list)) = 0 \<or> 
                      length (flts (bsimp a # map bsimp list)) = 1")
@@ -2300,17 +2505,6 @@
   apply(simp)
   oops
 
-lemma flts_append:
-  "flts (xs1 @ xs2) = flts xs1 @ flts xs2"
-  apply(induct xs1  arbitrary: xs2  rule: rev_induct)
-   apply(auto)
-  apply(case_tac xs)
-   apply(auto)
-   apply(case_tac x)
-        apply(auto)
-  apply(case_tac x)
-        apply(auto)
-  done
 
 lemma flts_bsimp:
   "flts (map bsimp rs) = map bsimp (flts rs)"