# HG changeset patch
# User Chengsong
# Date 1662419923 -7200
# Node ID 19d304554ae145ae349f3b16ec897362d63ef202
# Parent  b306628a0eab067bc8cf48a127eb11254ac0b338
more bsimpidem

diff -r b306628a0eab -r 19d304554ae1 thys4/posix/FBound.thy
--- a/thys4/posix/FBound.thy	Sat Sep 03 00:14:20 2022 +0100
+++ b/thys4/posix/FBound.thy	Tue Sep 06 01:18:43 2022 +0200
@@ -236,6 +236,35 @@
   shows "map rerase (flts (map bsimp rs)) = map rerase rs \<Longrightarrow> map rerase (map bsimp rs) = map rerase rs"
   oops
 
+
+  thm asize.simps
+fun s_complexity:: "arexp \<Rightarrow> nat" where
+    "s_complexity AZERO = 1"
+  | "s_complexity (AONE _) = 1"
+  | "s_complexity (ASTAR bs r) = Suc (s_complexity r)"
+  | "s_complexity (AALTs bs rs) = Suc (Suc (sum_list (map s_complexity rs)))"
+  | "s_complexity (ASEQ bs r1 r2) = Suc (s_complexity r1 + s_complexity r2)"
+  | "s_complexity (ACHAR _ _) = 1"
+  | "s_complexity (ANTIMES _ r _) = Suc (s_complexity r)"
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
 inductive leq1 ("_ \<le>1 _" [80, 80] 80) where  
   "r1 \<le>1 r1"
 | "AZERO \<le>1 ASEQ bs AZERO r" 
@@ -254,6 +283,12 @@
 | "\<lbrakk>r1' \<le>1 r1;  r2' \<le>1 r2\<rbrakk> \<Longrightarrow> bsimp_ASEQ bs1 r1' r2' \<le>1 ASEQ bs1 r1 r2"
 | "\<lbrakk>AALTs bs rs1 \<le>1 AALTs bs rs2; r1 \<le>1 r2 \<rbrakk> \<Longrightarrow> AALTs bs (r1 # rs1) \<le>1 AALTs bs (r2 # rs2)"
 | "\<lbrakk>r1 \<le>1 r2; r2 \<le>1 r3 \<rbrakk> \<Longrightarrow> r1 \<le>1 r3"
+| "AALTs bs (rs1 @ distinctWith rs2 eq1 (set rs1)) \<le>1 AALTs bs (rs1 @ rs2)"
+| "bsimp_AALTs bs rs \<le>1 AALTs bs rs"
+
+
+
+
 
 
 lemma leq1_6_variant1:
@@ -278,16 +313,61 @@
    apply (simp add: leq1.intros(1) leq1.intros(16))
   using leq1.intros(1) leq1.intros(16) by force
 
-lemma dB_leq12:
-  shows "AALTs bs (rs1 @ (distinctWith rs1 eq1 (set rs2))) \<le>1 AALTs bs (rs1 @ rs2)"
-  apply(induct rs1 arbitrary: rs2)
-  apply simp
-  sorry
+
 
 
 lemma dB_leq1:
   shows "AALTs bs (distinctWith rs eq1 {}) \<le>1 AALTs bs rs"
-  sorry
+  by (metis append_Nil empty_set leq1.intros(18))
+
+lemma leq1_list:
+  shows "
+       \<lbrakk>\<And>x2aa. x2aa \<in> set x2a \<Longrightarrow> bsimp x2aa \<le>1 x2aa;
+        bsimp_AALTs x1 (distinctWith (flts (map bsimp x2a)) eq1 {}) \<le>1 AALTs x1 (distinctWith (flts (map bsimp x2a)) eq1 {});
+        AALTs x1 (distinctWith (flts (map bsimp x2a)) eq1 {}) \<le>1 AALTs x1 (flts (map bsimp x2a));
+        AALTs x1 (flts (map bsimp x2a)) \<le>1 AALTs x1 (map bsimp x2a)\<rbrakk>
+       \<Longrightarrow> AALTs x1 (map bsimp x2a) \<le>1 AALTs x1 x2a"
+  apply(induct x2a)
+   apply simp
+  by (simp add: dB_leq1 flts_leq1 leq1.intros(16) leq1.intros(19))
+
+
+
+lemma bsimp_leq1:
+  shows "bsimp r \<le>1 r"
+  apply(induct r)
+        apply simp
+  
+  apply (simp add: leq1.intros(1))
+  
+  using leq1.intros(1) apply force
+  
+  apply (simp add: leq1.intros(1))
+
+  
+     apply (simp add: leq1.intros(15))
+  prefer 2
+
+  apply (simp add: leq1.intros(1))
+   prefer 2
+  
+  apply (simp add: leq1.intros(1))
+  apply simp
+  apply(subgoal_tac " bsimp_AALTs x1 (distinctWith (flts (map bsimp x2a)) eq1 {}) \<le>1  AALTs x1 (distinctWith (flts (map bsimp x2a)) eq1 {})")
+  apply(subgoal_tac " AALTs x1 (distinctWith (flts (map bsimp x2a)) eq1 {}) \<le>1  AALTs x1 ( (flts (map bsimp x2a)) )")
+    apply(subgoal_tac " AALTs x1 ( (flts (map bsimp x2a)) ) \<le>1  AALTs x1 ( ( (map bsimp x2a)) )")
+
+    apply(subgoal_tac " AALTs x1 ( map bsimp x2a ) \<le>1  AALTs x1   x2a ")
+  
+  apply (meson leq1.intros(17))
+  
+  using leq1_list apply blast
+
+  using flts_leq1 apply presburger
+  
+  using dB_leq1 apply blast
+  
+  using leq1.intros(19) by blast
 
 
 
@@ -298,6 +378,36 @@
         apply simp+
   done
 
+
+lemma rerase_arexp_additional1:
+  shows " asize (AALTs bs (rs1 @ rs2)) = rsize (RALTS (map rerase rs1 @ map rerase rs2))"
+  apply simp
+  by (metis (mono_tags, lifting) asize_rsize comp_apply map_eq_conv)
+
+  
+
+
+lemma rerase2:
+  shows "rsizes (map rerase (distinctWith rs2 eq1 (set rs1))) \<le> rsizes (map rerase rs2)"
+  apply(induct rs2 arbitrary: rs1)
+   apply simp+
+  by (metis List.set_insert trans_le_add2)
+
+lemma rerase3:
+  shows "rsize (RALTS (map rerase rs1 @ map rerase (distinctWith rs2 eq1 (set rs1)))) \<le> rsize (RALTS (map rerase rs1 @ map rerase rs2))"
+  using rerase2 by force
+
+
+lemma bsimpalts_size:
+  shows "asize (bsimp_AALTs bs rs) \<le> asize (AALTs bs rs)"
+  apply(case_tac rs)
+   apply simp
+  apply(case_tac list)
+   apply auto
+  by (metis asize_rsize dual_order.refl le_SucI rerase_fuse)
+  
+
+
 lemma leq1_size:
   shows "r1 \<le>1 r2 \<Longrightarrow> asize r1 \<le> asize r2"
   apply (induct rule: leq1.induct)
@@ -316,7 +426,13 @@
    apply simp
   apply (metis asize_rsize le_SucI rerase_fuse trans_le_add2)
   apply (smt (verit, best) Suc_eq_plus1 ab_semigroup_add_class.add_ac(1) add.commute add.right_neutral add_cancel_right_right add_mono_thms_linordered_semiring(1) asize.simps(5) asize_rsize nat_add_left_cancel_le order.trans order_trans plus_1_eq_Suc rSEQ_mono rerase_bsimp_ASEQ rsize.simps(5))
-  sorry
+     apply simp
+  
+  using dual_order.trans apply blast
+  
+  using rerase3 rerase_arexp_additional1 apply force
+  using bsimpalts_size by blast
+  
 
 
 
@@ -357,153 +473,171 @@
   apply simp
   apply(simp add: asize_rsize)
   apply (simp add: rerase_fuse size_deciding_equality4)
-  apply (metis Suc_n_not_le_n asize_rsize leq1.intros(15) leq1_size rsize.simps(5) trans_le_add2)
-  sorry
+    apply (metis Suc_n_not_le_n asize_rsize leq1.intros(15) leq1_size rsize.simps(5) trans_le_add2)
+  apply simp
+  
+  apply (metis asize_rsize leq1_size lessI nle_le not_add_less2 plus_1_eq_Suc rsize.simps(5) trans_le_add2)
+   apply simp
+  by (metis Suc_n_not_le_n bsimpalts_size rsize.simps(5) size_deciding_equality5 trans_le_add2)
+
+lemma leq1_neq:
+  shows "\<lbrakk>r1 \<le>1 r2 ; r1 \<noteq> r2\<rbrakk> \<Longrightarrow> asize r1 < asize r2"
+  apply(induct rule : leq1.induct)
+                    apply simp+
+                 apply (metis asize_rsize lessI less_SucI rerase_fuse)
+  apply simp+
+  
+               apply (metis (mono_tags, lifting) comp_apply less_SucI map_eq_conv not_less_less_Suc_eq rerase_fuse size_deciding_equality3)
+  apply simp
+  
+  apply (simp add: asize0)
+  
+  using less_Suc_eq apply auto[1]
+            apply simp
+           apply simp
+          apply simp
+         apply simp
+
+  oops
+
+lemma leq1_leq_case1:
+  shows " \<lbrakk>r1 \<le>1 r2; r1 = r2 \<or> rerase r1 \<noteq> rerase r2; r2 \<le>1 r3; r2 = r3 \<or> rerase r2 \<noteq> rerase r3\<rbrakk> \<Longrightarrow> r1 = r3 \<or> rerase r1 \<noteq> rerase r3"
+  apply(induct rule: leq1.induct)
+                    apply simp+
+  
+  apply (metis rerase.elims rrexp.distinct(1) rrexp.distinct(11) rrexp.distinct(3) rrexp.distinct(5) rrexp.distinct(7) rrexp.distinct(9))
+                  apply simp
+
+                  apply (metis leq1_trans1 rerase.simps(1) rerase.simps(5))
+
+                 apply (metis leq1_trans1 rerase.simps(5) rerase_fuse)
+                apply simp
+                apply auto
+ 
+  oops
+
+
+
+lemma scomp_rerase3:
+  shows "r1 ~1 r2 \<Longrightarrow> s_complexity r1 = s_complexity r2"
+  apply(induct rule: eq1.induct)
+                      apply simp+
+  done
 
   
 
-lemma leq1_less_or_equal: shows
-"r1 \<le>1 r2 \<Longrightarrow> r1 = r2 \<or> rerase r1 \<noteq> rerase r2"
-  apply(induct rule: leq1.induct)
-               apply simp
-              apply simp
-  apply simp
-            apply (simp add: rerase_fuse)
-           apply simp
-  apply simp
-  using r_finite1 rerase_fuse apply force
-         apply simp
-        apply simp
-        apply(case_tac "r1 = r2")
-         apply simp
-        apply simp
-  
-  using leq1_trans1 apply presburger
-       apply simp
-      apply simp
-     apply simp
-    apply simp
-   apply simp
-   apply simp
 
-  using r_finite1 rerase_fuse apply auto[1]
-  apply (smt (verit, best) BlexerSimp.bsimp_ASEQ0 BlexerSimp.bsimp_ASEQ2 bsimp_ASEQ.simps(1) bsimp_ASEQ1 leq1_trans1 rerase.simps(5) rerase_bsimp_ASEQ rerase_fuse rrexp.inject(2) rsimp_SEQ.simps(22))
-  sorry
+lemma scomp_rerase2:
+  shows "rerase r1 = rerase r2 \<Longrightarrow> s_complexity r1 = s_complexity r2"  
+  using eq1rerase scomp_rerase3 by blast
 
 
 
 
 
-lemma arexpfiniteaux4:
-  shows"
-       \<lbrakk>\<And>x. \<lbrakk>x \<in> set rs; rerase (bsimp x) = rerase x\<rbrakk> \<Longrightarrow> bsimp x = x;
-        rerase (bsimp_AALTs bs1 (distinctWith (flts (map bsimp rs)) eq1 {})) = RALTS (map rerase rs)\<rbrakk>
-       \<Longrightarrow> bsimp_AALTs bs1 (distinctWith (flts (map bsimp rs)) eq1 {}) = AALTs bs1 rs"
-  apply(induct rs)
+lemma scomp_rerase:
+  shows "s_complexity r1 < s_complexity r2 \<Longrightarrow>rerase  r1 \<noteq> rerase r2"
+  by (metis nat_neq_iff scomp_rerase2)
+
+thm bsimp_ASEQ.simps
+
+lemma scomp_bsimpalts:
+  shows "s_complexity (bsimp_ASEQ bs1 r1' r2') \<le> s_complexity (ASEQ bs1 r1' r2')"
+  apply(case_tac "r1' = AZERO")
+   apply simp
+  apply(case_tac "r2' = AZERO")
   apply simp
+  apply(case_tac "\<exists>bs2. r1' = AONE bs2")
+   apply(erule exE)
+ 
+   apply simp
   
+  apply (metis le_SucI le_add2 plus_1_eq_Suc rerase_fuse scomp_rerase2)
+  apply(subgoal_tac "bsimp_ASEQ bs1 r1' r2' = ASEQ bs1 r1' r2'")
+   apply simp
+  using bsimp_ASEQ1 by presburger
+  
+
+lemma scompsize_aux:
+  shows "s_complexity (AALTs bs (rs1 @ distinctWith rs2 eq1 (set rs1))) \<le> s_complexity (AALTs bs (rs1 @ rs2))"
+  sorry
+
+
+
+lemma scomp_size_reduction:
+  shows "r1 \<le>1 r2 \<Longrightarrow> s_complexity r1 \<le> s_complexity r2"
+  apply(induct rule: leq1.induct)
+                    apply simp+
+                 apply (metis le_SucI le_add2 plus_1_eq_Suc rerase_fuse scomp_rerase2)
+  apply simp+
+  
+  apply (smt (verit) comp_apply dual_order.eq_iff map_eq_conv plus_1_eq_Suc rerase_fuse scomp_rerase2 trans_le_add2)
+              apply simp+
+  
+       apply (metis le_SucI le_add2 plus_1_eq_Suc rerase_fuse scomp_rerase2)
+
+
+  
+  apply (smt (verit, del_insts) add_mono_thms_linordered_semiring(1) dual_order.trans le_numeral_extra(4) plus_1_eq_Suc s_complexity.simps(5) scomp_bsimpalts)
+     apply simp
+    apply simp
+  
+  using scompsize_aux apply auto[1]
+  apply(case_tac rs)
+   apply simp
+  apply(case_tac "list")
+   apply auto
+  by (metis eq_imp_le le_imp_less_Suc less_imp_le_nat rerase_fuse scomp_rerase2)
 
 
 
 
 
+
+
+
+lemma compl_rrewrite_down:
+  shows "r1 \<le>1 r2 \<Longrightarrow>r1 = r2 \<or> s_complexity r1 < s_complexity r2"
+  
+  apply(induct rule: leq1.induct)
+                    apply simp
+                   apply simp
+                  apply simp
+  apply (smt (verit) fuse.elims lessI less_Suc_eq plus_1_eq_Suc s_complexity.simps(2) s_complexity.simps(3) s_complexity.simps(4) s_complexity.simps(5) s_complexity.simps(6) s_complexity.simps(7))
+                apply simp
   sorry
 
 
+lemma compl_rrewrite_down1:
+  shows "\<lbrakk>r1 \<le>1 r2; s_complexity r1 = s_complexity r2 \<rbrakk> \<Longrightarrow> r1 = r2"
+  using compl_rrewrite_down nat_less_le by auto
+
+
+
+lemma leq1_less_or_equal: shows
+"r1 \<le>1 r2 \<Longrightarrow> r1 = r2 \<or> rerase r1 \<noteq> rerase r2"
+  using compl_rrewrite_down scomp_rerase by blast
+
+
+
+
+
+
+
+
+
 
 
 lemma arexp_finite1:
   shows "rerase (bsimp b) = rerase b \<Longrightarrow> bsimp b = b"
-  apply(induct rule: bsimp.induct)
-        apply simp
-        apply (smt (verit) arexpfiniteaux1 arexpfiniteaux2 arexpfiniteaux3 bsimp_ASEQ1 rerase.simps(5) rrexp.inject(2))
-  apply simp
+  using bsimp_leq1 leq1_less_or_equal by blast
   
-  using arexpfiniteaux4 apply blast
-      apply simp+
-  done
-(*
-  apply(induct b)
-        apply simp+
-         apply(case_tac "bsimp b2 = AZERO")
-          apply simp
-     apply (case_tac "bsimp b1 = AZERO")
-      apply simp
-  apply(case_tac "\<exists>bs. bsimp b1 = AONE bs")
-  using arexpfiniteaux1 apply blast
-     apply simp
-     apply(subgoal_tac "bsimp_ASEQ x1 (bsimp b1) (bsimp b2) = ASEQ x1 (bsimp b1) (bsimp b2)")
-  apply simp
-  using bsimp_ASEQ1 apply presburger
-  apply simp
-
-  sorry
-*)
-
-
-lemma bitcodes_unchanging2:
-  assumes "bsimp a = b"
-and "a ~1 b"
-shows "a = b"
-  using assms
-  apply(induct rule: eq1.induct)
-                      apply simp
-                      apply simp
-                      apply simp
-
-                      apply auto
-  
-  sorry
+lemma bsimp_idem:
+  shows "bsimp (bsimp r ) = bsimp r"
+  using arexp_finite1 bsimp_rerase rsimp_idem by presburger
 
 
 
-lemma bsimp_reduces:
-  shows "bsimp r \<le>1 r"
-  apply(induct rule: bsimp.induct)
-        apply simp
-        apply (simp add: leq1.intros(15))
-       apply simp
-  apply(case_tac rs)
-        apply simp
-  
-  apply (simp add: leq1.intros(13))
-       apply(case_tac list)
-        apply simp
-  
-
-  sorry
-
 
 
-lemma bitcodes_unchanging:
-  shows "\<lbrakk>bsimp a = b; rerase a = rerase b \<rbrakk> \<Longrightarrow> a = b"
-  apply(induction a arbitrary: b)
-        apply simp+
-     apply(case_tac "\<exists>bs. bsimp a1 = AONE bs")
-      apply(erule exE)
-      apply simp
-      prefer 2
-      apply(case_tac "bsimp a1 = AZERO")
-       apply simp
-      apply simp
-      apply (metis BlexerSimp.bsimp_ASEQ0 bsimp_ASEQ1 rerase.simps(1) rerase.simps(5) rrexp.distinct(5) rrexp.inject(2))
-  
-  sorry
-
-
-lemma bagnostic_shows_bsimp_idem:
-  assumes "bitcode_agnostic bsimp"
-and "rerase (bsimp a) = rsimp (rerase a)"
-and "rsimp r = rsimp (rsimp r)"
-shows "bsimp a = bsimp (bsimp a)"
-  
-  oops
-
-theorem bsimp_idem:
-  shows "bsimp (bsimp a) = bsimp a"
-  using bitcodes_unchanging bsimp_rerase rsimp_idem by auto
-
-
-unused_thms
-
 end