diff -r e6248d2c20c2 -r 2e7c7111c0be thys2/ClosedForms.thy --- a/thys2/ClosedForms.thy Wed Mar 23 10:09:32 2022 +0000 +++ b/thys2/ClosedForms.thy Thu Mar 24 20:52:34 2022 +0000 @@ -2,15 +2,17 @@ "BasicIdentities" begin -lemma add0_isomorphic: - shows "rsimp_ALTs (rdistinct (rflts [rsimp r, RZERO]) {}) = rsimp r" - sorry - +lemma idem_after_simp1: + shows "rsimp_ALTs (rdistinct (rflts [rsimp aa]) {}) = rsimp aa" + apply(case_tac "rsimp aa") + apply simp+ + apply (metis no_alt_short_list_after_simp no_further_dB_after_simp) + by simp lemma distinct_removes_last: - shows "\(a::rrexp) \ set as\ + shows "\a \ set as\ \ rdistinct as rset = rdistinct (as @ [a]) rset" and "rdistinct (ab # as @ [ab]) rset1 = rdistinct (ab # as) rset1" apply(induct as arbitrary: rset ab rset1 a) @@ -48,36 +50,61 @@ by (metis append_Cons insert_iff insert_is_Un rdistinct.simps(2)) -lemma distinct_removes_last2: - shows "\(a::rrexp) \ set as\ - \ rdistinct as rset = rdistinct (as @ [a]) rset" - using distinct_removes_last(1) by presburger - -lemma distinct_append_simp: - shows " rsimp (rsimp_ALTs rs1) = rsimp (rsimp_ALTs rs2) \ - rsimp (rsimp_ALTs (f a # rs1)) = - rsimp (rsimp_ALTs (f a # rs2))" - apply(case_tac rs1) +lemma distinct_removes_middle: + shows "\a \ set as\ + \ rdistinct (as @ as2) rset = rdistinct (as @ [a] @ as2) rset" +and "rdistinct (ab # as @ [ab] @ as3) rset1 = rdistinct (ab # as @ as3) rset1" + apply(induct as arbitrary: rset rset1 ab as2 as3 a) + apply simp + apply simp + apply(case_tac "a \ rset") + apply simp + apply metis apply simp - apply(case_tac rs2) - apply simp + apply (metis insertI1) + apply(case_tac "a = ab") apply simp - prefer 2 - apply(case_tac list) - apply(case_tac rs2) - apply simp - using add0_isomorphic apply blast + apply(case_tac "ab \ rset") apply simp - sorry - -(* apply (smt (z3) append.right_neutral empty_iff list.distinct(1) list.inject no_alt_short_list_after_simp no_further_dB_after_simp rdistinct.elims rflts.elims rflts.simps(2) rsimp_ALTs.simps(1) rsimp_ALTs.simps(2)))*) + apply presburger + apply (meson insertI1) + apply(case_tac "a \ rset") + apply (metis (no_types, opaque_lifting) Un_insert_left append_Cons insert_iff rdistinct.simps(2) sup_bot_left) + apply(case_tac "ab \ rset") + apply simp + apply (meson insert_iff) + apply simp + by (metis insertI1) +lemma distinct_removes_middle3: + shows "\a \ set as\ + \ rdistinct (as @ a #as2) rset = rdistinct (as @ as2) rset" + using distinct_removes_middle(1) by fastforce + +lemma distinct_removes_last2: + shows "\a \ set as\ + \ rdistinct as rset = rdistinct (as @ [a]) rset" + by (simp add: distinct_removes_last(1)) + +lemma distinct_removes_middle2: + shows "a \ set as \ rdistinct (as @ [a] @ rs) {} = rdistinct (as @ rs) {}" + 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 {}" + apply(induct rs) + apply simp+ + apply(subgoal_tac "rdistinct (as @ aa # 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)) " +"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") @@ -209,14 +236,259 @@ 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" + apply(induct rs) + apply simp + by (metis append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot) + +lemma flts_keeps1: + shows " rflts (rs @ [RONE]) = + rflts rs @ [RONE] " + apply (induct rs) + apply simp + by (metis append.assoc append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot) + +lemma flts_keeps_others: + shows "\a \ RZERO; \rs1. a = RALTS rs1\ \rflts (rs @ [a]) = rflts rs @ [a]" + apply(induct rs) + apply simp + apply (simp add: rflts_def_idiot) + apply(case_tac a) + apply simp + using flts_keeps1 apply blast + apply (metis append.assoc append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot) + apply (metis append.assoc append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot) + apply blast + by (metis append.assoc append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot) + + +lemma rflts_def_idiot2: + shows "\a \ RZERO; \rs1. a = RALTS rs1; a \ set rs\ \ a \ set (rflts rs)" + apply(induct rs) + apply simp + by (metis append.assoc in_set_conv_decomp insert_iff list.simps(15) rflts.simps(2) rflts.simps(3) rflts_def_idiot) + +lemma rflts_spills_last: + shows "a = RALTS rs \ rflts (rs1 @ [a]) = rflts rs1 @ rs" + apply (induct rs1) + apply simp + by (metis append.assoc append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot) + + +lemma spilled_alts_contained: + shows "\a = RALTS rs ; a \ set rs1\ \ \r \ set rs. r \ set (rflts rs1)" + apply(induct rs1) + apply simp + apply(case_tac "a = aa") + apply simp + apply(subgoal_tac " a \ set rs1") + prefer 2 + apply (meson set_ConsD) + apply(case_tac aa) + using rflts.simps(2) apply presburger + apply fastforce + apply fastforce + apply fastforce + apply fastforce + by fastforce + +lemma distinct_removes_duplicate_flts: + shows " a \ set rsa + \ rdistinct (rflts (map rsimp rsa @ [rsimp a])) {} = + rdistinct (rflts (map rsimp rsa)) {}" + apply(subgoal_tac "rsimp a \ set (map rsimp rsa)") + prefer 2 + apply simp + apply(induct "rsimp a") + apply simp + using flts_removes0 apply presburger + apply(subgoal_tac " rdistinct (rflts (map rsimp rsa @ [rsimp a])) {} = + rdistinct (rflts (map rsimp rsa @ [RONE])) {}") + apply (simp only:) + apply(subst flts_keeps1) + apply (metis distinct_removes_last2 rflts_def_idiot2 rrexp.simps(20) rrexp.simps(6)) + apply presburger + apply(subgoal_tac " rdistinct (rflts (map rsimp rsa @ [rsimp a])) {} = + rdistinct ((rflts (map rsimp rsa)) @ [RCHAR x]) {}") + apply (simp only:) + prefer 2 + apply (metis flts_keeps_others rrexp.distinct(21) rrexp.distinct(3)) + apply (metis distinct_removes_last2 rflts_def_idiot2 rrexp.distinct(21) rrexp.distinct(3)) + + apply (metis distinct_removes_last2 flts_keeps_others rflts_def_idiot2 rrexp.distinct(25) rrexp.distinct(5)) + prefer 2 + apply (metis distinct_removes_last2 flts_keeps_others flts_removes0 rflts_def_idiot2 rrexp.distinct(29)) + apply(subgoal_tac "rflts (map rsimp rsa @ [rsimp a]) = rflts (map rsimp rsa) @ x") + prefer 2 + apply (simp add: rflts_spills_last) + apply(simp only:) + apply(subgoal_tac "\ r \ set x. r \ set (rflts (map rsimp rsa))") + prefer 2 + using spilled_alts_contained apply presburger + by (metis append_self_conv distinct_removes_list in_set_conv_decomp rev_exhaust) + +lemma flts_middle0: + shows "rflts (rsa @ RZERO # rsb) = rflts (rsa @ rsb)" + apply(induct rsa) + apply simp + by (metis append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot) + +lemma flts_middle01: + shows "rflts (rsa @ [RZERO] @ rsb) = rflts (rsa @ rsb)" + by (simp add: flts_middle0) + +lemma flts_append1: + shows "\a \ RZERO; \rs1. a = RALTS rs1; a \ set rs\ \ + rflts (rsa @ [a] @ rsb) = rflts rsa @ [a] @ (rflts rsb)" + apply(induct rsa arbitrary: rsb) + apply simp + using rflts_def_idiot apply presburger + apply(case_tac aa) + apply simp+ + done + +lemma flts_append: + shows "rflts (rs1 @ rs2) = rflts rs1 @ rflts rs2" + apply(induct rs1) + apply simp + apply(case_tac a) + apply simp+ + done + +lemma simp_removes_duplicate1: + shows " a \ set rsa \ rsimp (RALTS (rsa @ [a])) = rsimp (RALTS (rsa))" +and " rsimp (RALTS (a1 # rsa @ [a1])) = rsimp (RALTS (a1 # rsa))" + apply(induct rsa arbitrary: a1) + apply simp + apply simp + prefer 2 + apply(case_tac "a = aa") + apply simp + apply simp + apply (metis Cons_eq_appendI Cons_eq_map_conv distinct_removes_duplicate_flts list.set_intros(2)) + apply (metis append_Cons append_Nil distinct_removes_duplicate_flts list.set_intros(1) list.simps(8) list.simps(9)) + by (metis (mono_tags, lifting) append_Cons distinct_removes_duplicate_flts list.set_intros(1) list.simps(8) list.simps(9) map_append rsimp.simps(2)) + +lemma simp_removes_duplicate2: + shows "a \ set rsa \ rsimp (RALTS (rsa @ [a] @ rsb)) = rsimp (RALTS (rsa @ rsb))" + apply(induct rsb arbitrary: rsa) + apply simp + using distinct_removes_duplicate_flts apply auto[1] + by (metis append.assoc head_one_more_simp rsimp.simps(2) simp_flatten simp_removes_duplicate1(1)) + +lemma simp_removes_duplicate3: + shows "a \ set rsa \ rsimp (RALTS (rsa @ a # rsb)) = rsimp (RALTS (rsa @ rsb))" + using simp_removes_duplicate2 by auto + +lemma distinct_removes_middle4: + shows "a \ set rsa \ rdistinct (rsa @ [a] @ rsb) rset = rdistinct (rsa @ rsb) rset" + using distinct_removes_middle(1) by fastforce + +lemma distinct_removes_middle_list: + shows "\a \ set x. a \ set rsa \ rdistinct (rsa @ x @ rsb) rset = rdistinct (rsa @ rsb) rset" + apply(induct x) + apply simp + by (simp add: distinct_removes_middle3) + + +lemma distinct_removes_duplicate_flts2: + shows " a \ set rsa + \ rdistinct (rflts (rsa @ [a] @ rsb)) {} = + rdistinct (rflts (rsa @ rsb)) {}" + apply(induct a arbitrary: rsb) + using flts_middle01 apply presburger + apply(subgoal_tac "rflts (rsa @ [RONE] @ rsb) = rflts rsa @ [RONE] @ rflts rsb") + prefer 2 + using flts_append1 apply blast + apply simp + apply(subgoal_tac "RONE \ set (rflts rsa)") + prefer 2 + using rflts_def_idiot2 apply blast + apply(subst distinct_removes_middle3) + apply simp + using flts_append apply presburger + apply simp + apply (metis distinct_removes_middle3 flts_append in_set_conv_decomp rflts.simps(5)) + apply (metis distinct_removes_middle(1) flts_append flts_append1 rflts_def_idiot2 rrexp.distinct(25) rrexp.distinct(5)) + apply(subgoal_tac "rflts (rsa @ [RALTS x] @ rsb) = rflts rsa @ x @ rflts rsb") + prefer 2 + apply (simp add: flts_append) + apply (simp only:) + + apply(subgoal_tac "\r1 \ set x. r1 \ set (rflts rsa)") + prefer 2 + using spilled_alts_contained apply blast + apply(subst flts_append) + using distinct_removes_middle_list apply blast + using distinct_removes_middle2 flts_append rflts_def_idiot2 by fastforce + + +lemma simp_removes_duplicate: + shows "a \ set rsa \ rsimp (rsimp_ALTs (rsa @ a # rs)) = rsimp (rsimp_ALTs (rsa @ rs))" + apply(subgoal_tac "rsimp (rsimp_ALTs (rsa @ a # rs)) = rsimp (RALTS (rsa @ a # rs))") + prefer 2 + apply (smt (verit, best) Cons_eq_append_conv append_is_Nil_conv empty_set equals0D list.distinct(1) rsimp_ALTs.elims) + apply(simp only:) + apply simp + apply(subgoal_tac "(rdistinct (rflts (map rsimp rsa @ rsimp a # map rsimp rs)) {}) = (rdistinct (rflts (map rsimp rsa @ map rsimp rs)) {})") + apply(simp only:) + prefer 2 + apply(subgoal_tac "rsimp a \ set (map rsimp rsa)") + prefer 2 + apply simp + using distinct_removes_duplicate_flts2 apply force + apply(case_tac rsa) + apply simp + apply(case_tac rs) + apply simp + apply(case_tac list) + apply simp + using idem_after_simp1 apply presburger + apply simp+ + apply(subgoal_tac "rsimp_ALTs (aa # list @ aaa # lista) = RALTS (aa # list @ aaa # lista)") + apply simp + using rsimpalts_conscons by presburger + +lemma simp_der_pierce_flts: + shows " rsimp (rsimp_ALTs (rdistinct (map (rder x) (rflts (map (rsimp \ (\r. rders_simp r xs)) rs))) {})) = + rsimp (rsimp_ALTs (rdistinct (rflts (map (rder x) (map (rsimp \ (\r. rders_simp r xs)) rs))) {}))" + oops + lemma simp_more_distinct: - shows "rsimp (rsimp_ALTs (rsa @ rs)) = rsimp (rsimp_ALTs (rsa @ (rdistinct rs (set rsa)))) \ - rsimp (rsimp_ALTs (rsb @ (rdistinct rs (set rsb)))) = - rsimp (rsimp_ALTs (rsb @ (rdistinct (rflts rs) (set rsb))))" - apply(induct rs arbitrary: rsa rsb) + shows "rsimp (rsimp_ALTs (rsa @ rs)) = rsimp (rsimp_ALTs (rsa @ (rdistinct rs (set rsa)))) " +and "a1 \ set rsb \ rsimp (rsimp_ALTs (rsb @ a1 # rs)) = rsimp (rsimp_ALTs (rsb @ rs))" + apply(induct rs arbitrary: rsa rsb a1) + apply simp + apply simp + apply(case_tac " a \ set rsa") apply simp + prefer 2 + apply simp + apply(drule_tac x = "rsa @ [a]" in meta_spec) + apply simp + sorry @@ -316,9 +588,9 @@ done lemma distinct_removes_last3: - shows "\(a::rrexp) \ set as\ + shows "\a \ set as\ \ rdistinct as {} = rdistinct (as @ [a]) {}" - using distinct_removes_last2 by blast + by (simp add: distinct_removes_last2) lemma set_inclusion_with_flts1: shows " \RONE \ set rs\ \ RONE \ set (rflts rs)" @@ -367,6 +639,8 @@ \ rsimp_ALTs (rdistinct (rflts (map rsimp as @ [rsimp a])) {}) = rsimp_ALTs (rdistinct (rflts (map rsimp as @ x5)) {})" + sorry + lemma last_elem_dup1: shows " a \ set as \ rsimp (RALTS (as @ [a] )) = rsimp (RALTS (as ))" @@ -461,6 +735,29 @@ rsimp_ALTs (rdistinct (rflts rs) {})" by (metis map_idI rsimp.simps(2) rsimp_idem) + +lemma add0_isomorphic: + shows "rsimp_ALTs (rdistinct (rflts [rsimp r, RZERO]) {}) = rsimp r" + sorry + + +lemma distinct_append_simp: + shows " rsimp (rsimp_ALTs rs1) = rsimp (rsimp_ALTs rs2) \ + rsimp (rsimp_ALTs (f a # rs1)) = + rsimp (rsimp_ALTs (f a # rs2))" + apply(case_tac rs1) + apply simp + apply(case_tac rs2) + apply simp + apply simp + prefer 2 + apply(case_tac list) + apply(case_tac rs2) + apply simp + using add0_isomorphic apply blast + apply simp + sorry + lemma alts_closed_form: shows "rsimp (rders_simp (RALTS rs) s) = rsimp (RALTS (map (\r. rders_simp r s) rs))" @@ -501,12 +798,11 @@ apply(subst repeated_altssimp) apply simp apply fastforce - apply (metis inside_simp_removal list.map_comp rder.simps(4) rsimp.simps(2) rsimp_idem) - -(* apply (metis head_one_more_simp list.inject list.map_comp list.simps(9) rders_simp_lambda rsimp.simps(2)) -*) + 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) - sorry + *) lemma alts_closed_form_variant: shows "s \ [] \ rders_simp (RALTS rs) s =