--- a/thys2/BasicIdentities.thy Wed Apr 13 18:57:24 2022 +0100
+++ b/thys2/BasicIdentities.thy Wed Apr 13 22:20:08 2022 +0100
@@ -53,12 +53,24 @@
(if x \<in> acc then rdistinct xs acc
else x # (rdistinct xs ({x} \<union> acc)))"
+lemma rdistinct1:
+ assumes "a \<in> acc"
+ shows "a \<notin> set (rdistinct rs acc)"
+ using assms
+ apply(induct rs arbitrary: acc a)
+ apply(auto)
+ done
+
+
lemma rdistinct_does_the_job:
shows "distinct (rdistinct rs s)"
apply(induct rs arbitrary: s)
- apply simp
+ apply simp
apply simp
- sorry
+ apply(auto)
+ by (simp add: rdistinct1)
+
+
lemma rdistinct_concat:
@@ -110,24 +122,18 @@
done
-lemma rdistinct_concat_general:
- shows "rdistinct (rs1 @ rs2) {} = (rdistinct rs1 {}) @ (rdistinct rs2 (set rs1))"
- sorry
+
+
+
+lemma rdistinct_set_equality1:
+ shows "set (rdistinct rs acc) = set rs - acc"
+ apply(induct rs acc rule: rdistinct.induct)
+ apply(auto)
+ done
lemma rdistinct_set_equality:
shows "set (rdistinct rs {}) = set rs"
- sorry
-
-lemma distinct_once_enough:
- shows "rdistinct (rs @ rsa) {} = rdistinct (rdistinct rs {} @ rsa) {}"
- apply(subgoal_tac "distinct (rdistinct rs {})")
- apply(subgoal_tac
-" rdistinct (rdistinct rs {} @ rsa) {} = rdistinct rs {} @ (rdistinct rsa (set rs))")
- apply(simp only:)
- using rdistinct_concat_general apply blast
- apply (simp add: distinct_rdistinct_append rdistinct_set_equality)
- by (simp add: rdistinct_does_the_job)
-
+ by (simp add: rdistinct_set_equality1)
fun rflts :: "rrexp list \<Rightarrow> rrexp list"
@@ -429,14 +435,97 @@
+fun
+ RL :: "rrexp \<Rightarrow> string set"
+where
+ "RL (RZERO) = {}"
+| "RL (RONE) = {[]}"
+| "RL (RCHAR c) = {[c]}"
+| "RL (RSEQ r1 r2) = (RL r1) ;; (RL r2)"
+| "RL (RALTS rs) = (\<Union> (set (map RL rs)))"
+| "RL (RSTAR r) = (RL r)\<star>"
+
+
+lemma RL_rnullable:
+ shows "rnullable r = ([] \<in> RL r)"
+ apply(induct r)
+ apply(auto simp add: Sequ_def)
+ done
+
+lemma RL_rder:
+ shows "RL (rder c r) = Der c (RL r)"
+ apply(induct r)
+ apply(auto simp add: Sequ_def Der_def)
+ apply (metis append_Cons)
+ using RL_rnullable apply blast
+ apply (metis append_eq_Cons_conv)
+ apply (metis append_Cons)
+ apply (metis RL_rnullable append_eq_Cons_conv)
+ apply (metis Star.step append_Cons)
+ using Star_decomp by auto
+
+
+
+
+lemma RL_rsimp_RSEQ:
+ shows "RL (rsimp_SEQ r1 r2) = (RL r1 ;; RL r2)"
+ apply(induct r1 r2 rule: rsimp_SEQ.induct)
+ apply(simp_all)
+ done
+
+lemma RL_rsimp_RALTS:
+ shows "RL (rsimp_ALTs rs) = (\<Union> (set (map RL rs)))"
+ apply(induct rs rule: rsimp_ALTs.induct)
+ apply(simp_all)
+ done
+
+lemma RL_rsimp_rdistinct:
+ shows "(\<Union> (set (map RL (rdistinct rs {})))) = (\<Union> (set (map RL rs)))"
+ apply(auto)
+ apply (metis rdistinct_set_equality)
+ by (metis rdistinct_set_equality)
+
+lemma RL_rsimp_rflts:
+ shows "(\<Union> (set (map RL (rflts rs)))) = (\<Union> (set (map RL rs)))"
+ apply(induct rs rule: rflts.induct)
+ apply(simp_all)
+ done
+
+lemma RL_rsimp:
+ shows "RL r = RL (rsimp r)"
+ apply(induct r rule: rsimp.induct)
+ apply(auto simp add: Sequ_def RL_rsimp_RSEQ)
+ using RL_rsimp_RALTS RL_rsimp_rdistinct RL_rsimp_rflts apply auto[1]
+ by (smt (verit, del_insts) RL_rsimp_RALTS RL_rsimp_rdistinct RL_rsimp_rflts UN_E image_iff list.set_map)
+
+lemma RL_rders:
+ shows "RL (rders_simp r s) = RL (rders r s)"
+ apply(induct s arbitrary: r rule: rev_induct)
+ apply(simp)
+ apply(simp add: rders_append rders_simp_append)
+ apply(subst RL_rsimp[symmetric])
+ using RL_rder by force
+
+
+lemma der_simp_nullability:
+ shows "rnullable r = rnullable (rsimp r)"
+ using RL_rnullable RL_rsimp by auto
+
lemma ders_simp_nullability:
shows "rnullable (rders r s) = rnullable (rders_simp r s)"
- sorry
+ apply(induct s arbitrary: r rule: rev_induct)
+ apply(simp)
+ apply(simp add: rders_append rders_simp_append)
+ apply(simp only: RL_rnullable)
+ apply(simp only: RL_rder)
+ apply(subst RL_rsimp[symmetric])
+ apply(simp only: RL_rder)
+ by (simp add: RL_rders)
-lemma der_simp_nullability:
- shows "rnullable r = rnullable (rsimp r)"
- sorry
+
+
+
lemma first_elem_seqder:
@@ -459,21 +548,6 @@
-lemma seq_ders_closed_form1:
- shows "\<exists>Ss. rders_simp (RSEQ r1 r2) [c] = rsimp (RALTS ((RSEQ (rders_simp r1 [c]) r2) #
-(map ( rders_simp r2 ) Ss)))"
- apply(case_tac "rnullable r1")
- apply(subgoal_tac " rders_simp (RSEQ r1 r2) [c] =
-rsimp (RALTS ((RSEQ (rders_simp r1 [c]) r2) # (map (rders_simp r2) [[c]])))")
- prefer 2
- apply (simp add: rsimp_idem)
- apply(rule_tac x = "[[c]]" in exI)
- apply simp
- apply(subgoal_tac " rders_simp (RSEQ r1 r2) [c] =
-rsimp (RALTS ((RSEQ (rders_simp r1 [c]) r2) # (map (rders_simp r2) [])))")
- apply blast
- apply(simp add: rsimp_idem)
- sorry
@@ -632,10 +706,26 @@
apply simp
by (metis good1.cases good1.intros(1) goods.cases list.distinct(1) list.inject list.set_intros(2) rrexp.distinct(15) rrexp.distinct(29) rrexp.distinct(7) rrexp.inject(3) rrexp.simps(26) rrexp.simps(30))
+lemma rsimp_good10:
+ shows "good1 (rsimp r)"
+ apply(induct r)
+ apply simp
+
+ apply (simp add: good1.intros(2))
+ apply simp
+
+ apply (simp add: good1.intros(3))
+
+ apply (simp add: good1.intros(4))
+ sledgehammer
+
+ sorry
+
lemma rsimp_good1:
shows "rsimp r = r1 \<Longrightarrow> good1 r1"
+ using rsimp_good10 by blast
- sorry
+
lemma rsimp_no_dup:
shows "rsimp r = RALTS rs \<Longrightarrow> distinct rs"
@@ -740,6 +830,22 @@
+lemma rdistinct_concat_general:
+ shows "rdistinct (rs1 @ rs2) {} = (rdistinct rs1 {}) @ (rdistinct rs2 (set rs1))"
+
+ sorry
+
+lemma distinct_once_enough:
+ shows "rdistinct (rs @ rsa) {} = rdistinct (rdistinct rs {} @ rsa) {}"
+ apply(subgoal_tac "distinct (rdistinct rs {})")
+ apply(subgoal_tac
+" rdistinct (rdistinct rs {} @ rsa) {} = rdistinct rs {} @ (rdistinct rsa (set rs))")
+ apply(simp only:)
+ using rdistinct_concat_general apply blast
+ apply (simp add: distinct_rdistinct_append rdistinct_set_equality)
+ by (simp add: rdistinct_does_the_job)
+
+
lemma simp_flatten:
shows "rsimp (RALTS ((RALTS rsa) # rsb)) = rsimp (RALTS (rsa @ rsb))"
apply simp
--- a/thys2/ClosedForms.thy Wed Apr 13 18:57:24 2022 +0100
+++ b/thys2/ClosedForms.thy Wed Apr 13 22:20:08 2022 +0100
@@ -1329,28 +1329,52 @@
shows "\<lbrakk>r1 \<leadsto>* r2; r3 \<leadsto>* r4\<rbrakk> \<Longrightarrow> RSEQ r1 r3 \<leadsto>* RSEQ r2 r4"
by (meson hreal_trans hrewrites_seq_context hrewrites_seq_context2)
+lemma hrewrite_simpeq:
+ shows "r1 \<leadsto> r2 \<Longrightarrow> rsimp r1 = rsimp r2"
+ apply(induct rule: hrewrite.induct)
+ apply simp+
+ apply (simp add: basic_rsimp_SEQ_property3)
+ apply (simp add: basic_rsimp_SEQ_property1)
+ using rsimp.simps(1) apply presburger
+ apply simp+
+ using flts_middle0 apply force
+ using simp_flatten3 apply presburger
+ apply simp+
+ apply (simp add: idem_after_simp1)
+ using grewrite.intros(4) grewrite_equal_rsimp by presburger
+
lemma hrewrites_simpeq:
shows "r1 \<leadsto>* r2 \<Longrightarrow> rsimp r1 = rsimp r2"
- sorry
-
-lemma distinct_grewrites_subgoal1:
- shows " \<And>rs1 rs2 rs3 a list.
- \<lbrakk>rs1 \<leadsto>g* [a]; RALTS rs1 \<leadsto>* a; [a] \<leadsto>g rs3; rs2 = [a]; list = []\<rbrakk> \<Longrightarrow> RALTS rs1 \<leadsto>* rsimp_ALTs rs3"
- (* apply (smt (z3) append.left_neutral append.right_neutral append_Cons grewrite.simps grewrite_singleton hrewrite.intros(10) hrewrite.intros(9) hrewrites.simps list.inject r_finite1 rsimp_ALTs.elims rsimp_ALTs.simps(2) rsimp_alts_equal)*)
- sorry
+ apply(induct rule: hrewrites.induct)
+ apply simp
+ apply(subgoal_tac "rsimp r2 = rsimp r3")
+ apply auto[1]
+ using hrewrite_simpeq by presburger
+
lemma grewrite_ralts:
shows "rs \<leadsto>g rs' \<Longrightarrow> RALTS rs \<leadsto>* RALTS rs'"
by (smt (verit) grewrite_cases_middle hr_in_rstar hrewrite.intros(11) hrewrite.intros(7) hrewrite.intros(8))
-
-
-
lemma grewrites_ralts:
shows "rs \<leadsto>g* rs' \<Longrightarrow> RALTS rs \<leadsto>* RALTS rs'"
- apply(induct rs rs' rule: grewrites.induct)
+ apply(induct rule: grewrites.induct)
apply simp
using grewrite_ralts hreal_trans by blast
+
+
+lemma distinct_grewrites_subgoal1:
+ shows "
+ \<lbrakk>rs1 \<leadsto>g* [a]; RALTS rs1 \<leadsto>* a; [a] \<leadsto>g rs3\<rbrakk> \<Longrightarrow> RALTS rs1 \<leadsto>* rsimp_ALTs rs3"
+ apply(subgoal_tac "RALTS rs1 \<leadsto>* RALTS rs3")
+ apply (metis hrewrite.intros(10) hrewrite.intros(9) rs2 rsimp_ALTs.cases rsimp_ALTs.simps(1) rsimp_ALTs.simps(2) rsimp_ALTs.simps(3))
+ apply(subgoal_tac "rs1 \<leadsto>g* rs3")
+ using grewrites_ralts apply blast
+ using grewrites.intros(2) by presburger
+
+
+
+
lemma grewrites_ralts_rsimpalts:
@@ -1477,24 +1501,51 @@
lemma rnullable_hrewrite:
shows "r1 \<leadsto> r2 \<Longrightarrow> rnullable r1 = rnullable r2"
- sorry
+ apply(induct rule: hrewrite.induct)
+ apply simp+
+ apply blast
+ apply simp+
+ done
lemma interleave1:
shows "r \<leadsto> r' \<Longrightarrow> rder c r \<leadsto>* rder c r'"
apply(induct r r' rule: hrewrite.induct)
-
-
apply (simp add: hr_in_rstar hrewrite.intros(1))
apply (metis (no_types, lifting) basic_rsimp_SEQ_property3 list.simps(8) list.simps(9) rder.simps(1) rder.simps(5) rdistinct.simps(1) rflts.simps(1) rflts.simps(2) rsimp.simps(1) rsimp.simps(2) rsimp.simps(3) rsimp_ALTs.simps(1) simp_hrewrites)
apply simp
apply(subst interleave_aux1)
apply simp
apply(case_tac "rnullable r1")
-
- sorry
-
+ apply simp
+
+ apply (simp add: hrewrites_seq_context rnullable_hrewrite srewritescf_alt1 ss1 ss2)
+
+ apply (simp add: hrewrites_seq_context rnullable_hrewrite)
+ apply(case_tac "rnullable r1")
+ apply simp
+
+ using hr_in_rstar hrewrites_seq_context2 srewritescf_alt1 ss1 ss2 apply presburger
+ apply simp
+ using hr_in_rstar hrewrites_seq_context2 apply blast
+ apply simp
+ using hrewrites_alts apply auto[1]
+ apply simp
+ using grewrite.intros(1) grewrite_append grewrite_ralts apply auto[1]
+ apply simp
+ apply (simp add: grewrite.intros(2) grewrite_append grewrite_ralts)
+ apply (simp add: hr_in_rstar hrewrite.intros(9))
+ apply (simp add: hr_in_rstar hrewrite.intros(10))
+ apply simp
+ using hrewrite.intros(11) by auto
+
+lemma interleave_star1:
+ shows "r \<leadsto>* r' \<Longrightarrow> rder c r \<leadsto>* rder c r'"
+ apply(induct rule : hrewrites.induct)
+ apply simp
+ by (meson hreal_trans interleave1)
+
lemma inside_simp_removal:
@@ -1507,9 +1558,11 @@
using inside_simp_seq_nullable apply blast
apply simp
apply (smt (verit, del_insts) basic_rsimp_SEQ_property2 basic_rsimp_SEQ_property3 der_simp_nullability rder.simps(1) rder.simps(5) rnullable.simps(2) rsimp.simps(1) rsimp_SEQ.simps(1) rsimp_idem)
-
+ apply(subgoal_tac "rder x (RALTS xa) \<leadsto>* rder x (rsimp (RALTS xa))")
+ using hrewrites_simpeq apply presburger
+ using interleave_star1 simp_hrewrites apply presburger
+ by simp
- sorry
@@ -2091,7 +2144,7 @@
shows "rsimp (RALT a b) = rsimp (RALTS ((hflat_aux a) @ (hflat_aux b)))"
apply(subgoal_tac "[a, b] \<leadsto>g* hflat_aux a @ hflat_aux b")
using grewrites_equal_rsimp apply presburger
- sorry
+ by (metis append.right_neutral greal_trans grewrites_cons hflat_aux_grewrites)
lemma hfau_rsimpeq2:
@@ -2221,16 +2274,5 @@
using star_closed_form4 star_closed_form5 star_closed_form6 star_closed_form8 by presburger
-lemma simp_helps_der_pierce:
- shows " rsimp
- (rder x
- (rsimp_ALTs rs)) =
- rsimp
- (rsimp_ALTs
- (map (rder x )
- rs
- )
- )"
- sorry
end
\ No newline at end of file