|
444
|
1 |
theory ClosedForms imports
|
|
|
2 |
"BasicIdentities"
|
|
443
|
3 |
begin
|
|
|
4 |
|
|
451
|
5 |
|
|
|
6 |
|
|
|
7 |
lemma simp_rdistinct_f: shows
|
|
|
8 |
"f ` rset = frset \<Longrightarrow> rsimp (rsimp_ALTs (map f (rdistinct rs rset))) = rsimp (rsimp_ALTs (rdistinct (map f rs) frset)) "
|
|
|
9 |
apply(induct rs arbitrary: rset)
|
|
|
10 |
apply simp
|
|
|
11 |
apply(case_tac "a \<in> rset")
|
|
|
12 |
apply(case_tac " f a \<in> frset")
|
|
|
13 |
apply simp
|
|
|
14 |
apply blast
|
|
|
15 |
apply(subgoal_tac "f a \<notin> frset")
|
|
|
16 |
apply(simp)
|
|
|
17 |
apply(subgoal_tac "f ` (insert a rset) = insert (f a) frset")
|
|
|
18 |
prefer 2
|
|
|
19 |
apply (meson image_insert)
|
|
|
20 |
|
|
|
21 |
|
|
|
22 |
|
|
|
23 |
sorry
|
|
|
24 |
|
|
|
25 |
|
|
|
26 |
lemma distinct_der:
|
|
|
27 |
shows "rsimp (rsimp_ALTs (map (rder x) (rdistinct rs {}))) = rsimp ( rsimp_ALTs (rdistinct (map (rder x) rs) {}))"
|
|
|
28 |
|
|
|
29 |
sorry
|
|
|
30 |
|
|
|
31 |
|
|
444
|
32 |
lemma alts_closed_form: shows
|
|
|
33 |
"rsimp (rders_simp (RALTS rs) s) =
|
|
|
34 |
rsimp (RALTS (map (\<lambda>r. rders_simp r s) rs))"
|
|
|
35 |
apply(induct s rule: rev_induct)
|
|
|
36 |
apply simp
|
|
|
37 |
apply simp
|
|
|
38 |
apply(subst rders_simp_append)
|
|
|
39 |
apply(subgoal_tac " rsimp (rders_simp (rders_simp (RALTS rs) xs) [x]) =
|
|
|
40 |
rsimp(rders_simp (rsimp_ALTs (rdistinct (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs)) {})) [x])")
|
|
|
41 |
prefer 2
|
|
|
42 |
apply (metis inside_simp_removal rders_simp_one_char)
|
|
|
43 |
apply(simp only: )
|
|
451
|
44 |
apply(subst rders_simp_one_char)
|
|
|
45 |
apply(subst rsimp_idem)
|
|
|
46 |
apply(subgoal_tac "rsimp (rder x (rsimp_ALTs (rdistinct (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs)) {}))) =
|
|
|
47 |
rsimp ((rsimp_ALTs (map (rder x) (rdistinct (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs)) {})))) ")
|
|
|
48 |
prefer 2
|
|
|
49 |
using rder_rsimp_ALTs_commute apply presburger
|
|
|
50 |
apply(simp only:)
|
|
|
51 |
apply(subgoal_tac "rsimp (rsimp_ALTs (map (rder x) (rdistinct (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs)) {})))
|
|
|
52 |
= rsimp (rsimp_ALTs (rdistinct (map (rder x) (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs))) {}))")
|
|
|
53 |
prefer 2
|
|
|
54 |
|
|
|
55 |
using distinct_der apply presburger
|
|
|
56 |
apply(simp only:)
|
|
|
57 |
|
|
444
|
58 |
sorry
|
|
443
|
59 |
|
|
444
|
60 |
lemma alts_closed_form_variant: shows
|
|
|
61 |
"s \<noteq> [] \<Longrightarrow> rders_simp (RALTS rs) s =
|
|
|
62 |
rsimp (RALTS (map (\<lambda>r. rders_simp r s) rs))"
|
|
|
63 |
sorry
|
|
443
|
64 |
|
|
|
65 |
|
|
|
66 |
|
|
444
|
67 |
lemma star_closed_form:
|
|
|
68 |
shows "rders_simp (RSTAR r0) (c#s) =
|
|
|
69 |
rsimp ( RALTS ( (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) (star_updates s r0 [[c]]) ) ))"
|
|
|
70 |
apply(induct s)
|
|
|
71 |
apply simp
|
|
|
72 |
sorry
|
|
443
|
73 |
|
|
|
74 |
|
|
|
75 |
|
|
|
76 |
lemma seq_closed_form: shows
|
|
|
77 |
"rsimp (rders_simp (RSEQ r1 r2) s) =
|
|
|
78 |
rsimp ( RALTS ( (RSEQ (rders_simp r1 s) r2) #
|
|
445
|
79 |
(map (rders_simp r2) (vsuf s r1))
|
|
443
|
80 |
)
|
|
|
81 |
)"
|
|
|
82 |
apply(induct s)
|
|
|
83 |
apply simp
|
|
|
84 |
sorry
|
|
|
85 |
|
|
|
86 |
|
|
444
|
87 |
lemma seq_closed_form_variant: shows
|
|
|
88 |
"s \<noteq> [] \<Longrightarrow> (rders_simp (RSEQ r1 r2) s) =
|
|
|
89 |
rsimp (RALTS ((RSEQ (rders_simp r1 s) r2) # (map (rders_simp r2) (vsuf s r1))))"
|
|
445
|
90 |
apply(induct s rule: rev_induct)
|
|
|
91 |
apply simp
|
|
|
92 |
apply(subst rders_simp_append)
|
|
|
93 |
apply(subst rders_simp_one_char)
|
|
|
94 |
apply(subst rsimp_idem[symmetric])
|
|
|
95 |
apply(subst rders_simp_one_char[symmetric])
|
|
|
96 |
apply(subst rders_simp_append[symmetric])
|
|
|
97 |
apply(insert seq_closed_form)
|
|
|
98 |
apply(subgoal_tac "rsimp (rders_simp (RSEQ r1 r2) (xs @ [x]))
|
|
|
99 |
= rsimp (RALTS (RSEQ (rders_simp r1 (xs @ [x])) r2 # map (rders_simp r2) (vsuf (xs @ [x]) r1)))")
|
|
|
100 |
apply force
|
|
|
101 |
by presburger
|
|
443
|
102 |
|
|
444
|
103 |
end |