# HG changeset patch # User Chengsong # Date 1648851460 -3600 # Node ID 56837303ce61cfa065a7af3245f2e22af54a619c # Parent 10fd25fba2bade1e37b514d585fb5cfef2aa8900 hello diff -r 10fd25fba2ba -r 56837303ce61 thys2/BasicIdentities.thy --- a/thys2/BasicIdentities.thy Wed Mar 30 11:18:51 2022 +0100 +++ b/thys2/BasicIdentities.thy Fri Apr 01 23:17:40 2022 +0100 @@ -104,6 +104,10 @@ shows "rsimp_ALTs (r1 # rsa @ r2 # rsb) = RALTS (r1 # rsa @ r2 # rsb)" by (metis Nil_is_append_conv list.exhaust rsimp_ALTs.simps(3)) +lemma rsimp_alts_equal: + shows "rsimp_ALTs (rsa @ a # rsb @ a # rsc) = RALTS (rsa @ a # rsb @ a # rsc) " + by (metis append_Cons append_Nil neq_Nil_conv rsimpalts_conscons) + fun rsimp_SEQ :: " rrexp \ rrexp \ rrexp" where @@ -330,17 +334,7 @@ apply(simp add: rders_append rders_simp_append) using inside_simp_removal by blast -lemma simp_helps_der_pierce: - shows " rsimp - (rder x - (rsimp_ALTs rs)) = - rsimp - (rsimp_ALTs - (map (rder x ) - rs - ) - )" - sorry + lemma rders_simp_one_char: @@ -428,9 +422,7 @@ -lemma simp_flatten2: - shows "rsimp (RALTS (r # [RALTS rs])) = rsimp (RALTS (r # rs))" - sorry + lemma simp_flatten: diff -r 10fd25fba2ba -r 56837303ce61 thys2/ClosedForms.thy --- a/thys2/ClosedForms.thy Wed Mar 30 11:18:51 2022 +0100 +++ b/thys2/ClosedForms.thy Fri Apr 01 23:17:40 2022 +0100 @@ -10,6 +10,10 @@ apply (metis no_alt_short_list_after_simp no_further_dB_after_simp) by simp +lemma identity_wwo0: + shows "rsimp (rsimp_ALTs (RZERO # rs)) = rsimp (rsimp_ALTs rs)" + by (metis idem_after_simp1 list.exhaust list.simps(8) list.simps(9) rflts.simps(2) rsimp.simps(2) rsimp.simps(3) rsimp_ALTs.simps(1) rsimp_ALTs.simps(2) rsimp_ALTs.simps(3)) + lemma distinct_removes_last: shows "\a \ set as\ @@ -92,33 +96,15 @@ by (metis distinct_removes_middle(1)) lemma distinct_removes_list: - shows "\a \ set as; \r \ set rs. r \ set as\ \ rdistinct (as @ rs) {} = rdistinct as {}" + shows "\ \r \ set rs. r \ set as\ \ rdistinct (as @ rs) {} = rdistinct as {}" apply(induct rs) apply simp+ - apply(subgoal_tac "rdistinct (as @ aa # rs) {} = rdistinct (as @ rs) {}") + apply(subgoal_tac "rdistinct (as @ a # rs) {} = rdistinct (as @ rs) {}") prefer 2 apply (metis append_Cons append_Nil distinct_removes_middle(1)) by presburger - -lemma simp_rdistinct_f: shows -"f ` rset = frset \ rsimp (rsimp_ALTs (map f (rdistinct rs rset))) = - rsimp (rsimp_ALTs (rdistinct (map f rs) frset)) " - apply(induct rs arbitrary: rset) - apply simp - apply(case_tac "a \ rset") - apply(case_tac " f a \ frset") - apply simp - apply blast - apply(subgoal_tac "f a \ frset") - apply(simp) - apply(subgoal_tac "f ` (insert a rset) = insert (f a) frset") - prefer 2 - apply (meson image_insert) - - oops - lemma spawn_simp_rsimpalts: shows "rsimp (rsimp_ALTs rs) = rsimp (rsimp_ALTs (map rsimp rs))" apply(cases rs) @@ -139,90 +125,6 @@ apply(subst rsimp_idem)+ by (metis comp_apply rsimp_idem) -lemma spawn_simp_distinct: - shows "rsimp (rsimp_ALTs (rsa @ (rdistinct rs (set rsa)))) = rsimp (rsimp_ALTs (rsa @ rs)) -\ (a1 \ set rsa1 \ rsimp (rsimp_ALTs (rsa1 @ rs)) = rsimp (rsimp_ALTs (rsa1 @ a1 # rs))) -\ rsimp (rsimp_ALTs (rsc @ rs)) = rsimp (rsimp_ALTs (rsc @ (rdistinct rs (set rsc))))" - apply(induct rs arbitrary: rsa rsa1 a1 rsc) - apply simp - apply(subgoal_tac "rsimp (rsimp_ALTs (rsa1 @ [a1])) = rsimp (rsimp_ALTs (rsa1 @ (rdistinct [a1] (set rsa1))))") - prefer 2 - - - - - oops - -lemma inv_one_derx: - shows " RONE = rder xa r2 \ r2 = RCHAR xa" - apply(case_tac r2) - apply simp+ - using rrexp.distinct(1) apply presburger - apply (metis rder.simps(5) rrexp.distinct(13) rrexp.simps(20)) - apply simp+ - done - -lemma shape_of_derseq: - shows "rder x (RSEQ r1 r2) = RSEQ (rder x r1) r2 \ rder x (RSEQ r1 r2) = (RALT (RSEQ (rder x r1) r2) (rder x r2))" - using rder.simps(5) by presburger -lemma shape_of_derseq2: - shows "rder x (RSEQ r11 r12) = RSEQ x41 x42 \ x41 = rder x r11" - by (metis rrexp.distinct(25) rrexp.inject(2) shape_of_derseq) - -lemma alts_preimage_case1: - shows "rder x r = RALTS [r] \ \ra. r = RALTS [ra]" - apply(case_tac r) - apply simp+ - apply (metis rrexp.simps(12) rrexp.simps(20)) - apply (metis rrexp.inject(3) rrexp.simps(30) rsimp_ALTs.simps(2) rsimp_ALTs.simps(3) shape_of_derseq) - apply auto[1] - by auto - -lemma alts_preimage_case2: - shows "rder x r = RALT r1 r2 \ \ra rb. (r = RSEQ ra rb \ r = RALT ra rb)" - apply(case_tac r) - apply simp+ - apply (metis rrexp.distinct(15) rrexp.distinct(7)) - apply simp - apply auto[1] - by auto - -lemma alts_preimage_case2_2: - shows "rder x r = RALT r1 r2 \ (\ra rb. r = RSEQ ra rb) \ (\rc rd. r = RALT rc rd)" - using alts_preimage_case2 by blast - -lemma alts_preimage_case3: - shows "rder x r = RALT r1 r2 \ (\ra rb. r = RSEQ ra rb) \ (\rcs rc rd. r = RALTS rcs \ rcs = [rc, rd])" - using alts_preimage_case2 by blast - -lemma star_seq: - shows "rder x (RSEQ (RSTAR a) b) = RALT (RSEQ (RSEQ (rder x a) (RSTAR a)) b) (rder x b)" - using rder.simps(5) rder.simps(6) rnullable.simps(6) by presburger - -lemma language_equality_id1: - shows "\rnullable a \ rder x (RSEQ (RSTAR a) b) = rder x (RALT (RSEQ (RSEQ a (RSTAR a)) b) b)" - apply (subst star_seq) - apply simp - done - - - -lemma distinct_der_set: - shows "(rder x) ` rset = dset \ -rsimp (rsimp_ALTs (map (rder x) (rdistinct rs rset))) = rsimp ( rsimp_ALTs (rdistinct (map (rder x) rs) dset))" - apply(induct rs arbitrary: rset dset) - apply simp - apply(case_tac "a \ rset") - apply(subgoal_tac "rder x a \ dset") - prefer 2 - apply blast - apply simp - apply(case_tac "rder x a \ dset") - prefer 2 - apply simp - - oops - lemma map_concat_cons: shows "map f rsa @ f a # rs = map f (rsa @ [a]) @ rs" by simp @@ -231,29 +133,6 @@ shows " \ a \ aset \ a \ aset" by simp -lemma simp_more_flts: - shows "rsimp (rsimp_ALTs (rdistinct rs {})) = rsimp (rsimp_ALTs (rdistinct (rflts rs) {}))" - - oops - -lemma simp_more_distinct1: - shows "rsimp (rsimp_ALTs rs) = rsimp (rsimp_ALTs (rdistinct rs {}))" - apply(induct rs) - apply simp - apply simp - oops - - -(* -\ - rsimp (rsimp_ALTs (rsb @ (rdistinct rs (set rsb)))) = - rsimp (rsimp_ALTs (rsb @ (rdistinct (rflts rs) (set rsb)))) -*) -lemma simp_removes_duplicate2: - shows "a " - - oops - lemma flts_removes0: shows " rflts (rs @ [RZERO]) = rflts rs" @@ -469,13 +348,6 @@ apply simp using rsimpalts_conscons by presburger -lemma no0_flts: - shows "RZERO \ set (rflts rs)" - apply (induct rs) - apply simp - apply(case_tac a) - apply simp+ - oops @@ -641,11 +513,78 @@ using grewrites_append apply blast by (meson greal_trans grewrites.simps grewrites_concat) +fun alt_set:: "rrexp \ rrexp set" + where + "alt_set (RALTS rs) = set rs \ \ (alt_set ` (set rs))" +| "alt_set r = {r}" + +lemma alt_set_has_all: + shows "RALTS rs \ alt_set rx \ set rs \ alt_set rx" + apply(induct rx arbitrary: rs) + apply simp_all + apply(rename_tac rSS rss) + using in_mono by fastforce + + + + +lemma grewrite_equal_rsimp: + shows "\rs1 \g rs2; rsimp_ALTs (rdistinct (rflts (map rsimp rs1)) (rset \ \(alt_set ` rset))) = + rsimp_ALTs (rdistinct (rflts (map rsimp rs2)) (rset \ \(alt_set ` rset)))\ + \ rsimp_ALTs (rdistinct (rflts (rsimp r # map rsimp rs1)) (rset \ \(alt_set ` rset))) = + rsimp_ALTs (rdistinct (rflts (rsimp r # map rsimp rs2)) (rset \ \(alt_set ` rset)))" + apply(induct rs1 rs2 arbitrary:rset rule: grewrite.induct) + apply simp + apply (metis append_Cons append_Nil flts_middle0) + apply(case_tac "rsimp r \ rset") + apply simp + oops + + + +lemma grewrite_equal_rsimp: + shows "rs1 \g rs2 \ rsimp (RALTS rs1) = rsimp (RALTS rs2)" + apply(induct rs1 rs2 rule: grewrite.induct) + apply simp + using simp_flatten apply blast + prefer 2 + apply (smt (verit) append.assoc append_Cons in_set_conv_decomp simp_removes_duplicate2) + apply simp + apply(case_tac "rdistinct (rflts (map rsimp rs1)) {}") + apply(case_tac "rsimp r = RZERO") + apply simp + apply(case_tac "\rs. rsimp r = RALTS rs") + prefer 2 + + apply(subgoal_tac "rdistinct (rflts (rsimp r # map rsimp rs1)) {} = + rsimp r # rdistinct (rflts (map rsimp rs1)) {rsimp r}") + prefer 2 + apply (simp add: list.inject rflts_def_idiot) + apply(simp only:) + + sorry + + lemma grewrites_equal_rsimp: shows "rs1 \g* rs2 \ rsimp (RALTS rs1) = rsimp (RALTS rs2)" + apply (induct rs1 rs2 rule: grewrites.induct) apply simp + using grewrite_equal_rsimp by presburger + + + + +lemma grewrites_equal_simp_2: + shows "rsimp (RALTS rs1) = rsimp (RALTS rs2) \ rs1 \g* rs2" sorry +lemma grewrites_last: + shows "r # [RALTS rs] \g* r # rs" + by (metis gr_in_rstar grewrite.intros(2) grewrite.intros(3) self_append_conv) + +lemma simp_flatten2: + shows "rsimp (RALTS (r # [RALTS rs])) = rsimp (RALTS (r # rs))" + using grewrites_equal_rsimp grewrites_last by blast lemma frewrites_middle: shows "rs1 \f* rs2 \ r # (RALTS rs # rs1) \f* r # (rs @ rs1)" @@ -674,18 +613,9 @@ by (simp add: frewrites_cons) -fun alt_set:: "rrexp \ rrexp set" - where - "alt_set (RALTS rs) = set rs" -| "alt_set r = {r}" -lemma rd_flts_set: - shows "rs1 \f* rs2 \ rdistinct rs1 ({RZERO} \ (rset \ \(alt_set ` rset))) \g* - rdistinct rs2 ({RZERO} \ (rset \ \(alt_set ` rset)))" - sorry - lemma with_wo0_distinct: shows "rdistinct rs rset \f* rdistinct rs (insert RZERO rset)" apply(induct rs arbitrary: rset) @@ -711,50 +641,126 @@ apply (simp add: frewrites_cons) done +(*Interesting lemma: not obvious but easily proven by sledgehammer*) + + + +(*lemma induction last rule not go through + example: +r # + rdistinct rs1 + (insert RZERO + (insert r + (rset \ + \ (alt_set ` + rset)))) \g* r # + rdistinct rs2 + (insert RZERO (insert r (rset \ \ (alt_set ` rset)))) + rs2 = [+rs] rs3 = rs, +r = +rs +[] \g* rs which is wrong +*) lemma frewrite_with_distinct: shows " \rs2 \f rs3\ \ rdistinct rs2 - (insert RZERO (rset \ \ (alt_set ` rset))) \f* + (insert RZERO (rset \ \ (alt_set ` rset))) \g* rdistinct rs3 (insert RZERO (rset \ \ (alt_set ` rset)))" - apply(induct rs2 rs3 rule: frewrite.induct) + apply(induct rs2 rs3 arbitrary: rset rule: frewrite.induct) apply(case_tac "RZERO \ (rset \ \ (alt_set ` rset))") apply simp apply simp - apply(case_tac "RALTS rs \ rset") - apply simp - apply(subgoal_tac "\r \ set rs. r \ \ (alt_set ` rset)") - apply(subgoal_tac " rdistinct (rs @ rsa) (insert RZERO (rset \ \ (alt_set ` rset))) = - rdistinct rsa (insert RZERO (rset \ \ (alt_set ` rset)))") - using frewrites.intros(1) apply presburger - apply (simp add: rdistinct_concat2) - apply simp - using alt_set.simps(1) apply blast - apply(case_tac "RALTS rs \ rset \ \(alt_set ` rset)") - + - sorry + oops + lemma frewrites_with_distinct: - shows "rs1 \f* rs2 \ - rs1 @ (rdistinct rsa (insert RZERO (set rs1 \ \(alt_set ` (set rs1) )))) \f* - rs2 @ (rdistinct rsb (insert RZERO (set rs2 \ \(alt_set ` (set rs2) ))))" + shows "\rsa \f rsb \ \ +( (rs1 @ (rdistinct rsa (insert RZERO (set rs1 \ \(alt_set ` (set rs1) )))) \g* + rs1 @ (rdistinct rsb (insert RZERO (set rs1 \ \(alt_set ` (set rs1) ))))) +\ ( rs1 @ (rdistinct rsb (insert RZERO (set rs1 \ \(alt_set ` (set rs1) )))) \g* + rs1 @ (rdistinct rsa (insert RZERO (set rs1 \ \(alt_set ` (set rs1) ))))) + ) +" + apply(induct rsa rsb arbitrary: rs1 rule: frewrite.induct) + apply simp + apply(case_tac "RALTS rs \ set rs1") + apply(subgoal_tac "set rs \ \ (alt_set `set rs1)") + apply (metis (full_types) Un_iff Un_insert_left +Un_insert_right grewrites.intros(1) le_supI2 rdistinct.simps(2) rdistinct_concat) + apply (metis Un_subset_iff Union_upper alt_set.simps(1) imageI) + + apply(case_tac "RALTS rs \ \ (alt_set ` set rs1)") + apply simp + apply (smt (z3) UN_insert Un_iff alt_set.simps(1) alt_set_has_all dual_order.trans grewrites.intros(1) insert_absorb rdistinct_concat subset_insertI) + + + oops + + + +lemma rd_flts_set: + shows "rs1 \f* rs2 \ rdistinct rs1 ({RZERO} \ (rset \ \(alt_set ` rset))) \g* + rdistinct rs2 ({RZERO} \ (rset \ \(alt_set ` rset)))" apply(induct rs1 rs2 rule: frewrites.induct) apply simp - + oops + +lemma frewrite_simpeq: + shows "rs1 \f rs2 \ rsimp (RALTS rs1) = rsimp (RALTS rs2)" + apply(induct rs1 rs2 rule: frewrite.induct) + apply simp + using simp_flatten apply presburger + by (meson grewrites_cons grewrites_equal_rsimp grewrites_equal_simp_2) + +lemma frewrite_rd_grewrites: + shows "rs1 \f rs2 \ +\rs3. (rs1 \g* rs3) \ (rs2 \g* rs3) " + apply(induct rs1 rs2 rule: frewrite.induct) + apply(rule_tac x = "rs" in exI) + apply(rule conjI) + apply(rule gr_in_rstar) + apply(rule grewrite.intros) + apply(rule grewrites.intros) + using grewrite.intros(2) apply blast + by (meson grewrites_cons) - sorry + +lemma frewrites_rd_grewrites: + shows "rs1 \f* rs2 \ +\rs3. (rs1 \g* rs3) \ (rs2 \g* rs3)" + apply(induct rs1 rs2 rule: frewrites.induct) + apply simp + apply(rule exI) + apply(rule grewrites.intros) + by (metis frewrite_simpeq grewrites_equal_rsimp grewrites_equal_simp_2) + + + + +lemma frewrite_simpeq2: + shows "rs1 \f rs2 \ rsimp (RALTS (rdistinct rs1 {})) = rsimp (RALTS (rdistinct rs2 {}))" + apply(induct rs1 rs2 rule: frewrite.induct) + apply simp + apply (simp add: distinct_flts_no0) + apply simp (*a more refined notion of \* is needed, this lemma fails when rs1 contains some RALTS rs where elements of rs appear in later parts of rs1, which will be picked up by rs2 and deduplicated*) -lemma wrong_frewrites_with_distinct2: +lemma frewrites_simpeq: shows "rs1 \f* rs2 \ - (rdistinct rs1 {RZERO}) \f* rdistinct rs2 {RZERO}" - oops + rsimp (RALTS (rdistinct rs1 {})) = rsimp (RALTS ( rdistinct rs2 {})) " + apply(induct rs1 rs2 rule: frewrites.induct) + apply simp + + sorry + + lemma frewrite_single_step: shows " rs2 \f rs3 \ rsimp (RALTS rs2) = rsimp (RALTS rs3)" @@ -769,11 +775,38 @@ apply simp using frewrite_single_step by presburger +lemma grewrite_simpalts: + shows " rs2 \g rs3 \ rsimp (rsimp_ALTs rs2) = rsimp (rsimp_ALTs rs3)" + apply(induct rs2 rs3 rule : grewrite.induct) + using identity_wwo0 apply presburger + apply (metis frewrite.intros(1) frewrite_single_step identity_wwo0 rsimp_ALTs.simps(3) simp_flatten) + apply (smt (verit, ccfv_SIG) gmany_steps_later grewrites.intros(1) grewrites_cons grewrites_equal_rsimp identity_wwo0 rsimp_ALTs.simps(3)) + apply simp + apply(subst rsimp_alts_equal) + apply(case_tac "rsa = [] \ rsb = [] \ rsc = []") + apply(subgoal_tac "rsa @ a # rsb @ rsc = [a]") + apply (simp only:) + apply (metis append_Nil frewrite.intros(1) frewrite_single_step identity_wwo0 rsimp_ALTs.simps(3) simp_removes_duplicate1(2)) + apply simp + by (smt (verit, best) append.assoc append_Cons frewrite.intros(1) frewrite_single_step identity_wwo0 in_set_conv_decomp rsimp_ALTs.simps(3) simp_removes_duplicate3) + + +lemma grewrites_simpalts: + shows " rs2 \g* rs3 \ rsimp (rsimp_ALTs rs2) = rsimp (rsimp_ALTs rs3)" + apply(induct rs2 rs3 rule: grewrites.induct) + apply simp + using grewrite_simpalts by presburger +(* lemma frewrites_dB_wwo0_simp: shows "rdistinct rs1 {RZERO} \f* rdistinct rs2 {RZERO} \ rsimp (RALTS (rdistinct rs1 {})) = rsimp (RALTS (rdistinct rs2 {}))" sorry +*) +lemma "rsimp (rsimp_ALTs (RZERO # rdistinct (map (rder x) (rflts rs)) {RZERO})) = + rsimp (rsimp_ALTs (rdistinct (map (rder x) (rflts rs)) {})) " + + sorry @@ -782,13 +815,28 @@ rsimp (RALTS (rdistinct (rflts (map (rder x) rs)) {}))" apply(subgoal_tac "map (rder x) (rflts rs) \f* rflts (map (rder x) rs)") apply(subgoal_tac "rdistinct (map (rder x) (rflts rs)) {RZERO} - \f* rdistinct ( rflts (map (rder x) rs)) {RZERO}") + \g* rdistinct ( rflts (map (rder x) rs)) {RZERO}") apply(subgoal_tac "rsimp (RALTS (rdistinct (map (rder x) (rflts rs)) {})) = rsimp (RALTS ( rdistinct ( rflts (map (rder x) rs)) {}))") apply meson - using frewrites_dB_wwo0_simp apply blast - using frewrites_with_distinct2 apply blast - using early_late_der_frewrites by blast + apply (metis distinct_flts_no0 grewrites_equal_rsimp rsimp.simps(2)) + sorry + + + + + + + + +lemma simp_der_pierce_flts_prelim: + shows "rsimp (rsimp_ALTs (rdistinct (map (rder x) (rflts rs)) {})) + = rsimp (rsimp_ALTs (rdistinct (rflts (map (rder x) rs)) {}))" + apply(subgoal_tac "map (rder x) (rflts rs) \g* rflts (map (rder x) rs)") + apply(subgoal_tac "rdistinct (map (rder x) (rflts rs)) {RZERO} \g* rdistinct (rflts (map (rder x) rs)) {RZERO}") + using grewrites_equal_simp_2 grewrites_simpalts simp_der_flts apply blast + apply (simp add: early_late_der_frewrites frewrites_with_distinct2_grewrites) + using early_late_der_frewrites frewrites_equivalent_simp grewrites_equal_simp_2 by blast lemma simp_der_pierce_flts: @@ -798,9 +846,7 @@ rsimp ( rsimp_ALTs (rdistinct (rflts (map (rder x) (map (rsimp \ (\r. rders_simp r xs)) rs))) {}) )" - - sorry - + using simp_der_pierce_flts_prelim by presburger @@ -1119,10 +1165,7 @@ apply simp apply fastforce apply (metis inside_simp_removal list.map_comp rder.simps(4) rsimp.simps(2) rsimp_idem) - sledgehammer - (* by (metis inside_simp_removal rder_rsimp_ALTs_commute self_append_conv2 set_empty simp_more_distinct) - - *) + using simp_der_pierce_flts by blast lemma alts_closed_form_variant: shows "s \ [] \ rders_simp (RALTS rs) s = @@ -1167,4 +1210,16 @@ apply force 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