--- 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