equal
deleted
inserted
replaced
1 theory ClosedForms imports |
1 theory ClosedForms imports |
2 "BasicIdentities" |
2 "BasicIdentities" |
3 begin |
3 begin |
|
4 |
|
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 |
4 |
31 |
5 lemma alts_closed_form: shows |
32 lemma alts_closed_form: shows |
6 "rsimp (rders_simp (RALTS rs) s) = |
33 "rsimp (rders_simp (RALTS rs) s) = |
7 rsimp (RALTS (map (\<lambda>r. rders_simp r s) rs))" |
34 rsimp (RALTS (map (\<lambda>r. rders_simp r s) rs))" |
8 apply(induct s rule: rev_induct) |
35 apply(induct s rule: rev_induct) |
12 apply(subgoal_tac " rsimp (rders_simp (rders_simp (RALTS rs) xs) [x]) = |
39 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])") |
40 rsimp(rders_simp (rsimp_ALTs (rdistinct (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs)) {})) [x])") |
14 prefer 2 |
41 prefer 2 |
15 apply (metis inside_simp_removal rders_simp_one_char) |
42 apply (metis inside_simp_removal rders_simp_one_char) |
16 apply(simp only: ) |
43 apply(simp only: ) |
|
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 |
17 sorry |
58 sorry |
18 |
59 |
19 lemma alts_closed_form_variant: shows |
60 lemma alts_closed_form_variant: shows |
20 "s \<noteq> [] \<Longrightarrow> rders_simp (RALTS rs) s = |
61 "s \<noteq> [] \<Longrightarrow> rders_simp (RALTS rs) s = |
21 rsimp (RALTS (map (\<lambda>r. rders_simp r s) rs))" |
62 rsimp (RALTS (map (\<lambda>r. rders_simp r s) rs))" |