--- a/thys2/ClosedForms.thy Sat Apr 09 19:17:42 2022 +0100
+++ b/thys2/ClosedForms.thy Tue Apr 12 15:51:35 2022 +0100
@@ -1280,7 +1280,7 @@
| "r3 \<leadsto> r4 \<Longrightarrow> RSEQ r1 r3 \<leadsto> RSEQ r1 r4"
| "r \<leadsto> r' \<Longrightarrow> (RALTS (rs1 @ [r] @ rs2)) \<leadsto> (RALTS (rs1 @ [r'] @ rs2))"
(*context rule for eliminating 0, alts--corresponds to the recursive call flts r::rs = r::(flts rs)*)
-| "RALTS (rsa @ [AZERO] @ rsb) \<leadsto> RALTS (rsa @ rsb)"
+| "RALTS (rsa @ [RZERO] @ rsb) \<leadsto> RALTS (rsa @ rsb)"
| "RALTS (rsa @ [RALTS rs1] @ rsb) \<leadsto> RALTS (rsa @ rs1 @ rsb)"
| "RALTS [] \<leadsto> RZERO"
| "RALTS [r] \<leadsto> r"
@@ -1468,9 +1468,13 @@
lemma interleave_aux1:
shows " RALT (RSEQ RZERO r1) r \<leadsto>* r"
apply(subgoal_tac "RSEQ RZERO r1 \<leadsto>* RZERO")
- apply (metis append_eq_Cons_conv hr_in_rstar hrewrite.intros(10) hrewrite.intros(7) hrewrites.simps)
+ apply(subgoal_tac "RALT (RSEQ RZERO r1) r \<leadsto>* RALT RZERO r")
+ apply (meson grewrite.intros(1) grewrite_ralts hreal_trans hrewrite.intros(10) hrewrites.simps)
+ using rs1 srewritescf_alt1 ss1 ss2 apply presburger
by (simp add: hr_in_rstar hrewrite.intros(1))
+
+
lemma rnullable_hrewrite:
shows "r1 \<leadsto> r2 \<Longrightarrow> rnullable r1 = rnullable r2"
sorry
@@ -1632,19 +1636,175 @@
| "r1 \<leadsto>o rs1 \<Longrightarrow> (RALT r1 r2) \<leadsto>o (rs1 @ [r2])"
-fun sflat :: "rrexp \<Rightarrow> rrexp list " where
- "sflat (RALTS (r # rs)) = sflat r @ rs"
-| "sflat (RALTS []) = []"
-| "sflat r = [r]"
+fun sflat_aux :: "rrexp \<Rightarrow> rrexp list " where
+ "sflat_aux (RALTS (r # rs)) = sflat_aux r @ rs"
+| "sflat_aux (RALTS []) = []"
+| "sflat_aux r = [r]"
+
+
+fun sflat :: "rrexp \<Rightarrow> rrexp" where
+ "sflat (RALTS (r # [])) = r"
+| "sflat (RALTS (r # rs)) = RALTS (sflat_aux r @ rs)"
+| "sflat r = r"
+
+inductive created_by_seq:: "rrexp \<Rightarrow> bool" where
+ "created_by_seq (RSEQ r1 r2) "
+| "created_by_seq r1 \<Longrightarrow> created_by_seq (RALT r1 r2)"
+
+(*Why \<and> rnullable case would be provable.....?*)
+lemma seq_der_shape:
+ shows "\<forall>r1 r2. \<exists>r3 r4. (rder c (RSEQ r1 r2) = RSEQ r3 r4 \<or> rder c (RSEQ r1 r2) = RALT r3 r4)"
+ by (meson rder.simps(5))
+
+lemma alt_der_shape:
+ shows "\<forall>rs. \<exists> rs'. (rder c (RALTS rs)) = RALTS (map (rder c) rs)"
+ by force
+
+lemma seq_ders_shape1:
+ shows "\<forall>r1 r2. \<exists>r3 r4. (rders (RSEQ r1 r2) s) = RSEQ r3 r4 \<or> (rders (RSEQ r1 r2) s) = RALT r3 r4"
+ apply(induct s rule: rev_induct)
+ apply auto[1]
+ apply(rule allI)+
+ apply(subst rders_append)+
+ apply(subgoal_tac " \<exists>r3 r4. rders (RSEQ r1 r2) xs = RSEQ r3 r4 \<or> rders (RSEQ r1 r2) xs = RALT r3 r4 ")
+ apply(erule exE)+
+ apply(erule disjE)
+ apply simp+
+ done
+
+
+lemma seq_ders_shape2:
+ shows "rders (RSEQ r1 r2) s = RALTS (ra # rb # rs) \<Longrightarrow> rs = []"
+ using seq_ders_shape1
+ by (metis list.inject rrexp.distinct(25) rrexp.inject(3))
+
+lemma created_by_seq_der:
+ shows "created_by_seq r \<Longrightarrow> created_by_seq (rder c r)"
+ apply(induct r)
+ apply simp+
+
+ using created_by_seq.cases apply blast
+
+ apply (meson created_by_seq.cases rrexp.distinct(19) rrexp.distinct(21))
+ apply (metis created_by_seq.simps rder.simps(5))
+ apply (smt (verit, ccfv_threshold) created_by_seq.simps list.set_intros(1) list.simps(8) list.simps(9) rder.simps(4) rrexp.distinct(25) rrexp.inject(3))
+ using created_by_seq.intros(1) by force
+
+lemma createdbyseq_left_creatable:
+ shows "created_by_seq (RALT r1 r2) \<Longrightarrow> created_by_seq r1"
+ using created_by_seq.cases by blast
+
+
+
+lemma recursively_derseq:
+ shows " created_by_seq (rders (RSEQ r1 r2) s)"
+ apply(induct s rule: rev_induct)
+ apply simp
+ using created_by_seq.intros(1) apply force
+ apply(subgoal_tac "created_by_seq (rders (RSEQ r1 r2) (xs @ [x]))")
+ apply blast
+ apply(subst rders_append)
+ apply(subgoal_tac "\<exists>r3 r4. rders (RSEQ r1 r2) xs = RSEQ r3 r4 \<or>
+ rders (RSEQ r1 r2) xs = RALT r3 r4")
+ prefer 2
+ using seq_ders_shape1 apply presburger
+ apply(erule exE)+
+ apply(erule disjE)
+ apply(subgoal_tac "created_by_seq (rders (RSEQ r3 r4) [x])")
+ apply presburger
+ apply simp
+ using created_by_seq.intros(1) created_by_seq.intros(2) apply presburger
+ apply simp
+ apply(subgoal_tac "created_by_seq r3")
+ prefer 2
+ using createdbyseq_left_creatable apply blast
+ using created_by_seq.intros(2) created_by_seq_der by blast
-lemma softrewrite_flat:
- shows "r \<leadsto>o sflat r"
- oops
+
+lemma recursively_derseq1:
+ shows "r = rders (RSEQ r1 r2) s \<Longrightarrow> created_by_seq r"
+ using recursively_derseq by blast
+
+lemma recursively_derseq2:
+ shows "r = rders (RSEQ r1 r2) s \<Longrightarrow> \<exists>r1 r2. r = RSEQ r1 r2 \<or> (r = RALT r1 r2 \<and> created_by_seq r1) "
+ by (meson created_by_seq.cases recursively_derseq)
+
+lemma recursively_derseq3:
+ shows "created_by_seq r \<Longrightarrow> \<exists>r1 r2. r = RSEQ r1 r2 \<or> (r = RALT r1 r2 \<and> created_by_seq r1) "
+ by (meson created_by_seq.cases recursively_derseq)
+
+lemma createdbyseq_prop1:
+ shows "created_by_seq (RALTS xs) \<Longrightarrow> \<exists> ra rb. xs = [ra, rb]"
+ by (metis created_by_seq.cases rrexp.inject(3) rrexp.simps(30))
+
+
+lemma sfau_head:
+ shows " created_by_seq r \<Longrightarrow> \<exists>ra rb rs. sflat_aux r = RSEQ ra rb # rs"
+ apply(induction r rule: created_by_seq.induct)
+ apply simp
+ by fastforce
+
+
+
+
+lemma sfaux_eq10:
+ shows "created_by_seq r3 \<Longrightarrow>
+rs \<noteq> [] \<Longrightarrow> sflat (RALTS ((map (rder c) (sflat_aux r3)) @ (map (rder c) rs))) =
+RALTS (sflat_aux (rder c r3) @ (map (rder c ) rs) )"
+ apply(induction r3 arbitrary: rs rule: created_by_seq.induct)
+ apply simp
+ apply(case_tac "rnullable r1")
+ apply simp
+
+ apply (metis append_Cons list.exhaust map_is_Nil_conv self_append_conv2 sflat.simps(2) sflat_aux.simps(1) sflat_aux.simps(6))
+ apply simp
+
+ apply (metis Nil_is_map_conv append_Cons append_Nil list.exhaust sflat.simps(2) sflat_aux.simps(6))
+ apply simp
+ by force
-lemma sflat_der:
- shows "sflat r1 = sflat r2 \<Longrightarrow> sflat (rder c r1) = sflat (rder c r2)"
- apply(case_tac r1 )
+lemma sfaux_keeps_tail:
+ shows "created_by_seq r3 \<Longrightarrow>
+ sflat_aux (RALTS (map (rder c) (sflat_aux r3) @ xs )) =
+ sflat_aux (RALTS (map (rder c) (sflat_aux r3))) @ xs "
+ using sfau_head by fastforce
+
+
+
+lemma sfaux_eq00:
+ shows "created_by_seq r3 \<Longrightarrow>
+ sflat_aux (RALTS ((map (rder c) (sflat_aux r3)) @ (map (rder c) rs))) =
+ (sflat_aux (rder c r3) @ (map (rder c ) rs) )"
+ apply(induct rs rule: rev_induct)
+ apply simp
+ apply (smt (verit, del_insts) append_Cons created_by_seq.simps list.distinct(1) list.simps(9) map_append rder.simps(4) rrexp.inject(3) self_append_conv self_append_conv2 sfau_head sfaux_eq10 sflat_aux.simps(1) sflat_aux.simps(6))
+ apply simp
+ apply(subst sfaux_keeps_tail)
+ apply simp
+ apply(subst (asm) sfaux_keeps_tail)
+ apply simp+
+ done
+
+
+lemma sfaux_eq1:
+ shows "created_by_seq r3 \<Longrightarrow> sflat (RALTS ((map (rder c) (sflat_aux r3)) @ [rder c r4])) = RALTS (sflat_aux (rder c r3) @ [rder c r4] )"
+ by (metis (no_types, lifting) list.distinct(1) list.simps(9) map_append map_concat_cons self_append_conv sfaux_eq10)
+
+lemma sflat_seq_induct:
+ shows "sflat (rder c (sflat (rders (RSEQ r1 r2) s) )) = sflat (rders (RSEQ r1 r2) (s @ [c]))"
+ apply(subst rders_append)
+ apply(case_tac "rders (RSEQ r1 r2) s ")
+ prefer 6
+ apply simp+
+ apply(subgoal_tac "\<exists>r3 r4. x5 = [r3, r4]")
+ apply(erule exE)+
+ apply(subgoal_tac "sflat (rder c (sflat (RALT r3 r4))) = sflat (RALTS (map (rder c) [r3, r4]))")
+ apply meson
+ apply simp
+
+ apply (metis createdbyseq_left_creatable recursively_derseq sfaux_eq1)
+ by (metis created_by_seq.simps recursively_derseq rrexp.distinct(25) rrexp.inject(3))
@@ -1653,69 +1813,81 @@
(map (rders r2) (vsuf s r1))) )"
apply(induct s rule: rev_induct)
apply simp
- apply(subst rders_append)
- sorry
+ apply(subst rders_append)+
-lemma seq_sflat1:
- shows "sflat ( RALTS ( (RSEQ (rders r1 (s @ [c])) r2) #
- (map (rders r2) (vsuf (s @ [c]) r1))
- ) ) = sflat (rders (RSEQ r1 r2) (s @ [c]))"
- sorry
-
-
-lemma seq_sflat:
- shows "sflat ( RALTS ( (RSEQ (rders r1 (s @ [c])) r2) #
- (map (rders r2) (vsuf (s @ [c]) r1))
- ) ) = sflat ( rder x (RALTS ( (RSEQ (rders r1 s) r2) #
- (map (rders r2) (vsuf s r1))
- )) )"
sorry
-lemma sflat_elemnum:
- shows "sflat (RALTS [a1, a2, a3]) = [a1, a2, a3]"
- sorry
+lemma vsuf_prop1:
+ shows "vsuf (xs @ [x]) r = (if (rnullable (rders r xs))
+ then [x] # (map (\<lambda>s. s @ [x]) (vsuf xs r) )
+ else (map (\<lambda>s. s @ [x]) (vsuf xs r)) )
+ "
+ apply(induct xs arbitrary: r)
+ apply simp
+ apply(case_tac "rnullable r")
+ apply simp
+ apply simp
+ done
-lemma sflat_emptyalts:
- shows "sflat (RALTS xs) = [] \<Longrightarrow> xs = []"
- using sflat.elims by auto
+fun breakHead :: "rrexp list \<Rightarrow> rrexp list" where
+ "breakHead [] = [] "
+| "breakHead (RALT r1 r2 # rs) = r1 # r2 # rs"
+| "breakHead (r # rs) = r # rs"
+
+
+lemma sfau_idem_der:
+ shows "created_by_seq r \<Longrightarrow> sflat_aux (rder c r) = breakHead (map (rder c) (sflat_aux r))"
+ apply(induct rule: created_by_seq.induct)
+ apply simp+
+ using sfau_head by fastforce
-lemma ralt_sflat_gte2:
- shows "\<exists>ra rb rsc. sflat (RALT r1 r2) = ra # rb # rsc"
- apply(case_tac r1)
- apply simp+
+lemma vsuf_compose1:
+ shows " \<not> rnullable (rders r1 xs)
+ \<Longrightarrow> map (rder x \<circ> rders r2) (vsuf xs r1) = map (rders r2) (vsuf (xs @ [x]) r1)"
+ apply(subst vsuf_prop1)
+ apply simp
+ by (simp add: rders_append)
- oops
+
+
-lemma sflat_singleton:
- shows "sflat (RALTS xs) = [a] \<Longrightarrow> xs = [a]"
- apply(case_tac xs)
+lemma seq_sfau0:
+ shows "sflat_aux (rders (RSEQ r1 r2) s) = (RSEQ (rders r1 s) r2) #
+ (map (rders r2) (vsuf s r1)) "
+ apply(induct s rule: rev_induct)
apply simp
- apply(case_tac list)
+ apply(subst rders_append)+
+ apply(subgoal_tac "created_by_seq (rders (RSEQ r1 r2) xs)")
+ prefer 2
+ using recursively_derseq1 apply blast
+ apply simp
+ apply(subst sfau_idem_der)
+
+ apply blast
+ apply(case_tac "rnullable (rders r1 xs)")
apply simp
+ apply(subst vsuf_prop1)
apply simp
- oops
+ apply (simp add: rders_append)
+ apply simp
+ using vsuf_compose1 by blast
+
+
+
+
+
+
+
+
thm sflat.elims
-lemma sflat_ralts:
- shows "sflat (RALTS xs) = sflat (RALTS xs')
- \<Longrightarrow> rsimp (RALTS xs) = rsimp (RALTS xs')"
- apply(induct xs)
-
- apply(case_tac xs)
- apply simp
- apply (metis list.simps(8) rdistinct.simps(1) rflts.simps(1) rsimp_ALTs.simps(1) sflat_emptyalts)
- apply(case_tac list)
- apply simp
- apply
- sledgehammer
-
lemma sflat_rsimpeq:
- shows "sflat r1 = sflat r2 \<Longrightarrow> rsimp r1 = rsimp r2"
+ shows "sflat_aux r1 = sflat_aux r2 \<Longrightarrow> rsimp r1 = rsimp r2"
apply(cases r1 )
apply(cases r2)
apply simp+
@@ -1723,8 +1895,7 @@
apply simp
apply(case_tac list)
apply simp
- apply(case_tac lista)
- apply simp
+
sorry
@@ -1734,10 +1905,14 @@
lemma seq_closed_form_general:
shows "rsimp (rders (RSEQ r1 r2) s) =
rsimp ( (RALTS ( (RSEQ (rders r1 s) r2 # (map (rders r2) (vsuf s r1))))))"
- apply(subgoal_tac "sflat (rders (RSEQ r1 r2) s) = sflat (RALTS ( (RSEQ (rders r1 s) r2 # (map (rders r2) (vsuf s r1)))))")
+ apply(case_tac "s \<noteq> []")
+ apply(subgoal_tac "sflat_aux (rders (RSEQ r1 r2) s) = sflat_aux (RALTS ( (RSEQ (rders r1 s) r2 # (map (rders r2) (vsuf s r1)))))")
using sflat_rsimpeq apply blast
- by (simp add: seq_sflat0)
+ using seq_sfau0 apply blast
+ apply simp
+ by (metis idem_after_simp1 rsimp.simps(1))
+
lemma seq_closed_form_aux1:
shows "rsimp ( (RALTS ( (RSEQ (rders r1 s) r2 # (map (rders r2) (vsuf s r1)))))) =
rsimp ( (RALTS ( (RSEQ (rders_simp r1 s) r2 # (map (rders r2) (vsuf s r1))))))"
@@ -1789,7 +1964,6 @@
apply (metis idem_after_simp1 rsimp.simps(1))
apply(subgoal_tac " s \<noteq> []")
using rders_simp_same_simpders rsimp_idem seq_closed_form_aux1 seq_closed_form_aux2 seq_closed_form_general apply presburger
-
by fastforce