|
444
|
1 |
theory ClosedForms imports
|
|
|
2 |
"BasicIdentities"
|
|
443
|
3 |
begin
|
|
|
4 |
|
|
444
|
5 |
lemma alts_closed_form: shows
|
|
|
6 |
"rsimp (rders_simp (RALTS rs) s) =
|
|
|
7 |
rsimp (RALTS (map (\<lambda>r. rders_simp r s) rs))"
|
|
|
8 |
apply(induct s rule: rev_induct)
|
|
|
9 |
apply simp
|
|
|
10 |
apply simp
|
|
|
11 |
apply(subst rders_simp_append)
|
|
|
12 |
apply(subgoal_tac " rsimp (rders_simp (rders_simp (RALTS rs) xs) [x]) =
|
|
|
13 |
rsimp(rders_simp (rsimp_ALTs (rdistinct (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs)) {})) [x])")
|
|
|
14 |
prefer 2
|
|
|
15 |
apply (metis inside_simp_removal rders_simp_one_char)
|
|
|
16 |
apply(simp only: )
|
|
|
17 |
sorry
|
|
443
|
18 |
|
|
444
|
19 |
lemma alts_closed_form_variant: shows
|
|
|
20 |
"s \<noteq> [] \<Longrightarrow> rders_simp (RALTS rs) s =
|
|
|
21 |
rsimp (RALTS (map (\<lambda>r. rders_simp r s) rs))"
|
|
|
22 |
sorry
|
|
443
|
23 |
|
|
|
24 |
|
|
|
25 |
|
|
444
|
26 |
lemma star_closed_form:
|
|
|
27 |
shows "rders_simp (RSTAR r0) (c#s) =
|
|
|
28 |
rsimp ( RALTS ( (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) (star_updates s r0 [[c]]) ) ))"
|
|
|
29 |
apply(induct s)
|
|
|
30 |
apply simp
|
|
|
31 |
sorry
|
|
443
|
32 |
|
|
|
33 |
|
|
|
34 |
|
|
|
35 |
lemma seq_closed_form: shows
|
|
|
36 |
"rsimp (rders_simp (RSEQ r1 r2) s) =
|
|
|
37 |
rsimp ( RALTS ( (RSEQ (rders_simp r1 s) r2) #
|
|
445
|
38 |
(map (rders_simp r2) (vsuf s r1))
|
|
443
|
39 |
)
|
|
|
40 |
)"
|
|
|
41 |
apply(induct s)
|
|
|
42 |
apply simp
|
|
|
43 |
sorry
|
|
|
44 |
|
|
|
45 |
|
|
444
|
46 |
lemma seq_closed_form_variant: shows
|
|
|
47 |
"s \<noteq> [] \<Longrightarrow> (rders_simp (RSEQ r1 r2) s) =
|
|
|
48 |
rsimp (RALTS ((RSEQ (rders_simp r1 s) r2) # (map (rders_simp r2) (vsuf s r1))))"
|
|
445
|
49 |
apply(induct s rule: rev_induct)
|
|
|
50 |
apply simp
|
|
|
51 |
apply(subst rders_simp_append)
|
|
|
52 |
apply(subst rders_simp_one_char)
|
|
|
53 |
apply(subst rsimp_idem[symmetric])
|
|
|
54 |
apply(subst rders_simp_one_char[symmetric])
|
|
|
55 |
apply(subst rders_simp_append[symmetric])
|
|
|
56 |
apply(insert seq_closed_form)
|
|
|
57 |
apply(subgoal_tac "rsimp (rders_simp (RSEQ r1 r2) (xs @ [x]))
|
|
|
58 |
= rsimp (RALTS (RSEQ (rders_simp r1 (xs @ [x])) r2 # map (rders_simp r2) (vsuf (xs @ [x]) r1)))")
|
|
|
59 |
apply force
|
|
|
60 |
by presburger
|
|
443
|
61 |
|
|
444
|
62 |
end |