# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1557917512 -3600
# Node ID 09ce1cdb70ab1fcaf9d963db783170e38b47689e
# Parent  22e34f93cd5d08c0e37909c55f68fb10be6a2033
updated

diff -r 22e34f93cd5d -r 09ce1cdb70ab exps/bit-test.scala
--- a/exps/bit-test.scala	Tue May 14 21:43:11 2019 +0100
+++ b/exps/bit-test.scala	Wed May 15 11:51:52 2019 +0100
@@ -691,7 +691,7 @@
   flatten.toSet.flatten.minBy(a => asize(a._1))
 
 // tests about good
-def good (a: ARexp) : Boolean = a match {
+def good(a: ARexp) : Boolean = a match {
   case AZERO => false
   case AONE(_) => true
   case APRED(_, _, _) => true
diff -r 22e34f93cd5d -r 09ce1cdb70ab thys/BitCoded.thy
--- a/thys/BitCoded.thy	Tue May 14 21:43:11 2019 +0100
+++ b/thys/BitCoded.thy	Wed May 15 11:51:52 2019 +0100
@@ -577,9 +577,6 @@
 | "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"
@@ -1088,7 +1085,7 @@
   by (metis good.simps(4) good.simps(5) neq_Nil_conv)
 
 lemma good0:
-  assumes "rs \<noteq> Nil"
+  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)
@@ -1096,12 +1093,12 @@
   done
 
 lemma good0a:
-  assumes "flts (map bsimp rs) \<noteq> Nil"
+  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)
+   apply(simp)
   done
 
 lemma flts0:
@@ -1283,97 +1280,6 @@
   apply(simp)
   by simp
 
-lemma flts_idem:
-  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)
-   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]
-  
-   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)")
-  thm k0 k0a k0b
-  apply(subst k0b)
-     apply(simp)
-    apply(simp)
-   apply(simp)
-  apply(subst k0b)
-     apply(simp)
-    apply(simp)
-   apply(simp)
-  apply(subst k0)
-  apply(subst k0b)
-     apply(simp)
-    apply(simp)
-   apply(simp)
-  apply(simp)
-  apply(simp add: k00)
-  apply(subst k0a2)
-   apply(simp)
-  apply(subst k0a2)
-   apply(simp)
-  apply(case_tac a)
-  apply(simp_all)
-  oops
-
 
 lemma flts_0:
   assumes "nonnested (AALTs bs  rs)"
@@ -1442,63 +1348,7 @@
   apply(simp)
   apply(case_tac list)
    apply(simp)  
-  
-  
-  apply(subgoal_tac "\<forall>r \<in> set (flts (map bsimp rs)). r \<noteq> AZERO")
-   prefer 2
-   apply(rule_tac bs="bs' @ bs1" in flts_0)
-  
-  
-  thm bsimp_AALTs_qq
-  apply(case_tac "1 < length rs")
-  apply(drule_tac bsimp_AALTs_qq)
-  apply(subgoal_tac "nonnested (AALTs bs rsa)")
-   prefer 2
-   apply (metis nn1b)
-  apply(rule ballI)
-  apply(simp)
-  apply(drule_tac x="r" in meta_spec)
-  apply(simp)
-  (* HERE *)
-  apply(drule flts_0)
-  
-  
-  
-  apply(simp)
-  
-  
-  
-  
-  apply(subst 
-
-  apply (sm t arexp.distinct(15) arexp.distinct(21) arexp.distinct(25) arexp.distinct(29) arexp.inject(4) b1 fuse.elims)
-    
-   prefer 2
-  
-  
-  apply(induct r arbitrary: rs bs bs' rule: bsimp.induct)
-       apply(auto)
-  apply(case_tac "bsimp r1 = AZERO")
-    apply simp
-   apply(case_tac "bsimp r2 = AZERO")
-    apply(simp)
-    apply(case_tac "\<exists>bs'. bsimp r1 = AONE bs'")
-     apply(auto)
-  apply (simp add: bsimp_ASEQ0)
-  apply(case_tac "\<exists>bs'. bsimp r1 = AONE bs'")
-    apply(auto)
-    apply (simp add: bsimp_ASEQ2)
-  using bsimp_fuse apply fast force
-   apply (simp add: bsimp_ASEQ1)
-  
-  
-  
-  apply(subst 
-
-  apply (sm t arexp.distinct(15) arexp.distinct(21) arexp.distinct(25) arexp.distinct(29) arexp.inject(4) b1 fuse.elims)
-    
-   prefer 2
-  
+  oops  
 
 
 lemma ww1:
@@ -1516,6 +1366,35 @@
   apply(auto)
   oops
 
+fun nonazero :: "arexp \<Rightarrow> bool"
+  where
+  "nonazero AZERO = False"
+| "nonazero r = True"
+
+lemma flts_concat:
+  shows "flts rs = concat (map (\<lambda>r. flts [r]) rs)"
+  apply(induct rs)
+   apply(auto)
+  apply(subst k0)
+  apply(simp)
+  done
+
+lemma flts_single1:
+  assumes "nonalt r" "nonazero r"
+  shows "flts [r] = [r]"
+  using assms
+  apply(induct r)
+  apply(auto)
+  done
+
+lemma test:
+  assumes "good  r"
+  shows "bsimp (r) = r"
+  using assms
+  apply(induct r)
+  apply(simp_all)
+
+
 lemma bsimp_idem:
   shows "bsimp (bsimp r) = bsimp r"
 apply(induct r taking: "asize" rule: measure_induct)
@@ -1542,8 +1421,44 @@
    apply(simp)
    apply(simp add: flts_append)
    apply(subst (2) k0)
-  
-   apply(simp add: flts_append)
+   apply(subst (asm) k0)
+   apply(simp)
+   apply(subgoal_tac "good (bsimp a) \<or> bsimp a = AZERO")
+    prefer 2
+  using good1 apply blast
+   apply(erule disjE)
+    prefer 2
+    apply(simp)
+    apply(drule_tac x="AALTs x51 list" in spec)
+    apply(drule mp)
+  apply(simp add: asize0)
+    apply(simp)
+    apply (simp add: bsimp_AALTs_qq)
+   apply(case_tac "nonalt (bsimp a)")
+  apply(subst flts_single1)
+      apply(simp)
+  using nonazero.elims(3) apply force
+    apply(simp)
+  apply(subst k0b)
+      apply(simp)
+     apply(auto)[1]
+  apply(subst k0b)
+      apply(simp)
+     apply(auto)[1]
+    apply(simp)
+  (* HERE *)
+    apply(subst (asm) flts_single1)
+      apply(simp)
+     apply(simp)
+  using nonazero.elims(3) apply force
+    apply(simp)
+  apply(subst (2) bsimp_AALTs_qq)
+     apply(auto)[1]
+  apply(subst bsimp_AALTs_qq)
+     apply(auto)[1]
+     apply(case_tac list)
+      apply(simp)
+  apply(simp)
 
    prefer 2
   apply(subgoal_tac "length (flts (bsimp a # map bsimp list)) = 0 \<or>