equal
deleted
inserted
replaced
33 |
33 |
34 |
34 |
35 lemma seq_closed_form: shows |
35 lemma seq_closed_form: shows |
36 "rsimp (rders_simp (RSEQ r1 r2) s) = |
36 "rsimp (rders_simp (RSEQ r1 r2) s) = |
37 rsimp ( RALTS ( (RSEQ (rders_simp r1 s) r2) # |
37 rsimp ( RALTS ( (RSEQ (rders_simp r1 s) r2) # |
38 (map (rders r2) (vsuf s r1)) |
38 (map (rders_simp r2) (vsuf s r1)) |
39 ) |
39 ) |
40 )" |
40 )" |
41 apply(induct s) |
41 apply(induct s) |
42 apply simp |
42 apply simp |
43 sorry |
43 sorry |
44 |
44 |
45 |
45 |
46 lemma seq_closed_form_variant: shows |
46 lemma seq_closed_form_variant: shows |
47 "s \<noteq> [] \<Longrightarrow> (rders_simp (RSEQ r1 r2) s) = |
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))))" |
48 rsimp (RALTS ((RSEQ (rders_simp r1 s) r2) # (map (rders_simp r2) (vsuf s r1))))" |
49 sorry |
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 |
50 |
61 |
51 end |
62 end |