# HG changeset patch # User Chengsong # Date 1649775095 -3600 # Node ID 72edbac05c59755571c5dc58a7eed6ae24421b73 # Parent 15f02ec4d9fe25d5d06dc5c024fa2bec4483b6b4 central lemma for seqclosedforms diff -r 15f02ec4d9fe -r 72edbac05c59 thys2/ClosedForms.thy --- 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 \ r4 \ RSEQ r1 r3 \ RSEQ r1 r4" | "r \ r' \ (RALTS (rs1 @ [r] @ rs2)) \ (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) \ RALTS (rsa @ rsb)" +| "RALTS (rsa @ [RZERO] @ rsb) \ RALTS (rsa @ rsb)" | "RALTS (rsa @ [RALTS rs1] @ rsb) \ RALTS (rsa @ rs1 @ rsb)" | "RALTS [] \ RZERO" | "RALTS [r] \ r" @@ -1468,9 +1468,13 @@ lemma interleave_aux1: shows " RALT (RSEQ RZERO r1) r \* r" apply(subgoal_tac "RSEQ RZERO r1 \* 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 \* 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 \ r2 \ rnullable r1 = rnullable r2" sorry @@ -1632,19 +1636,175 @@ | "r1 \o rs1 \ (RALT r1 r2) \o (rs1 @ [r2])" -fun sflat :: "rrexp \ rrexp list " where - "sflat (RALTS (r # rs)) = sflat r @ rs" -| "sflat (RALTS []) = []" -| "sflat r = [r]" +fun sflat_aux :: "rrexp \ rrexp list " where + "sflat_aux (RALTS (r # rs)) = sflat_aux r @ rs" +| "sflat_aux (RALTS []) = []" +| "sflat_aux r = [r]" + + +fun sflat :: "rrexp \ rrexp" where + "sflat (RALTS (r # [])) = r" +| "sflat (RALTS (r # rs)) = RALTS (sflat_aux r @ rs)" +| "sflat r = r" + +inductive created_by_seq:: "rrexp \ bool" where + "created_by_seq (RSEQ r1 r2) " +| "created_by_seq r1 \ created_by_seq (RALT r1 r2)" + +(*Why \ rnullable case would be provable.....?*) +lemma seq_der_shape: + shows "\r1 r2. \r3 r4. (rder c (RSEQ r1 r2) = RSEQ r3 r4 \ rder c (RSEQ r1 r2) = RALT r3 r4)" + by (meson rder.simps(5)) + +lemma alt_der_shape: + shows "\rs. \ rs'. (rder c (RALTS rs)) = RALTS (map (rder c) rs)" + by force + +lemma seq_ders_shape1: + shows "\r1 r2. \r3 r4. (rders (RSEQ r1 r2) s) = RSEQ r3 r4 \ (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 " \r3 r4. rders (RSEQ r1 r2) xs = RSEQ r3 r4 \ 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) \ 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 \ 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) \ 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 "\r3 r4. rders (RSEQ r1 r2) xs = RSEQ r3 r4 \ + 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 \o sflat r" - oops + +lemma recursively_derseq1: + shows "r = rders (RSEQ r1 r2) s \ created_by_seq r" + using recursively_derseq by blast + +lemma recursively_derseq2: + shows "r = rders (RSEQ r1 r2) s \ \r1 r2. r = RSEQ r1 r2 \ (r = RALT r1 r2 \ created_by_seq r1) " + by (meson created_by_seq.cases recursively_derseq) + +lemma recursively_derseq3: + shows "created_by_seq r \ \r1 r2. r = RSEQ r1 r2 \ (r = RALT r1 r2 \ created_by_seq r1) " + by (meson created_by_seq.cases recursively_derseq) + +lemma createdbyseq_prop1: + shows "created_by_seq (RALTS xs) \ \ 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 \ \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 \ +rs \ [] \ 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 \ sflat (rder c r1) = sflat (rder c r2)" - apply(case_tac r1 ) +lemma sfaux_keeps_tail: + shows "created_by_seq r3 \ + 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 \ + 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 \ 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 "\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 (\s. s @ [x]) (vsuf xs r) ) + else (map (\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) = [] \ xs = []" - using sflat.elims by auto +fun breakHead :: "rrexp list \ 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 \ 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 "\ra rb rsc. sflat (RALT r1 r2) = ra # rb # rsc" - apply(case_tac r1) - apply simp+ +lemma vsuf_compose1: + shows " \ rnullable (rders r1 xs) + \ map (rder x \ 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] \ 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') - \ 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 \ rsimp r1 = rsimp r2" + shows "sflat_aux r1 = sflat_aux r2 \ 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 \ []") + 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 \ []") using rders_simp_same_simpders rsimp_idem seq_closed_form_aux1 seq_closed_form_aux2 seq_closed_form_general apply presburger - by fastforce