--- a/thys2/BasicIdentities.thy Mon Apr 04 23:56:40 2022 +0100
+++ b/thys2/BasicIdentities.thy Thu Apr 07 21:31:29 2022 +0100
@@ -363,9 +363,7 @@
apply(simp_all)
done
-lemma inside_simp_removal:
- shows " rsimp (rder x (rsimp r)) = rsimp (rder x r)"
- sorry
+
lemma set_related_list:
shows "distinct rs \<Longrightarrow> length rs = card (set rs)"
@@ -378,15 +376,6 @@
-lemma rders_simp_same_simpders:
- shows "s \<noteq> [] \<Longrightarrow> rders_simp r s = rsimp (rders r s)"
- apply(induct s rule: rev_induct)
- apply simp
- apply(case_tac "xs = []")
- apply simp
- apply(simp add: rders_append rders_simp_append)
- using inside_simp_removal by blast
-
@@ -432,6 +421,11 @@
shows "rnullable (rders r s) = rnullable (rders_simp r s)"
sorry
+lemma der_simp_nullability:
+ shows "rnullable r = rnullable (rsimp r)"
+ sorry
+
+
lemma first_elem_seqder:
shows "\<not>rnullable r1p \<Longrightarrow> map rsimp (rder x (RSEQ r1p r2)
# rs) = map rsimp ((RSEQ (rder x r1p) r2) # rs) "
--- a/thys2/ClosedForms.thy Mon Apr 04 23:56:40 2022 +0100
+++ b/thys2/ClosedForms.thy Thu Apr 07 21:31:29 2022 +0100
@@ -498,7 +498,17 @@
lemma grewrite_rdistinct_aux:
shows "rs @ rdistinct rsa rset \<leadsto>g* rs @ rdistinct rsa (rset \<union> set rs)"
- sorry
+ apply(induct rsa arbitrary: rs rset)
+ apply simp
+ apply(case_tac " a \<in> rset")
+ apply simp
+ apply(case_tac "a \<in> set rs")
+ apply simp
+ apply (metis Un_insert_left Un_insert_right gmany_steps_later grewrite_variant1 insert_absorb)
+ apply simp
+ apply(drule_tac x = "rs @ [a]" in meta_spec)
+ by (metis Un_insert_left Un_insert_right append.assoc append.right_neutral append_Cons append_Nil insert_absorb2 list.simps(15) set_append)
+
lemma grewrite_rdistinct_worth1:
shows "(rsb @ [a]) @ rdistinct rs set1 \<leadsto>g* (rsb @ [a]) @ rdistinct rs (insert a set1)"
@@ -540,11 +550,37 @@
lemma flts_gstar:
shows "rs \<leadsto>g* rflts rs"
- sorry
+ apply(induct rs)
+ apply simp
+ apply(case_tac "a = RZERO")
+ apply simp
+ using gmany_steps_later grewrite.intros(1) apply blast
+ apply(case_tac "\<exists>rsa. a = RALTS rsa")
+ apply(erule exE)
+ apply simp
+ apply (meson grewrite.intros(2) grewrites.simps grewrites_cons)
+ by (simp add: grewrites_cons rflts_def_idiot)
+
-lemma create_nonexistent_distinct_set:
+lemma wrong1:
shows "a \<in> set rs1 \<Longrightarrow> rs1 @ (rdistinct rs (insert a rset)) \<leadsto>g* rs1 @ (rdistinct rs (rset))"
- sorry
+
+ oops
+
+lemma more_distinct1:
+ shows " \<lbrakk>\<And>rsb rset rset2.
+ rset2 \<subseteq> set rsb \<Longrightarrow> rsb @ rdistinct rs rset \<leadsto>g* rsb @ rdistinct rs (rset \<union> rset2);
+ rset2 \<subseteq> set rsb; a \<notin> rset; a \<in> rset2\<rbrakk>
+ \<Longrightarrow> rsb @ a # rdistinct rs (insert a rset) \<leadsto>g* rsb @ rdistinct rs (rset \<union> rset2)"
+ apply(subgoal_tac "rsb @ a # rdistinct rs (insert a rset) \<leadsto>g* rsb @ rdistinct rs (insert a rset)")
+ apply(subgoal_tac "rsb @ rdistinct rs (insert a rset) \<leadsto>g* rsb @ rdistinct rs (rset \<union> rset2)")
+ apply (meson greal_trans)
+ apply (metis Un_iff Un_insert_left insert_absorb)
+ by (simp add: gr_in_rstar grewrite_variant1 in_mono)
+
+
+
+
lemma grewrites_in_distinct0:
shows "a \<in> set rs1 \<Longrightarrow> rs1 @ (rdistinct (a # rs) rset) \<leadsto>g* rs1 @ (rdistinct rs rset)"
@@ -562,13 +598,38 @@
lemma frewrite_rd_grewrites_aux:
- shows " rsb @
- rdistinct (RALTS rs # rsa)
- (set rsb) \<leadsto>g* rsb @
- rdistinct rs (set rsb) @ rdistinct rsa (insert (RALTS rs) (set rs) \<union> set rsb)"
+ shows " RALTS rs \<notin> set rsb \<Longrightarrow>
+ rsb @
+ RALTS rs #
+ rdistinct rsa
+ (insert (RALTS rs)
+ (set rsb)) \<leadsto>g* rflts rsb @
+ rdistinct rs (set rsb) @ rdistinct rsa (set rs \<union> set rsb \<union> {RALTS rs})"
+ apply simp
+ apply(subgoal_tac "rsb @
+ RALTS rs #
+ rdistinct rsa
+ (insert (RALTS rs)
+ (set rsb)) \<leadsto>g* rsb @
+ rs @
+ rdistinct rsa
+ (insert (RALTS rs)
+ (set rsb)) ")
+ apply(subgoal_tac " rsb @
+ rs @
+ rdistinct rsa
+ (insert (RALTS rs)
+ (set rsb)) \<leadsto>g*
+ rsb @
+ rdistinct rs (set rsb) @
+ rdistinct rsa
+ (insert (RALTS rs)
+ (set rsb)) ")
+ apply (smt (verit, ccfv_SIG) Un_insert_left flts_gstar greal_trans grewrite_rdistinct_aux grewritess_concat inf_sup_aci(5) rdistinct_concat_general rdistinct_set_equality set_append)
+ apply (metis append_assoc grewrites.intros(1) grewritess_concat gstar_rdistinct_general)
+ by (simp add: gr_in_rstar grewrite.intros(2) grewrites_append)
- sorry
@@ -698,10 +759,24 @@
apply (simp add: insert_absorb)
by auto
+lemma middle_grewrites:
+"rs1 \<leadsto>g* rs2 \<Longrightarrow> rsa @ rs1 @ rsb \<leadsto>g* rsa @ rs2 @ rsb "
+ by (simp add: grewritess_concat)
+
+lemma rdistinct_removes_all:
+ shows "set rs \<subseteq> rset \<Longrightarrow> rdistinct rs rset = []"
+
+ by (metis append.right_neutral rdistinct.simps(1) rdistinct_concat)
lemma ends_removal:
shows " rsb @ rdistinct rs (set rsb) @ RALTS rs # rsc \<leadsto>g* rsb @ rdistinct rs (set rsb) @ rsc"
- sorry
+ apply(subgoal_tac "rsb @ rdistinct rs (set rsb) @ RALTS rs # rsc \<leadsto>g*
+ rsb @ rdistinct rs (set rsb) @ rs @ rsc")
+ apply(subgoal_tac "rsb @ rdistinct rs (set rsb) @ rs @ rsc \<leadsto>g*
+rsb @ rdistinct rs (set rsb) @ rdistinct rs (set (rsb @ rdistinct rs (set rsb))) @ rsc")
+ apply (metis (full_types) append_Nil2 append_eq_appendI greal_trans list_dlist_union rdistinct_removes_all set_append)
+ apply (metis append.assoc append_Nil gstar_rdistinct_general middle_grewrites)
+ using gr_in_rstar grewrite.intros(2) grewrites_append by presburger
lemma grewrites_rev_append:
shows "rs1 \<leadsto>g* rs2 \<Longrightarrow> rs1 @ [x] \<leadsto>g* rs2 @ [x]"
@@ -717,7 +792,7 @@
shows "\<lbrakk>x \<notin> rset; x \<notin> set xs \<rbrakk> \<Longrightarrow> rdistinct (xs @ [x]) rset = rdistinct xs rset @ [x]"
by (simp add: concat_rdistinct_equality1)
-lemma grewrites_shape2:
+lemma grewrites_shape2_aux:
shows " RALTS rs \<notin> set rsb \<Longrightarrow>
rsb @
rdistinct (rs @ rsa)
@@ -767,6 +842,16 @@
apply (simp add: distinct_keeps_last)+
done
+lemma grewrites_shape2:
+ shows " RALTS rs \<notin> set rsb \<Longrightarrow>
+ rsb @
+ rdistinct (rs @ rsa)
+ (set rsb) \<leadsto>g* rflts rsb @
+ rdistinct rs (set rsb) @
+ rdistinct rsa (set rs \<union> set rsb \<union> {RALTS rs})"
+ apply (meson flts_gstar greal_trans grewrites.simps grewrites_shape2_aux grewritess_concat)
+ done
+
lemma rdistinct_add_acc:
shows "rset2 \<subseteq> set rsb \<Longrightarrow> rsb @ rdistinct rs rset \<leadsto>g* rsb @ rdistinct rs (rset \<union> rset2)"
apply(induct rs arbitrary: rsb rset rset2)
@@ -774,8 +859,8 @@
apply (case_tac "a \<in> rset")
apply simp
apply(case_tac "a \<in> rset2")
- apply simp
- apply (meson create_nonexistent_distinct_set gr_in_rstar greal_trans grewrite_variant1 in_mono)
+ apply simp
+ apply (simp add: more_distinct1)
apply simp
apply(drule_tac x = "rsb @ [a]" in meta_spec)
by (metis Un_insert_left append.assoc append_Cons append_Nil set_append sup.coboundedI1)
@@ -823,14 +908,13 @@
apply (metis frewrite_fun1 rdistinct_concat sup_ge2)
apply(simp)
apply(rule_tac x =
- "rsb @
+ "rflts rsb @
rdistinct rs (set rsb) @
rdistinct rsa (set rs \<union> set rsb \<union> {RALTS rs})" in exI)
apply(rule conjI)
prefer 2
using grewrites_shape2 apply force
- by (metis Un_insert_left frewrite_rd_grewrites_aux inf_sup_aci(5) insert_is_Un rdistinct.simps(2))
-
+ using frewrite_rd_grewrites_aux by blast
@@ -896,13 +980,7 @@
apply(induct rs2 rs3 rule: grewrites.induct)
apply simp
using grewrite_simpalts by presburger
-(*
-lemma frewrites_dB_wwo0_simp:
- shows "rdistinct rs1 {RZERO} \<leadsto>f* rdistinct rs2 {RZERO}
- \<Longrightarrow> rsimp (RALTS (rdistinct rs1 {})) = rsimp (RALTS (rdistinct rs2 {}))"
- sorry
-*)
@@ -942,12 +1020,9 @@
lemma simp_more_distinct:
shows "rsimp (rsimp_ALTs (rsa @ rs)) = rsimp (rsimp_ALTs (rsa @ (rdistinct rs (set rsa)))) "
-
-
+ oops
- sorry
-
lemma non_empty_list:
shows "a \<in> set as \<Longrightarrow> as \<noteq> []"
by (metis empty_iff empty_set)
@@ -1091,89 +1166,136 @@
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>
+lemma can_spill_lst:"\<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)) {})"
+
+ using flts_append rflts_spills_last rsimp_inner_idem4 by presburger
+
+
+
+
+
+lemma common_rewrites_equal:
+ shows "(rs1 \<leadsto>g* rs3) \<and> (rs2 \<leadsto>g* rs3) \<Longrightarrow> rsimp (rsimp_ALTs rs1 ) = rsimp (rsimp_ALTs rs2)"
+ using grewrites_simpalts by force
+
+
+lemma basic_regex_property1:
+ shows "rnullable r \<Longrightarrow> rsimp r \<noteq> RZERO"
+ sorry
+
+lemma basic_rsimp_SEQ_property1:
+ shows "rsimp_SEQ RONE r = r"
+ by (simp add: idiot)
+
+lemma basic_rsimp_SEQ_property3:
+ shows "rsimp_SEQ r RZERO = RZERO"
+ using rsimp_SEQ.elims by blast
+
+thm rsimp_SEQ.elims
+
+
+lemma basic_rsimp_SEQ_property2:
+ shows "\<lbrakk>r1 \<noteq> RZERO ; r1 \<noteq> RONE; r2 \<noteq> RZERO\<rbrakk> \<Longrightarrow>rsimp_SEQ r1 r2 = RSEQ r1 r2"
+ apply(case_tac r1)
+ apply simp+
+ apply (simp add: idiot2)
+ using idiot2 apply blast
+ using idiot2 apply auto[1]
+ using idiot2 by blast
+
+
+(*
+lemma rderssimp_same_rewrites_rder_induct1:
+ shows "\<lbrakk> ([rder x (rsimp r1)] \<leadsto>g* rs1) \<and> ([rder x r1] \<leadsto>g* rs1) ;
+ ([rder x (rsimp r2)] \<leadsto>g* rs2) \<and> ([rder x r2] \<leadsto>g* rs2) \<rbrakk> \<Longrightarrow>
+\<exists>rs3. ([rder x (rsimp (RSEQ r1 r2))] \<leadsto>g* rs3) \<and> ([rder x (RSEQ r1 r2)] \<leadsto>g* rs3) "
+ sorry
+
+lemma rderssimp_same_rewrites_rder_induct2:
+ shows "\<lbrakk> ([rder x (rsimp r1)] \<leadsto>g* rs1) \<and> ([rder x r1] \<leadsto>g* rs1) \<rbrakk> \<Longrightarrow>
+\<exists>rs3. ([rder x (rsimp (RSTAR r1))] \<leadsto>g* rs3) \<and> ([rder x (RSTAR r1)] \<leadsto>g* rs3) "
+ sorry
+
+lemma rderssimp_same_rewrites_rder_induct3:
+ shows "\<lbrakk> ([rder x (rsimp r1)] \<leadsto>g* rs1) \<and> ([rder x r1] \<leadsto>g* rs1) ;
+ ([rder x (rsimp r2)] \<leadsto>g* rs2) \<and> ([rder x r2] \<leadsto>g* rs2) \<rbrakk> \<Longrightarrow>
+\<exists>rs3. ([rder x (rsimp (RALT r1 r2))] \<leadsto>g* rs3) \<and> ([rder x (RALT r1 r2)] \<leadsto>g* rs3) "
+ sorry
+
+lemma rderssimp_same_rewrites_rder_induct4:
+ shows "\<lbrakk>\<forall>r \<in> set rs. \<exists> rsa. ([rder x (rsimp r)] \<leadsto>g* rsa ) \<and> ([rder x r] \<leadsto>g* rsa) \<rbrakk> \<Longrightarrow>
+\<exists>rsb. ([rder x (rsimp (RALTS rs))] \<leadsto>g* rsb) \<and> ([rder x (RALTS rs)] \<leadsto>g* rsb) "
+ sorry
+
+lemma rderssimp_same_rewrites_rder_base1:
+ shows "([rder x (rsimp RONE)] \<leadsto>g* [] ) \<and> ([rder x RONE] \<leadsto>g* [])"
+ by (simp add: gr_in_rstar grewrite.intros(1))
+
+lemma rderssimp_same_rewrites_rder_base2:
+ shows " ([rder x (rsimp RZERO)] \<leadsto>g* [] ) \<and> ([rder x RZERO] \<leadsto>g* [])"
+ using rderssimp_same_rewrites_rder_base1 by auto
+
+lemma rderssimp_same_rewrites_rder_base3:
+ shows " ([rder x (rsimp (RCHAR c))] \<leadsto>g* [] ) \<and> ([rder x (RCHAR c)] \<leadsto>g* [])"
+ sorry
+*)
+
+lemma inside_simp_seq_nullable:
+ shows
+"\<And>r1 r2.
+ \<lbrakk>rsimp (rder x (rsimp r1)) = rsimp (rder x r1); rsimp (rder x (rsimp r2)) = rsimp (rder x r2);
+ rnullable r1\<rbrakk>
+ \<Longrightarrow> rsimp (rder x (rsimp_SEQ (rsimp r1) (rsimp r2))) =
+ rsimp_ALTs (rdistinct (rflts [rsimp_SEQ (rsimp (rder x r1)) (rsimp r2), rsimp (rder x r2)]) {})"
+ apply(case_tac "rsimp r1 = RONE")
+ apply(simp)
+ apply(subst basic_rsimp_SEQ_property1)
+ apply (simp add: idem_after_simp1)
+ apply(case_tac "rsimp r1 = RZERO")
+
+ using basic_regex_property1 apply blast
+ apply(case_tac "rsimp r2 = RZERO")
+
+ apply (simp add: basic_rsimp_SEQ_property3)
+ apply(subst basic_rsimp_SEQ_property2)
+ apply simp+
+ apply(subgoal_tac "rnullable (rsimp r1)")
+ apply simp
+ using rsimp_idem apply presburger
sorry
-lemma last_elem_dup1:
- shows " a \<in> set as \<Longrightarrow> rsimp (RALTS (as @ [a] )) = rsimp (RALTS (as ))"
- apply simp
- apply(subgoal_tac "rsimp a \<in> set (map rsimp as)")
- prefer 2
- apply simp
- apply(case_tac "rsimp a")
- apply simp
+lemma inside_simp_removal:
+ shows " rsimp (rder x (rsimp r)) = rsimp (rder x r)"
+ apply(induct r)
+ apply simp+
+ apply(case_tac "rnullable r1")
+ 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:
- shows " a \<in> set as \<Longrightarrow> rsimp (rsimp_ALTs (as @ [a] )) = rsimp (rsimp_ALTs (as ))"
- apply(induct as rule: rev_induct)
- apply simp
- apply simp
- apply(subgoal_tac "xs \<noteq> []")
- prefer 2
-
-
-
-
- sorry
-
-lemma appeared_before_remove_later:
- shows "a \<in> set as \<Longrightarrow> rsimp (rsimp_ALTs ( as @ a # rs)) = rsimp (rsimp_ALTs (as @ rs))"
-and "a \<in> set as \<Longrightarrow> rsimp (rsimp_ALTs as ) = rsimp (rsimp_ALTs (as @ [a]))"
- apply(induct rs arbitrary: as)
- apply simp
-
-
- sorry
-
-lemma distinct_remove_later:
- shows "\<lbrakk>rder x a \<in> rder x ` set rsa\<rbrakk>
- \<Longrightarrow> rsimp (rsimp_ALTs (map (rder x) rsa @ rder x a # map (rder x) (rdistinct rs (insert a (set rsa))))) =
- rsimp (rsimp_ALTs (map (rder x) rsa @ map (rder x) (rdistinct rs (set rsa))))"
-
+ using inside_simp_seq_nullable apply blast
sorry
-lemma distinct_der_general:
- shows "rsimp (rsimp_ALTs (map (rder x) (rsa @ (rdistinct rs (set rsa))))) =
- rsimp ( rsimp_ALTs ((map (rder x) rsa)@(rdistinct (map (rder x) rs) (set (map (rder x) rsa)))) )"
- apply(induct rs arbitrary: rsa)
- apply simp
- apply(case_tac "a \<in> set rsa")
- apply(subgoal_tac "rder x a \<in> set (map (rder x) rsa)")
- apply simp
+lemma rders_simp_same_simpders:
+ shows "s \<noteq> [] \<Longrightarrow> rders_simp r s = rsimp (rders r s)"
+ apply(induct s rule: rev_induct)
apply simp
- apply(case_tac "rder x a \<notin> set (map (rder x) rsa)")
- apply(simp)
- apply(subst map_concat_cons)+
- apply(drule_tac x = "rsa @ [a]" in meta_spec)
+ apply(case_tac "xs = []")
apply simp
- apply(drule neg_removal_element_of)
- apply simp
- apply(subst distinct_remove_later)
- apply simp
- apply(drule_tac x = "rsa" in meta_spec)
- by blast
+ apply(simp add: rders_append rders_simp_append)
+ using inside_simp_removal by blast
-
+
lemma distinct_der:
- shows "rsimp (rsimp_ALTs (map (rder x) (rdistinct rs {}))) = rsimp ( rsimp_ALTs (rdistinct (map (rder x) rs) {}))"
- by (metis distinct_der_general list.simps(8) self_append_conv2 set_empty)
+ shows "rsimp (rsimp_ALTs (map (rder x) (rdistinct rs {}))) =
+ rsimp (rsimp_ALTs (rdistinct (map (rder x) rs) {}))"
+ by (metis grewrites_simpalts gstar_rdistinct inside_simp_removal rder_rsimp_ALTs_commute)
+
--- a/thys2/ClosedFormsBounds.thy Mon Apr 04 23:56:40 2022 +0100
+++ b/thys2/ClosedFormsBounds.thy Thu Apr 07 21:31:29 2022 +0100
@@ -208,7 +208,7 @@
\<le> (sum_list
(map rsize (RONE # rdistinct rs (insert RZERO (insert RONE noalts_set \<union> alts_set)))))")
apply (smt (verit, best) dual_order.trans insert_iff rrexp.distinct(15))
- apply (metis (no_types, opaque_lifting) add_Suc_right le_add_same_cancel2 list.simps(9) sum_list.Cons zero_le)
+ apply (metis (no_types, opaque_lifting) le_add_same_cancel2 list.simps(9) sum_list.Cons zero_le)
apply fastforce
apply fastforce
apply (metis Un_iff insert_absorb)